Abstract
Algebraic reasoning has proven to be one of the most effective approaches for verifying gate-level integer mul-tipliers, but it struggles with certain components, necessitating the complementary use of SAT solvers. For this reason validation certificates require proofs in two different formats. Approaches to unify the certificates are not scalable, meaning that the validation results can only be trusted up to the correctness of compositional reasoning. We show in this paper that using dual variables in the algebraic encoding, together with a novel tail substitution and carry rewriting method, removes the need for SAT solvers in the verification flow and yields a single, uniform proof certificate.
Originalsprog | Engelsk |
---|---|
Titel | Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022 |
Redaktører | Cristiana Bolchini, Ingrid Verbauwhede, Ioana Vatajelu |
Antal sider | 6 |
Forlag | IEEE |
Publikationsdato | 2022 |
Sider | 1431-1436 |
ISBN (Elektronisk) | 9783981926361 |
DOI | |
Status | Udgivet - 2022 |
Begivenhed | 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022 - Virtual, Online, Belgien Varighed: 14 mar. 2022 → 23 mar. 2022 |
Konference
Konference | 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022 |
---|---|
Land/Område | Belgien |
By | Virtual, Online |
Periode | 14/03/2022 → 23/03/2022 |
Sponsor | Cadence, CEA, et al., HIPEAC, IEEE Council on Electronic Design Automation (CEDA), NanoElec |
Bibliografisk note
Funding Information:D. Kaufmann and A. Biere were supported by the LIT AI Lab funded by the state of Upper Austria. J. Nordström was supported by the Swedish Research Council grant 2016-00782 and the Independent Research Fund Denmark grant 9040-00389B. P. Beame was supported by NSF-SHF grant CCF-1714593.
Publisher Copyright:
© 2022 EDAA.