Combining Decision Diagrams and SAT Procedures for Efficient Symbolic Model Checking

Poul Frederick Williams, Armin Biere, Edmund M. Clarke, Anubhav Gupta

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

    Abstract

    In this paper we show how to do symbolic model checking using Boolean Expression Diagrams (BEDs), a non-canonical representation for Boolean formulas, instead of Binary Decision Diagrams (BDDs), the traditionally used canonical representation. The method is based on standard fixed point algorithms, combined with BDDs and SAT-solvers to perform satisfiability checking. As a result we are able to model check systems for which standard BDD-based methods fail. For example, we model check a liveness property of a 256 bit shift-and-add multiplier and we are able to find a previously undetected bug in the specification of a 16 bit multiplier. As opposed to Bounded Model Checking (BMC) our method is complete in practice. Our technique is based on a quantification procedure that allows us to eliminate quantifiers in Quantified Boolean Formulas (QBF). The basic step of this procedure is the up-one operation for BEDs. In addition we list a number of important optimizations to reduce the number of basic steps. In particular the optimization rule of quantification-by-substitution turned out to be very useful: exists x : {g /\ ( x f )} = g[f/x]. The rule is used (1) during fixed point iterations, (2) for deciding whether an initial set of states is a subset of another set of states, and finally (3) for iterative squaring.
    Original languageEnglish
    Title of host publicationLecture Notes in Computer Science1855
    PublisherSpringer Verlag
    Publication date2000
    Publication statusPublished - 2000
    EventInt. Conference on Computer Aided Verification - Chicago, USA
    Duration: 1 Jan 2000 → …

    Conference

    ConferenceInt. Conference on Computer Aided Verification
    CityChicago, USA
    Period01/01/2000 → …

    Cite this