Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Standard
Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification. / Kaufmann, Daniela; Beame, Paul; Biere, Armin; Nordstrom, Jakob.
Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022. red. / Cristiana Bolchini; Ingrid Verbauwhede; Ioana Vatajelu. IEEE, 2022. s. 1431-1436.Publikation: Bidrag til bog/antologi/rapport › Konferencebidrag i proceedings › Forskning › fagfællebedømt
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - GEN
T1 - Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification
AU - Kaufmann, Daniela
AU - Beame, Paul
AU - Biere, Armin
AU - Nordstrom, Jakob
N1 - Publisher Copyright: © 2022 EDAA.
PY - 2022
Y1 - 2022
N2 - 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.
AB - 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.
U2 - 10.23919/DATE54114.2022.9774587
DO - 10.23919/DATE54114.2022.9774587
M3 - Article in proceedings
AN - SCOPUS:85130769477
SP - 1431
EP - 1436
BT - Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022
A2 - Bolchini, Cristiana
A2 - Verbauwhede, Ingrid
A2 - Vatajelu, Ioana
PB - IEEE
T2 - 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022
Y2 - 14 March 2022 through 23 March 2022
ER -
ID: 344653290