Formal学习笔记之算法基础学习
compare specifications
通常，我们会将spec和设计实现进行比较。spec相对来说比较抽象些，可以是些sva的assertion，rtl model或者一些hvl，比如systemc等。而implemenation通常是rtl代码或者网表。
图1是一个简单的checker，a和b分别表示两种spec，它们接收相同的输入(input)，checker比较二者的输出是否相等。如果找到一个输入序列导致输出比较失败，就是找个了一个反例（counterexample）,工具会将此反例，包括相应的输入记录下来，呈现出来。这个checker其实是个黑盒（black box），因为我们无法观察a和b内部的状态或者信号（白盒white box则可以）。
图1 simple checker
如果a和b足够简单，那我们可以测到所有可能的情形，或者用formal verification来判定二者完全等价。同时，我们也可以借助这个等价来简化一些复杂的的问题，例如图2所示，一个更加复杂的系统，里面包含了a和b。
在这个例子中，因为我们先前已经证明了a等价于b，我们可以做下简化操作，把a和b从系统中拿掉，简化成c和d的比较，如图3所示。当然，c和d的输入(inputs’) 与原始的输入(input)已经有了很大的差别。这种divide and conquer 策略在fv中经常使用，主要用来简化分析大的design。
我们可以把上下方框想象成spec和implementation，这样的比较输入和输入我们可以判定implementation与spec是等价的，设计符合我们的要求。这个一个典型的formal equivalence verification (fev) 。不过，通常spec和implementation不会出现这种理想的等价情况。
cones of influence
如果我们把一些把相干的逻辑分别考量，验证复杂度能大大简化。比如，我们有个硬件，实现加法和乘法运算；在跑simulation的时候，我们可能造不同case侧重不同的点，有点测加法，有的测乘法。如果我们加法和乘法拆分出来，单独验，效率定能大幅提升，但在simulation里面不太现实，因为这需要造几套验证环境。
fv则能比较好的支持这种拆分，fv工具读取property，将设计里面一些与当前property不相关的逻辑移移除掉。这个叫cone of influence 简化。如图4所示，我们只考量result 输出的时候，很多逻辑对这个输出没影响，我们可以把它们简化掉。如果design特别大的话，这种可以极大的简化复杂度。
fv工具也可以支持用户自定义的简化，而非自动简化。例如有个输入，我们可以绑定成某个固定的值。这样逻辑也能大大简化。
bdd
bdd(binary decision tree)，顾名思义，用树形结果来表示电路的逻辑。如果去观察一些电路的真值表如图5，会发现有很多redundancy，很多行都是0。bdd可以表示相同设计的同时，移除一些冗余的逻辑。bdd是一种范式（canonical ），等价设计的bdd是一样的；如果两个电路的bdd一样，那么可以判定二者等价。bdd算法是第一代formal 工具常用的算法。
我们以一个mux为例来说明bdd，如图6所示，一个mux逻辑的bdd算法， xyz为输入，最下面一行为输出。类似于红黑树，每一个分支左侧代表下一输入变量为0，右侧代表输入为1.
我们把输出为0和1的做下merge，如图7所示。
进一步观察，左侧两个z，无论取值如何，输出都是一样，说明父节点y不影响结果。同理，对于观察右侧，z节点多余。于是，我们可以进一步简化成图8这样的。
当然，如果选择变量的顺序不一样，我们得到的bdd的大小会有所不同。如果我们选择z->x->y的顺序的，我们将得到图9这样的bdd。对于一些大的design来说，如果顺序选择不当，可能导致指数爆炸。通常用heuristic-based 算法来寻找最佳的变量顺序。比如根据电路的拓扑结构来，根据变量的相关性来映射。另一种方法是尝试将每一个输入变量替换0或者1，看看哪个精简的程度更大些。
对于大而复杂的设计来说，提取bdd仍然是一件很艰难的工作，或许随着输入的增加而指数级增长。
computing a bdd for a circuit design
如果我们有真值表，我们可以很快速的提取出bdd。但大部分电路，我们没那么容易算出真值表，尤其对rtl而言。庆幸的是，我们将根据基本的逻辑（与、或、非）的bdd组合起来，算出更大设计的bdd。
基本的与或非逻辑的bdd，参见图10所示。
例如，我们以 (x&&y)||z 为例，电路如图11所示。将这些基本门电路组合在一起，就是这个电路的bdd，参见图12.
model checking
model checking 是fv工具分析一段时间内时序逻辑的主要方法。给定properties ，model-checking 会去搜索可能的未来状态，然后判定是否违反这些property。
首先创建初始状态的bdd，然后根据相应的逻辑推导出下一个状态的bdd，不断重复这个过程（reachability ），直到所有的状态都加进来。如果遇到vilation，fv会倒推回去，给出一个反例。
model checker 可能出出现三种情形：
设计符合spec
有violation，并给出反例
逻辑爆炸，无法证明；只能推测n个cycle没有violation
boolean satisfiability
boolean satisfiability，即sat，它可以更快的举出反例。
假设我们有这样的spec和implemenation：
implementation = !(!a&&c || a&&!b)requirement = !a&&!c || b&c
即：
!(!a&&c || a&&!b) -> !a&&!c || b&c
p -> q 等价于 !p || q
(!a&&c || a&&!b) || (!a&&!c || b&&c)
solving the sat problem
对于很多表达式，证明其成立可能比较困难，但找反例则会简单的多。如果我们写成and形式，那只需要有一项为0，则表达式为0.
**conjunctive normal form (cnf) **表达式是写成||形式，各个item或在一起，也称作product-of-sums 。可以将and类比成乘法，or类比成加法。比如下式就是个cnf：
(a||b||!d)&&(!b||c)&&(a||c)
所有的bool逻辑都可以表达成cnf形式。
我们一个或门为例，输入为a,b，输出为c。它的基本逻辑是：
a -> cb -> c!(a||b) -> !c
改写一下：
(!a||c)&&(!b||c)&&(a||b||!c)
我们建立一个真值表，把输入一个个赋值进去，看看是否成立。比如a=0, b= 0, c = 0。但如果变量比较的多的话，算法会指数爆炸。
the davis-putnam sat algorithm
一个个枚举显然不太合理，一个简单的思路是先考虑一个变量，这样就拆分成两个子问题：一个a=0和一个a=1的情形。不断重复这个过程，直到证明或者有违规。
satdivide&conquer(formula)if the formula evaluates to 1{return success!}if the formula evaluates to 0,{return failure, hope another assignment works.}else{split the problem on some variable, v.satdivide&conquer (formula replacing v with 0)satdivide&conquer (formula replacing v with 1)}
最坏的情形是把所有的都遍历一遍，但一般来说不需要。例如对于表达是(a||!b||c) 来说，如果将a赋值成1，整个表达等于1，不需要继续分析了。
一个典型的列子如图13所以
总结：
不要理解成formal是逐个枚举输入变量的值，formal实际上用的数学方法来证明的。
国内首款CAR-T疗法获批上市，先发能否成为最大优势？
阿尔及利亚服务器的介绍，它的特点有哪些
FireflyRK3288的FAQ耳机耳麦介绍
2021年AI和机器学习的发展趋势
华为计划将在下半年发布一款颠覆性的VR终端
Formal学习笔记之算法基础学习
东风风光580一款带有互联网气息的SUV,公认的suv霸主,预售价10.9万
差示扫描量热仪的应用领域
集电环刷过多跟机械摩擦有什么关联
热变形温度和马丁耐热辨析
国内oled龙头企业有哪些?oled显示屏概念股一览
采用DIALOG蓝牙智能芯片，小米手环如虎添翼
华大电子MCU CIU32L061x8存储器（Flash）一
FTTH,FTTH系统结构组成详细介绍
车载式大气走航环境监测站应用解决方案
意法半导体最新推出MasterGaN器件
从摘机电话线获取150mW隔离电源
2019年的补贴退坡进入倒计时 新能源汽车年底现抢购潮
又现AppleWatch救人事件 库克转发并表达心声
嵌入式微控制器应用中的无线更新：设计权衡和经验教训
通常，我们会将spec和设计实现进行比较。spec相对来说比较抽象些，可以是些sva的assertion，rtl model或者一些hvl，比如systemc等。而implemenation通常是rtl代码或者网表。
图1是一个简单的checker，a和b分别表示两种spec，它们接收相同的输入(input)，checker比较二者的输出是否相等。如果找到一个输入序列导致输出比较失败，就是找个了一个反例（counterexample）,工具会将此反例，包括相应的输入记录下来，呈现出来。这个checker其实是个黑盒（black box），因为我们无法观察a和b内部的状态或者信号（白盒white box则可以）。
图1 simple checker
如果a和b足够简单，那我们可以测到所有可能的情形，或者用formal verification来判定二者完全等价。同时，我们也可以借助这个等价来简化一些复杂的的问题，例如图2所示，一个更加复杂的系统，里面包含了a和b。
在这个例子中，因为我们先前已经证明了a等价于b，我们可以做下简化操作，把a和b从系统中拿掉，简化成c和d的比较，如图3所示。当然，c和d的输入(inputs’) 与原始的输入(input)已经有了很大的差别。这种divide and conquer 策略在fv中经常使用，主要用来简化分析大的design。
我们可以把上下方框想象成spec和implementation，这样的比较输入和输入我们可以判定implementation与spec是等价的，设计符合我们的要求。这个一个典型的formal equivalence verification (fev) 。不过，通常spec和implementation不会出现这种理想的等价情况。
cones of influence
如果我们把一些把相干的逻辑分别考量，验证复杂度能大大简化。比如，我们有个硬件，实现加法和乘法运算；在跑simulation的时候，我们可能造不同case侧重不同的点，有点测加法，有的测乘法。如果我们加法和乘法拆分出来，单独验，效率定能大幅提升，但在simulation里面不太现实，因为这需要造几套验证环境。
fv则能比较好的支持这种拆分，fv工具读取property，将设计里面一些与当前property不相关的逻辑移移除掉。这个叫cone of influence 简化。如图4所示，我们只考量result 输出的时候，很多逻辑对这个输出没影响，我们可以把它们简化掉。如果design特别大的话，这种可以极大的简化复杂度。
fv工具也可以支持用户自定义的简化，而非自动简化。例如有个输入，我们可以绑定成某个固定的值。这样逻辑也能大大简化。
bdd
bdd(binary decision tree)，顾名思义，用树形结果来表示电路的逻辑。如果去观察一些电路的真值表如图5，会发现有很多redundancy，很多行都是0。bdd可以表示相同设计的同时，移除一些冗余的逻辑。bdd是一种范式（canonical ），等价设计的bdd是一样的；如果两个电路的bdd一样，那么可以判定二者等价。bdd算法是第一代formal 工具常用的算法。
我们以一个mux为例来说明bdd，如图6所示，一个mux逻辑的bdd算法， xyz为输入，最下面一行为输出。类似于红黑树，每一个分支左侧代表下一输入变量为0，右侧代表输入为1.
我们把输出为0和1的做下merge，如图7所示。
进一步观察，左侧两个z，无论取值如何，输出都是一样，说明父节点y不影响结果。同理，对于观察右侧，z节点多余。于是，我们可以进一步简化成图8这样的。
当然，如果选择变量的顺序不一样，我们得到的bdd的大小会有所不同。如果我们选择z->x->y的顺序的，我们将得到图9这样的bdd。对于一些大的design来说，如果顺序选择不当，可能导致指数爆炸。通常用heuristic-based 算法来寻找最佳的变量顺序。比如根据电路的拓扑结构来，根据变量的相关性来映射。另一种方法是尝试将每一个输入变量替换0或者1，看看哪个精简的程度更大些。
对于大而复杂的设计来说，提取bdd仍然是一件很艰难的工作，或许随着输入的增加而指数级增长。
computing a bdd for a circuit design
如果我们有真值表，我们可以很快速的提取出bdd。但大部分电路，我们没那么容易算出真值表，尤其对rtl而言。庆幸的是，我们将根据基本的逻辑（与、或、非）的bdd组合起来，算出更大设计的bdd。
基本的与或非逻辑的bdd，参见图10所示。
例如，我们以 (x&&y)||z 为例，电路如图11所示。将这些基本门电路组合在一起，就是这个电路的bdd，参见图12.
model checking
model checking 是fv工具分析一段时间内时序逻辑的主要方法。给定properties ，model-checking 会去搜索可能的未来状态，然后判定是否违反这些property。
首先创建初始状态的bdd，然后根据相应的逻辑推导出下一个状态的bdd，不断重复这个过程（reachability ），直到所有的状态都加进来。如果遇到vilation，fv会倒推回去，给出一个反例。
model checker 可能出出现三种情形：
设计符合spec
有violation，并给出反例
逻辑爆炸，无法证明；只能推测n个cycle没有violation
boolean satisfiability
boolean satisfiability，即sat，它可以更快的举出反例。
假设我们有这样的spec和implemenation：
implementation = !(!a&&c || a&&!b)requirement = !a&&!c || b&c
即：
!(!a&&c || a&&!b) -> !a&&!c || b&c
p -> q 等价于 !p || q
(!a&&c || a&&!b) || (!a&&!c || b&&c)
solving the sat problem
对于很多表达式，证明其成立可能比较困难，但找反例则会简单的多。如果我们写成and形式，那只需要有一项为0，则表达式为0.
**conjunctive normal form (cnf) **表达式是写成||形式，各个item或在一起，也称作product-of-sums 。可以将and类比成乘法，or类比成加法。比如下式就是个cnf：
(a||b||!d)&&(!b||c)&&(a||c)
所有的bool逻辑都可以表达成cnf形式。
我们一个或门为例，输入为a,b，输出为c。它的基本逻辑是：
a -> cb -> c!(a||b) -> !c
改写一下：
(!a||c)&&(!b||c)&&(a||b||!c)
我们建立一个真值表，把输入一个个赋值进去，看看是否成立。比如a=0, b= 0, c = 0。但如果变量比较的多的话，算法会指数爆炸。
the davis-putnam sat algorithm
一个个枚举显然不太合理，一个简单的思路是先考虑一个变量，这样就拆分成两个子问题：一个a=0和一个a=1的情形。不断重复这个过程，直到证明或者有违规。
satdivide&conquer(formula)if the formula evaluates to 1{return success!}if the formula evaluates to 0,{return failure, hope another assignment works.}else{split the problem on some variable, v.satdivide&conquer (formula replacing v with 0)satdivide&conquer (formula replacing v with 1)}
最坏的情形是把所有的都遍历一遍，但一般来说不需要。例如对于表达是(a||!b||c) 来说，如果将a赋值成1，整个表达等于1，不需要继续分析了。
一个典型的列子如图13所以
总结：
不要理解成formal是逐个枚举输入变量的值，formal实际上用的数学方法来证明的。
国内首款CAR-T疗法获批上市，先发能否成为最大优势？
阿尔及利亚服务器的介绍，它的特点有哪些
FireflyRK3288的FAQ耳机耳麦介绍
2021年AI和机器学习的发展趋势
华为计划将在下半年发布一款颠覆性的VR终端
Formal学习笔记之算法基础学习
东风风光580一款带有互联网气息的SUV,公认的suv霸主,预售价10.9万
差示扫描量热仪的应用领域
集电环刷过多跟机械摩擦有什么关联
热变形温度和马丁耐热辨析
国内oled龙头企业有哪些?oled显示屏概念股一览
采用DIALOG蓝牙智能芯片，小米手环如虎添翼
华大电子MCU CIU32L061x8存储器（Flash）一
FTTH,FTTH系统结构组成详细介绍
车载式大气走航环境监测站应用解决方案
意法半导体最新推出MasterGaN器件
从摘机电话线获取150mW隔离电源
2019年的补贴退坡进入倒计时 新能源汽车年底现抢购潮
又现AppleWatch救人事件 库克转发并表达心声
嵌入式微控制器应用中的无线更新：设计权衡和经验教训