SATORI-a fast sequential SAT engine for circuits
- 1 January 2003
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
Abstract
We describe the design and implementation of SATORI-a fast sequential justification engine based on state-of-the-art SAT and ATPG techniques. We present several novel techniques that propel SATORI to a demonstrable 10x improvement over a commercial engine. Traditional sequential justification based on ATPG or, on a bounded model of the sequential circuit using SAT, has diverging strengths and weaknesses. In this paper, we contrast these techniques and describe how their-strengths are combined in SATORI. We use conflict-based learning in each time-frame and illegal state learning across time-frames. This enables both combinational and sequential back-jumping. We experimentally analyze the main features of SATORI by comparing SATORI'S performance against a state-of-the-art SAT solver-ZCHAFF using a bounded model, and a commercial sequential ATPG engine performing justification. Additional results are presented for SATORI versus the commercial ATPG engine and VIS on ISCAS '89 and ITC'99 benchmark circuits for an application to assertion checking.Keywords
This publication has 12 references indexed in Scilit:
- SAT and ATPG: Boolean engines for formal hardware verificationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- On the over-specification problem in sequential ATPG algorithmsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Applying SAT Methods in Unbounded Symbolic Model CheckingPublished by Springer Nature ,2002
- IGRAINE-an Implication GRaph-bAsed engINE for fast implication, justification, and propagationIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 2000
- Current directions in automatic test-pattern generationComputer, 1999
- GRASP: a search algorithm for propositional satisfiabilityIEEE Transactions on Computers, 1999
- Model Checking Based on Sequential ATPGPublished by Springer Nature ,1999
- Sequential circuit test generation using dynamic justification equivalenceJournal of Electronic Testing, 1996
- VIS: A system for verification and synthesisLecture Notes in Computer Science, 1996
- A machine program for theorem-provingCommunications of the ACM, 1962