什么是形式验证

wjx197733

现在做集成电路好像不提什么后仿真了。时髦的名词是“形式验证”。不知道这个“形式验证”是什么东西。哪位大哥有相关资料，麻烦共享一下。谢谢了！！！！

老扁

Formal Verification。
由于后仿真对于超大规模设计来说太耗费时间，形式验证就出现了。当确认设计的功能仿真是正确的以后，设计实现的每一个步骤的结果都可以与上个步骤的结果做形式比较，也就是等价检查，如果一致就OK啦，不必进行仿真了。FV主要是进行逻辑形式和功能的一致性比较，是靠工具自己来完成，无需开发测试向量。而且由于实现的每个步骤之间逻辑结构变化都不是很大，所有逻辑的形式比较会非常快。这比仿真的时间要少很多。一般要做FV的步骤有：RTL和RTL，Synthesized Netlist和RTL，P&R后的网表和Synthesized Netlist，等等。跨步骤的结果之间也都可以做FV，很多设计也是这样做的，虽然比较的时间会长一点，但可以节省比较的次数。
就这个专题大家可以充分来补充阐述一下。

hitlzh

如果只做形式验证,那么触发器的建立和保持时间怎么来保证呀?

puffen

FV只保证功能正确，timing的分析是靠STA，FV不能完成timing正确性的分析，他只证明了在timing正确的前提下，功能是正确的，所以STA必须照样进行。举例
Q[n+1] = F( Q[n], x[n] ),此算式表示Q得下一个状态由Q当前状态以及系统输入x决定(可以广义的认为Q,x均为向量，代表所有系统状态，和所有系统输入)。F为一个布尔函数，假定合成后次关系时就变成了另一种形式 Q[n+1] = G( Q[n], x[n] )。
FV只证明了F函数和G函数相等，但是在实际电路上G( Q[n], x[n] )的计算是需要时间的，这个时间必须小于一个系统时钟周期(再加上DFF的setup时间)，而且这个时间必须大于DFF的hold时间。如果这个不满足了那么前面的差分方程就不成立了。
    假定硬件计算G( Q[n], x[n] )要花一个系统时钟多一点（小于两个系而统时钟），
在DFF load新的值实际是：G( Q[n-1], x[n-1] ) {有可能是G( Q[n-1], x[n] )，因为不同路径delay不同，这样更糟糕} 所以在 RTL时关系式是: F( Q[n], x[n] )。
而实际电路为 G( Q[n-1], x[n-1] )， FV只证明了:
    F( Q[n], x[n] ) = G( Q[n], x[n] )
而往往
    F( Q[n], x[n] ) != G( Q[n-1], x[n-1] )
最后结论
    Formal verification和static timing analysis 一个都不能少。

一声叹息

[这个贴子最后由一声叹息在 2004/09/21 09:09am 第 1 次编辑]

下面是Writing Testbenches 1st Edition中关于formal verification的描述：
Formal verifica¬tion does not eliminate the need to write testbenches.
Formal verification is often misunderstood initially. Engineers unfamiliar with the formal verification process often imagine that it is a tool that mathematically determines whether their design is correct, without having to write testbenches. Once you understand what the end points of the formal verification reconvergent paths are, you know what exactly is being verified.
Formal verification falls under two broad categories: equivalence checking and model checking.
Equivalence checking verification process mathematically proves that the origin and output are logically equivalent and that the transformation preserved its functionality.
In its most common use, equivalence checking compares two netlists to ensure that some netlist post-processing, such as scan-chain insertion, clock-tree synthesis, or manual modification1, did not change the functionality of the circuit.
Another popular use is to verify that the netlist correctly imple¬ments the original RTL code. If one trusted the synthesis tool com¬pletely this verification would not be necessary. However, synthesis tools are large software systems that depend on the correctness of algorithms and library information. History has shown that such systems are prone to error. Equivalence checking is used to keep the synthesis tool honest. In some rare instances, this form of equiva¬lence checking is used to verify that manually written RTL code faithfully represents a legacy gate-level design.
Less frequently, equivalence checking is used to verify that two RTL descriptions are logically identical, sometimes to avoid run¬ning lengthy regression simulations when only minor non-func¬tional changes are made to the source code to obtain better synthesis results.
Equivalence checking is a true alternative path to the logic synthe¬sis transformation being verified. It is only interested in comparing boolean and sequential logic functions, not mapping these functions to a specific technology while meeting stringent design constraints.
Model checking is a more recent application of formal verification technology. In it, assertions or characteristics of a design are for¬mally proven or disproved. For example, all state machines in a design could be checked for unreachable or isolated states. A more powerful model checker may be able to determine if deadlock con¬ditions can occur.

老扁

puffen说得很对。
做STA比做带时序的门级仿真要省时省力多啦。

hitlzh

呵呵.没有用过STA工具,不了解,谢谢大家的指点了.

老扁

“formal verifica¬tion does not eliminate the need to write testbenches。”
这句话要理解成：FV必须以做过仿真、通过testbench验证的golden design为基础。
否则单看这一句还以为FV本身也必须writting testbench呢。
不过后续段落还是基本说明白了EC的概念。

prguo

哪些EDA工具能做形式验证？

一声叹息

下面引用由老扁在 2004/09/21 01:14pm 发表的内容：
“formal verifica¬tion does not eliminate the need to write testbenches。”
这句话要理解成：FV必须以做过仿真、通过testbench验证的golden design为基础。
否则单看这一句还以为FV本身也必须writting  ...

那本书主要是将TestBench的。那段话也是讲几种验证方法处理的不同的侧重点的。