原创 后仿真能否被形式验证(Formal Verification)和静态时序分析（Static Timing Analysis）所取代

转自 http://www.cnblogs.com/jyaray/archive/2011/04/26/2029856.html

验证的主要目的：就是检查时间模型是否满足时间要求，是否实现了时间所需的功能。对于集成电路来说，具体就是在时间需求规定的激励下，电路是否产生了符合功能要求的输出；以及在设计需求规定的条件下，电路是否完成正常的功能。

    以RTL级设计为仿真对象的前仿真，主要是验证电路的逻辑功能，信号的跳变是瞬时完成的，因此只能在功能上证明设计的正确性，而无法证明在实际电路中逻辑功能仍然正确。

    门级仿真是对RTL代码综合并布局布线后生成的门级网表进行时序仿真，是引入了逻辑延时时间的仿真。在后仿真阶段，仿真的过程中引入了线上和门级的延时，重点是验证在引入了实际时延之后系统功能是否正确，以避免因时延问题而导致系统时序功能的错误。

    我们知道，当RTL级功能仿真或FPGA验证结束之后，传统的IC设计流程需要完成以下几次门级仿真：综合之后的门级仿真、DFT之后的门级仿真、布局布 线之后的门级仿真等。如果设计很大或者电路很复杂，往往需要庞大的测试向量来验证设计的功能及时序是否正确，这就使得我们花费在门级仿真的时间会随着电路 规模的增大而直线上升。

    那么，可不可以用形式验证(Formal Verification)和静态时序分析（Static Timing Analysis）来代替动态后仿真呢？让我们先简单了解一下形式验证和静态时序分析。

    形式验证是一种静态的验证手段，它根据电路结构静态地判断两个设计在功能上是否等价，常用来判断一个设 计在修改前和修改后其功能是否保持一致。它运行时无须测试向量，但是必须有一个参照设计和一个待验证的设计。参照设计是设计者认为功能上完备无缺的设计， 理论上它可以是用高级语言如C，C++实现的，也可以是用集成电路的建模语言SystemC，但就现实而言，多数形式验证过程中的参照设计就是我们的 RTL设计，一般是用verilog或VHDL实现的。

    静态时序分析简称STA ，它提供了一种针对大规模门级电路进行时序验证的有效方法。它只需要根据电路网表的拓扑，就可以检查电路设计中所有路径的时序特性，测试路径的覆盖率理论 上可以达到100％，从而保证时序验证的完备性；同时由于不需要测试向量，所以STA验证所需时间远小于门级仿真的时间。当然，静态时序分析也有自己的弱 点，它只能有效地验证同步时序电路的正确性，而无法验证电路功能的正确性，对于大部分设计中可能包含的异步电路的时序验证，则必须通过门级仿真来保证其时 序的正确性。

    对于上面的问题，我们的答案是模论两可的。

    其实不是后仿不需要，只是这可能花的时间太多，所以人们想用形式验 证+STA代替。但是这种方法还是有漏洞的，因为STA只检查边沿timing，而形式验证只看register和combination的抽象功能。后 仿在下面三种情况是必要的：异步逻辑设计部分、ATPG向量验证和初始化状态验证。另外，后仿产生的VCD文件还可以做功耗分析。

    现在通常的策略是：采用形式验证手段来保证门级网表在功能上与RTL设计保持一致，配合静态时序分析工具保证门级网表的时序，对于全同步的设计，甚至可以不做门级仿真；对于存在异步电路的设计，也只需要针对异步电路进行极少的门级仍真工作。这无疑会加快设计进度，加快产品上市时间。