Zhang H.-TJiang J.-H.RAmaru LMishchenko ABrayton R.JIE-HONG JIANG2022-04-252022-04-2520210738100Xhttps://www.scopus.com/inward/record.uri?eid=2-s2.0-85119404819&doi=10.1109%2fDAC18074.2021.9586331&partnerID=40&md5=35314485a2f6f10e964153dfd6af88fdhttps://scholars.lib.ntu.edu.tw/handle/123456789/607212The 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.Boolean satisfiabilitylogic synthesissimulationCircuit simulationCodes (symbols)IntegrationLogic SynthesisModel checkingTiming circuitsCircuit simulatorsDeep integrationsEfficient computationHardware designPre-processing stepSAT instancesSatisfiability solversSimulationState of the artComputer circuitsconference paper10.1109/DAC18074.2021.95863312-s2.0-85119404819