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