SATORI

SATORI - A Fast Sequential SAT Engine for Circuits. We describe the design and implementation of SATORI - a fast sequentialjustification engine based on state-of-the-art SAT and ATPG techniques.We present several novel techniques that propel SATORI to ademonstrable 10x improvement over a commercial engine. Traditionalsequential justification based on ATPG or, on a bounded model of thesequential circuit using SAT, has diverging strengths and weaknesses. Inthis paper, we contrast these techniques and describe how their strengthsare combined in SATORI. We use conflict-based learning in each time-frameand illegal state learning across time-frames. This enables bothcombinational and sequential back-jumping. We experimentally analyzethe main features of SATORI by comparing SATORI’s performanceagainst a state-of-the-art SAT solver - ZCHAFF using a boundedmodel, and a commercial sequential ATPG engine performing justification.Additional results are presented for SATORI versus the commercialATPG engine and VIS on ISCAS ý89 and ITC’99 benchmark circuitsfor an application to assertion checking.

This software is also peer reviewed by journal TOMS.

Keywords for this software

Anything in here will be replaced on browsers that support the canvas element


References in zbMATH (referenced in 11 articles )

Showing results 1 to 11 of 11.
Sorted by year (citations)

  1. Safarpour, Sean; Veneris, Andreas; Drechsler, Rolf: Improved SAT-based reachability analysis with observability don’t cares (2009)
  2. Yadgar, Avi; Grumberg, Orna; Schuster, Assaf: Hybrid BDD and All-SAT method for model checking (2009)
  3. Fey, Görschwin; Drechsler, Rolf: Robustness and usability in modern design flows (2008)
  4. Gupta, Aarti; Ganai, Malay K.; Wang, Chao: SAT-based verification methods and applications in hardware verification (2006)
  5. Iyer, Subramanian; Jain, Jawahar; Sahoo, Debashis; Emerson, E.Allen: Under-approximation heuristics for grid-based bounded model checking (2006)
  6. Iyer, Subramanian K.; Jain, Jawahar; Sahoo, Debashis; Emerson, E.Allen: Under-approximation heuristics for grid-based bounded model checking. (2006)
  7. Amla, Nina; Du, Xiaoqun; Kuehlmann, Andreas; Kurshan, Robert P.; McMillan, Kenneth L.: An analysis of sAT-based model checking techniques in an industrial environment (2005)
  8. Iyer, Subramanian K.; Jain, Jawahar; Prasad, Mukul R.; Sahoo, Debashis; Sidle, Thomas: Error detection using BMC in a parallel environment (2005)
  9. Jin, HoonSang; Han, HyoJung; Somenzi, Fabio: Efficient conflict analysis for finding all satisfying assignments of a Boolean circuit (2005)
  10. Prasad, Mukul R.; Biere, Armin; Gupta, Aarti: A survey of recent advances in sat-based formal verification (2005)
  11. Prasad, Mukul R.; Biere, Armin; Gupta, Aarti: A survey of recent advances in SAT-based formal verification (2005)