San Jose, CA, USA
Nov. 9, 2003 to Nov. 13, 2003
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.
M. K. Iyer, G. Parthasarathy, K.-T. Cheng, "SATORI - A Fast Sequential SAT Engine for Circuits", ICCAD, 2003, ICCAD-2003. International Conference on Computer Aided Design, ICCAD-2003. International Conference on Computer Aided Design 2003, pp. 320, doi:10.1109/ICCAD.2003.1257731