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

• sswlodc-des.ppt · application/vnd.ms-powerpoint · 1021 kbytes

• 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.