Deep Integration of Circuit Simulator and SAT Solver
Journal
Proceedings - Design Automation Conference
Journal Volume
2021-December
Pages
877-882
Date Issued
2021
Author(s)
Abstract
The 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. The speedup does not lead to a loss in quality because the computed equivalences are canonical. ? 2021 IEEE.
Subjects
Boolean satisfiability
logic synthesis
simulation
Circuit simulation
Codes (symbols)
Integration
Logic Synthesis
Model checking
Timing circuits
Circuit simulators
Deep integrations
Efficient computation
Hardware design
Pre-processing step
SAT instances
Satisfiability solvers
Simulation
State of the art
Computer circuits
Type
conference paper