Efficient SAT-based unbounded symbolic model checking using circuit cofactoring

Malay K. Ganai, Aarti Gupta, Pranav Ashar

Research output: Contribution to journalConference articlepeer-review

68 Scopus citations


We describe an efficient approach for SAT-based quantifier elimination that significantly improves the performance of pre-image and fixed-point computation in SAT-based unbounded symbolic model checking (UMC). The proposed method captures a larger set of new states per SAT-based enumeration step during quantifier elimination, in comparison to previous approaches. The novelty of our approach is in the use of circuit-based cofactoring to capture a large set of states, and in the use of a functional hashing based simplified circuit graph to represent the captured states. We also propose a number of heuristics to further enlarge the state set represented per enumeration, thereby reducing the number of enumeration steps. We have implemented our techniques in a SAT-based UMC framework where we show the effectiveness of SAT-based existential quantification on public benchmarks, and on a number of large industry designs that were hard to model check using purely BDD-based techniques. We show several orders of improvement in time and space using our approach over previous CNF-based approaches. We also present controlled experiments to demonstrate the role of several heuristics proposed in the paper. Importantly, we were able to prove using our method the correctness of a safety property in an industry design that could not be proved using other known approaches.

Original languageEnglish (US)
Pages (from-to)510-517
Number of pages8
JournalIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
StatePublished - 2004
EventICCAD-2004 - IEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers - San Jose, CA, United States
Duration: Nov 7 2004Nov 11 2004

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design


Dive into the research topics of 'Efficient SAT-based unbounded symbolic model checking using circuit cofactoring'. Together they form a unique fingerprint.

Cite this