A Performance Study of BDD-Based Model Checking

	  Bwolen Yang, Randal E. Bryant, David R. O'Hallaron,
	      Armin Biere, Olivier Coudert, Geert Janssen,
		  Rajeev K. Ranjan, and Fabio Somenzi


Abstract:

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.





@INPROCEEDINGS(yang:fmcad98,
    key="bdd study",
    author="Bwolen Yang and Randal E. Bryant and David R. O'Hallaron and
            Armin Biere and Olivier Coudert and Geert Janssen and
	    Rajeev K. Ranjan and Fabio Somenzi",
    Title="A Performance Study of {BDD}-Based Model Checking",
    BookTitle="Proceedings of the Formal Methods on Computer-Aided Design",
    pages="255-289",
    year="1998",
    month="November")