https://scholars.lib.ntu.edu.tw/handle/123456789/607212
標題: | Deep Integration of Circuit Simulator and SAT Solver | 作者: | Zhang H.-T Jiang J.-H.R Amaru L Mishchenko A Brayton R. JIE-HONG JIANG |
關鍵字: | 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 | 公開日期: | 2021 | 卷: | 2021-December | 起(迄)頁: | 877-882 | 來源出版物: | Proceedings - Design Automation Conference | 摘要: | 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. |
URI: | https://www.scopus.com/inward/record.uri?eid=2-s2.0-85119404819&doi=10.1109%2fDAC18074.2021.9586331&partnerID=40&md5=35314485a2f6f10e964153dfd6af88fd https://scholars.lib.ntu.edu.tw/handle/123456789/607212 |
ISSN: | 0738100X | DOI: | 10.1109/DAC18074.2021.9586331 |
顯示於: | 電機工程學系 |
在 IR 系統中的文件,除了特別指名其著作權條款之外,均受到著作權保護,並且保留所有的權利。