This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
2003 International Conference on Computer-Aided Design (ICCAD '03)
SATORI - A Fast Sequential SAT Engine for Circuits
San Jose, CA
November 09-November 13
ISBN: 1-58113-762-1
M. K. Iyer, University of California - Santa Barbara
G. Parthasarathy, University of California - Santa Barbara
K.-T. Cheng, University of California - Santa Barbara
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.
Citation:
M. K. Iyer, G. Parthasarathy, K.-T. Cheng, "SATORI - A Fast Sequential SAT Engine for Circuits," iccad, pp.320, 2003 International Conference on Computer-Aided Design (ICCAD '03), 2003
Usage of this product signifies your acceptance of the Terms of Use.