Deep Integration of Circuit Simulator and SAT Solver
TimeWednesday, December 8th4:50pm - 5:10pm PST Event Type
RTL/Logic Level and High-level Synthesis
DescriptionThe paper addresses a key aspect of efficient computation in logic synthesis and formal verification, namely, the integration of a circuit simulator and a Boolean satisfiability solver. A novel way of interfacing these is proposed along with a fast preprocessing step to detect easy SAT instances and a new hybrid SAT solver, which is more robust for hardware designs than are state-of-the-art CNF-based solvers. The proposed integration enables a 10x speedup in essential computation engines widely used in industrial EDA tools, including SAT sweeping, combinational and sequential equivalence checking, and computing structural choices for technology mapping.