标签: 形式验证

      后仿真能否被形式验证(Formal Verification)和静态时序分析（Static Timing Analysis）所取代       验证的主要目的：就是检查时间模型是否满足时间要求，是否实现了时间所需的功能。对于集成电路来说，具体就是在时间需求规定的激励下，电路是否产生了符合功能要求的输出；以及在设计需求规定的条件下，电路是否完成正常的功能。     以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设计保持一致，配合静态时序分析工具保证门级网表的时序，对于全同步的设计，甚至可以不做门级仿真；对于存在异步电路的设计，也只需要针对异步电路进行极少的门级仍真工作。这无疑会加快设计进度，加快产品上市时间。