M-CHECK: A multiple engine combinational equivalence checker

Abstract

Single engine equivalence checkers have been successfully used in efficiently verifying large designs. However, they also showed inefficiency in proving specific types of circuits. New trends tend to combine multiple equivalence checking engines into a single framework, so that they can verify different kinds of designs more efficiently. In this paper, M-CHECK, a multiple engine equivalence checker, is presented. The proposed checker verifies the combinational circuits using three checking engines: Binary Decision Diagram (BDD) engine, Boolean Satisfiability (SAT) engine, and a mixed BDD SAT engine. Also, the tool is capable of iteratively reducing the design through identifying of equivalent node pairs. The results of our methodology are presented on the ISCAS-85 benchmark circuits.