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

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

【50份好礼】首发直播：解密Keysight最新模拟信号源 如何应对供应风险和挑战，在行业竞争中赢得先机？

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比做带时序的门级仿真要省时省力多啦。

形式验证工具：

Synopsys的Formality比较流行；

Cadence LEC(Logic Equivalence Check)

国产EDA公司也纷纷推出了一些形式验证的工具

登录阅读全文



免责声明：该内容由专栏作者授权发布或作者转载，目的在于传递更多信息，并不代表本网赞同其观点，本站亦不保证或承诺内容真实性等。若内容或图片侵犯您的权益，请及时联系本站删除。侵权投诉联系： nick.zong@aspencore.com！

路科验证专注于数字芯片验证的系统思想和前沿工程领域。路桑是Intel资深验证专家，主持验证架构规划和方法学研究，担任过亿门级通信芯片的验证经理角色。在工程领域之外，他在西安电子科技大学和西安交通大学客座讲授芯片验证课程。著有书籍《芯片验证漫游指南》。

进入专栏

文章：1048篇粉丝：51人

 私信

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

最近文章

热门文章

推荐

最新资讯