Using constraint satisfaction to eliminate false negative in equivalence checking

作者：Zhang Li Ming; Zeng Hai Lin^*; Zhao Jian; Ouyang Dan Tong; He Li Li

来源：Journal of Jilin University (Engineering and Technology Edition), 2011, 41(5): 1374-1377.

• Abstraction level
• Constraint Satisfaction
• Constraint satisfaction techniques
• Constraint solvers
• Cut point
• Elimination method
• Equivalence checking
• Equivalence-checking problem
• False negatives
• False positive
• Heuristic policies
• Register transfer level
• System-level models

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.

• 出版日期2011