A performance study of BDD-based model checking

B. Yang, R.E. Bryant, D.R. O Hallaron, A. Biere, O. Coudert, G.L.J.M. Janssen, R.K. Ranjan, F. Somenzi

Research output: Chapter in Book/Report/Conference proceedingChapterAcademicpeer-review

45 Citations (Scopus)
138 Downloads (Pure)


We present a study of the computational aspects of model checking based on binary decision diagrams (BDDs). By using a trace-based evaluation framework, we are able to generate realistic benchmarks and perform this evaluation collaboratively across several different BDD packages. This collaboration has resulted in significant performance improvements and in the discovery of several interesting characteristics of model checking computations. One of the main conclusions of this work is that the BDD computations in model checking and in building BDDs for the outputs of combinational circuits have fundamentally different performance characteristics. The systematic evaluation has also uncovered several open issues that suggest new research directions. We hope that the evaluation methodology used in this study will help lay the foundation for future evaluation of BDD-based algorithms.
Original languageEnglish
Title of host publicationFMCAD : formal methods in computer-aided design : international conference : proceedings, 2nd, Palo Alto, CA, USA, November 4-6, 1998
EditorsG. Gopalakrishnan, P. Windley
Place of PublicationBerlin
Number of pages35
ISBN (Print)3-540-65191-8
Publication statusPublished - 1998

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Dive into the research topics of 'A performance study of BDD-based model checking'. Together they form a unique fingerprint.

Cite this