SHIVA – A Fast Hybrid Constraint Solver for Circuits

We present a novel hybrid constraint solving framework called SHIVA. Our approach makes efficient use of various levels of circuit abstraction automatically. We target CAD problems, such as formal verification and functional test generation. Our approach seamlessly combines sequential Boolean ATPG, and linear integer arithmetic solving techniques into an efficient solver. We use the strengths of each solver in different algebraic domains of the circuit. We describe the design and implementation of SATORI – a fast sequential justification engine based on state-of-theart SAT and ATPG techniques. 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 show results for SATORI versus a commercial ATPG engine and VIS [4] on ISCAS ’89 and ITC’99 benchmark circuits for an application to assertion checking. SHIVA is still under development and work is proceeding on completing full sequential search using SHIVA. We analyze SHIVA using some example circuits and discuss the results of these experiments.