结合约束满足消除误判的等价性验证方法

Using constraint satisfaction to eliminate false negative in equivalence checking

通过对集成电路等价性验证方法中消除误判方法的研究,给出一种结合约束满足消除误判的方法。提出消除误判约束关系的概念,当等价性验证可能存在误判现象时,调用约束求解器对消除误判约束关系进行求解,进而消除误判。本方法不用借助其他辅助的数据结构、相应约束关系或启发式策略,极大地降低了等价性验证的复杂度。本方法还适用于不同抽象层次间等价性验证方法中误判的消除,可以消除系统级模型和寄存器传输级等价性验证方法中存在的误判。

The introduction of cut-point is a breakthrough in Formal equivalence checking method.However,the method using cut-point is incomplete and may bring false-negative.Based on the study of false negative elimination in IC equivalence checking,we proposed a false positive elimination method using the constraint satisfaction technique.The concept of false negative elimination constraints was put forward.When the equivalence checking problem possibly runs into false negative,the constraint solver is called to solve the false positive elimination constraints,thus,the false positive is eliminated.The proposed method does not rely on the assistant data structures,the constraints or the heuristic policy.Therefore,the complexity of the equivalence checking is greatly reduced.The method is also applicable to the false negative elimination in the equivalence checking between different Abstraction levels,and between system-level models and register transfer levels.