Using SAT for combinational equivalence checking

This paper addresses the problem of combinational equivalence checking (CEC) which forms one of the key componentsof the current verification methodology for dig- ital systems. A number of recently proposed BDD based approaches have met with considerable success in this area. However, the growing gap between the capability of current solvers and the complexity of verification instances neces- sitates the exploration of alternative, better solutions. This paper revisits the application of Satisfiability (SAT) algo- rithms to the combinational equivalence checking (CEC) problem. We argue that SAT is a more robust and fle xi- ble engine of Boolean reasoning for the CEC application than BDDs, which have traditionally been the method of choice. Preliminary results on a simple framework for SAT based CEC show a speedup of up to two orders of mag- nitude compared to state-of-the-art SAT based methods for CEC and also demonstrate that even with this simple algo- rithm and untuned prototype implementationit is only mod- erately slower and sometimes faster than a state-of-the-art BDD based mixed engine commercial CEC tool. While SAT based CEC methods need further research and tuning be- fore they can surpass almost a decade of research in BDD based CEC, the recent progress is very promising and mer- its continued research.