FPGA/IC设计入门9-形式验证

形式验证
   形式验证是一种静态的验证手段，它根据电路静态地判断两个设计在功能上是否等价，常用来判断一个设计在修改前和修改后其功能是否保持一致。它运行时无需测试向量，但是必须有一个参照设计和一个待验证的设计。参照设计时设计者认为功能上完备无缺的设计，理论上它可以用高级语言如C，C++实现的，也可以是用集成电路的建模镅詓ystemC，或者验证语言vera或SpecmanE实现的；但是就实现而言，多数形式验证过程中参照设计就是我们的RTL设计，一般用verilog或VHDL实现的。
   当RTL级功能仿真或FPGA验证结束后，传统的IC设计流程需要完成一下几次门级仿真：综合后门级仿真；DFT之后的门级仿真；布局布线之后的门级仿真等，如果设计很大或者电路很复杂，往往需要庞大的测试向量来验证设计的功能及时序是否正确，这就使得我们花费在门级仿真的时间随着电路规模的增直线上升。
   形式验证在ASIC设计流程中犹如一个迭代算法，其最初的输入是RTL设计，每次比较，都将上一次比较后的设计（第n-1次）作为参照设计处理之后的结果（第n次）进行比较，之所以这么做，是基于以下考虑：
1．形式验证工具开始比较前，首先在两个设计中找到一一对应的比较点。
2．如果一个设计改动太大，改变前后的功能是完全一致的，但如果形式验证工具无法找到适合的比较点，也会认为这两个设计不等价
   形式验证在ASIC设计流程中主要应用在以下几个方面：RTL－RTL的对比，RTL－GATE的对比，GATE－GATE的对比。采用形式验证进行RTL与RTL的比较，可以在较短的时间内验证并保证代码修改的过程中没有引入功能性的错误；进行RTL与GATE的对比，是验证源代码与综合之后的门级网表是否等价，以保证综合过程中不会出现任何错误；进行GATE与GATE的对比，主要是发生在验证插入DFT后的电路网表在功能上是否一致；生成时钟树前后的电路网表在功能上是否一致；布局布线前后的电路网表在功能上是否一致等。