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则可以)。

SPEC

图1 simple checker

如果A和B足够简单,那我们可以测到所有可能的情形,或者用Formal Verification来判定二者完全等价。同时,我们也可以借助这个等价来简化一些复杂的的问题,例如图2所示,一个更加复杂的系统,里面包含了A和B。

SPEC

在这个例子中,因为我们先前已经证明了A等价于B,我们可以做下简化操作,把A和B从系统中拿掉,简化成C和D的比较,如图3所示。当然,C和D的输入(Inputs’) 与原始的输入(Input)已经有了很大的差别。这种divide and conquer 策略在FV中经常使用,主要用来简化分析大的design。

SPEC

我们可以把上下方框想象成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特别大的话,这种可以极大的简化复杂度。

SPEC

FV工具也可以支持用户自定义的简化,而非自动简化。例如有个输入,我们可以绑定成某个固定的值。这样逻辑也能大大简化。

BDD

BDD(binary decision tree),顾名思义,用树形结果来表示电路的逻辑。如果去观察一些电路的真值表如图5,会发现有很多redundancy,很多行都是0。BDD可以表示相同设计的同时,移除一些冗余的逻辑。BDD是一种范式(canonical ),等价设计的BDD是一样的;如果两个电路的BDD一样,那么可以判定二者等价。BDD算法是第一代Formal 工具常用的算法。

SPEC

我们以一个MUX为例来说明BDD,如图6所示,一个MUX逻辑的BDD算法, xyz为输入,最下面一行为输出。类似于红黑树,每一个分支左侧代表下一输入变量为0,右侧代表输入为1.

SPEC

我们把输出为0和1的做下merge,如图7所示。

SPEC

进一步观察,左侧两个z,无论取值如何,输出都是一样,说明父节点y不影响结果。同理,对于观察右侧,z节点多余。于是,我们可以进一步简化成图8这样的。

SPEC

当然,如果选择变量的顺序不一样,我们得到的BDD的大小会有所不同。如果我们选择z->x->y的顺序的,我们将得到图9这样的BDD。对于一些大的design来说,如果顺序选择不当,可能导致指数爆炸。通常用Heuristic-based 算法来寻找最佳的变量顺序。比如根据电路的拓扑结构来,根据变量的相关性来映射。另一种方法是尝试将每一个输入变量替换0或者1,看看哪个精简的程度更大些。

对于大而复杂的设计来说,提取BDD仍然是一件很艰难的工作,或许随着输入的增加而指数级增长。

SPEC

COMPUTING A BDD FOR A CIRCUIT DESIGN

如果我们有真值表,我们可以很快速的提取出BDD。但大部分电路,我们没那么容易算出真值表,尤其对RTL而言。庆幸的是,我们将根据基本的逻辑(与、或、非)的BDD组合起来,算出更大设计的BDD。

基本的与或非逻辑的BDD,参见图10所示。

SPEC

例如,我们以 (x&&y)||z 为例,电路如图11所示。将这些基本门电路组合在一起,就是这个电路的BDD,参见图12.

SPEC

SPEC

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 -> c
b -> 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所以

SPEC

总结:

不要理解成formal是逐个枚举输入变量的值,formal实际上用的数学方法来证明的。




 

审核编辑:刘清

打开APP阅读更多精彩内容
声明:本文内容及配图由入驻作者撰写或者入驻合作网站授权转载。文章观点仅代表作者本人,不代表电子发烧友网立场。文章及其配图仅供工程师学习之用,如有内容侵权或者其他违规问题,请联系本站处理。 举报投诉

全部0条评论

快来发表一下你的评论吧 !

×
20
完善资料,
赚取积分