Abstract:

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.

Key words: artificial intelligence, integrated circuit, equivalence checking, cut point