Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
(2022) 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022 In Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022 p.1431-1436- 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.
Please use this url to cite or link to this publication:
https://lup.lub.lu.se/record/b3479245-4461-44a9-a7b0-22d493dab4ca
- author
- Kaufmann, Daniela ; Beame, Paul ; Biere, Armin and Nordstrom, Jakob LU
- organization
- publishing date
- 2022
- type
- Chapter in Book/Report/Conference proceeding
- publication status
- published
- subject
- host publication
- Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022
- series title
- Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022
- editor
- Bolchini, Cristiana ; Verbauwhede, Ingrid and Vatajelu, Ioana
- pages
- 6 pages
- publisher
- IEEE - Institute of Electrical and Electronics Engineers Inc.
- conference name
- 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022
- conference location
- Virtual, Online, Belgium
- conference dates
- 2022-03-14 - 2022-03-23
- external identifiers
-
- scopus:85130769477
- ISBN
- 9783981926361
- DOI
- 10.23919/DATE54114.2022.9774587
- language
- English
- LU publication?
- yes
- id
- b3479245-4461-44a9-a7b0-22d493dab4ca
- date added to LUP
- 2022-07-15 13:21:44
- date last changed
- 2022-07-15 13:21:44
@inproceedings{b3479245-4461-44a9-a7b0-22d493dab4ca, abstract = {{<p>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.</p>}}, author = {{Kaufmann, Daniela and Beame, Paul and Biere, Armin and Nordstrom, Jakob}}, booktitle = {{Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022}}, editor = {{Bolchini, Cristiana and Verbauwhede, Ingrid and Vatajelu, Ioana}}, isbn = {{9783981926361}}, language = {{eng}}, pages = {{1431--1436}}, publisher = {{IEEE - Institute of Electrical and Electronics Engineers Inc.}}, series = {{Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022}}, title = {{Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification}}, url = {{http://dx.doi.org/10.23919/DATE54114.2022.9774587}}, doi = {{10.23919/DATE54114.2022.9774587}}, year = {{2022}}, }