时序电路的等价验证方法

随着集成电路设计水平的进步，电路规模日益增大，电路设计的时间越米越多的耗费在电路的验证问题上。传统的基于模拟的验证逐渐不能满足验证的需要，形式验证方法作为传统模拟验证方法的补充成为研究的热点。等价验证可以分为组合电路的等价验证和时序电路的等价验证。组合电路的等价验证算法目前发展比较成熟，成为很多时序电路验证算法的基础。本文的研究工作主要集中在时序电路的等价验证部分，由两部分组成： 第一部分是时序电路等价验证的研究。时序电路的等价验证通常使用的方法都是对有限状态机进行遍历，利用电路中的组合部分，或是展开成时间帧的形式加以验证，或是利用结构中的相似性用固定点迭代的方式进行验证，或是化作布尔表达式用可满足性问题的算法进行验证。本文的算法将时序电路的时序行为用状态转换图的形式来表示，对待验证电路的状态转化图进行同构验证，从而验证两电路是否等价。主要的创新处在于：1.不依赖于电路结构的相似性，可以验证结构不同，寄存器数目不同的电路；2.采用图的方式表示时序电路的行为，而不依赖于状态编码或者是布尔表达式：3.速度优于传统的基于BDD的状态遍历法以及结构不动点法。 第二部分是FPGA中电路等价验证的研究。针对FPGA流程的工艺映射流程、和装箱流程展开验证。对于经过工艺映射的由LUT(look up table)组成的电路和原始的gate_level的电路进行等价验证，以及对于经过装箱的由cluster组成的电路和LUT组成的电路进行等价验证。采用寄存器匹配的方法将时序电路转化为组合电路后，用C-SAT算法进行验证。

点击标签浏览更多相关技术资料资源：