SATORI-a fast sequential SAT engine for circuits

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.