*banner
 

SAT Sweeping with Local Observability Don't-Cares
Nathan Kitchen

Citation
Nathan Kitchen. "SAT Sweeping with Local Observability Don't-Cares". Talk or presentation, 20, March, 2007.

Abstract
SAT sweeping is a method for simplifying an And-Inverter graph by systematically merging graph vertices from the inputs towards the outputs using a combination of structural hashing, simulation, and SAT queries. Due to its robustness and efficiency, SAT sweeping provides a solid algorithm for Boolean reasoning in functional verification and logic synthesis. In previous work, SAT sweeping merges two vertices only if they are functionally equivalent. In this project, we developed a significant extension of the SAT-sweeping algorithm that exploits local observability don't-cares (ODCs) to increase the number of vertices merged. We use a novel technique to bound the use of ODCs and thus the computational effort to find them, while still finding a large fraction of them. Our reported results based on a set of industrial benchmark circuits demonstrate that ODC-based SAT sweeping results in significantly more graph simplification with great benefit for Boolean reasoning with a moderate increase in computational effort. Future work includes testing the effect of the simplification on runtimes of full-blown verification algorithms.

Electronic downloads

Citation formats  
  • HTML
    Nathan Kitchen. <a
    href="http://chess.eecs.berkeley.edu/pubs/270.html"
    ><i>SAT Sweeping with Local Observability
    Don't-Cares</i></a>, Talk or presentation,  20,
    March, 2007.
  • Plain text
    Nathan Kitchen. "SAT Sweeping with Local Observability
    Don't-Cares". Talk or presentation,  20, March, 2007.
  • BibTeX
    @presentation{Kitchen07_SATSweepingWithLocalObservabilityDontCares,
        author = {Nathan Kitchen},
        title = {SAT Sweeping with Local Observability Don't-Cares},
        day = {20},
        month = {March},
        year = {2007},
        abstract = {SAT sweeping is a method for simplifying an
                  And-Inverter graph by systematically merging graph
                  vertices from the inputs towards the outputs using
                  a combination of structural hashing, simulation,
                  and SAT queries. Due to its robustness and
                  efficiency, SAT sweeping provides a solid
                  algorithm for Boolean reasoning in functional
                  verification and logic synthesis. In previous
                  work, SAT sweeping merges two vertices only if
                  they are functionally equivalent. In this project,
                  we developed a significant extension of the
                  SAT-sweeping algorithm that exploits local
                  observability don't-cares (ODCs) to increase the
                  number of vertices merged. We use a novel
                  technique to bound the use of ODCs and thus the
                  computational effort to find them, while still
                  finding a large fraction of them. Our reported
                  results based on a set of industrial benchmark
                  circuits demonstrate that ODC-based SAT sweeping
                  results in significantly more graph simplification
                  with great benefit for Boolean reasoning with a
                  moderate increase in computational effort. Future
                  work includes testing the effect of the
                  simplification on runtimes of full-blown
                  verification algorithms.},
        URL = {http://chess.eecs.berkeley.edu/pubs/270.html}
    }
    

Posted by Christopher Brooks on 29 May 2007.
Groups: chess
For additional information, see the Publications FAQ or contact webmaster at chess eecs berkeley edu.

Notice: This material is presented to ensure timely dissemination of scholarly and technical work. Copyright and all rights therein are retained by authors or by other copyright holders. All persons copying this information are expected to adhere to the terms and constraints invoked by each author's copyright.

You are not logged in 
©2002-2014 Chess