@inproceedings{b3479245446144a9a7b022d493dab4ca,
title = "Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification",
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.",
author = "Daniela Kaufmann and Paul Beame and Armin Biere and Jakob Nordstrom",
year = "2022",
doi = "10.23919/DATE54114.2022.9774587",
language = "English",
series = "Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022",
publisher = "IEEE - Institute of Electrical and Electronics Engineers Inc.",
pages = "1431--1436",
editor = "Cristiana Bolchini and Ingrid Verbauwhede and Ioana Vatajelu",
booktitle = "Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022",
address = "United States",
note = "2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022 ; Conference date: 14-03-2022 Through 23-03-2022",
}