【FormalVerification形式验证】小知识分享

路科验证 2022-06-17 12:06

TI MCU方案：能源基础设施实时控制 如何增强电动汽车的实时控制能力？

Formal Verification（形式验证)

当确认设计的功能验证仿真没有问题以后，后面的Flow设计实现的每一个步骤的结果都可以与上个步骤的结果做形式比较，也就是等价检查，如果检查结果一致就表示通过啦。

FV（Formal Verification）主要是进行逻辑形式和功能的一致性比较，是靠工具自己来完成，无需开发测试向量，所以对于工程师而言，只需要掌握软件的操作用法就够了，无需额外的知识去掌握，但对于EDA软件开发而言，就比较有挑战了。另一方面，由于实现的每个步骤之间逻辑结构变化都不是很大，所有逻辑的形式验证比较会非常快。这比做仿真的时间要少很多。

一般要做FV的步骤有：RTL和RTL， Synthesized Netlist和RTL，P&R后的网表和Synthesized Netlist，等等。跨步骤的结果之间也都可以做FV，很多设计也是这样做的，虽然比较的时间会长一点，但可以节省比较的次数。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 一个都不能少。做STA比做带时序的门级仿真要省时省力多啦。