Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

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. ed. / Cristiana Bolchini; Ingrid Verbauwhede; Ioana Vatajelu. IEEE, 2022. p. 1431-1436.

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-review

Harvard

Kaufmann, D, Beame, P, Biere, A & Nordstrom, J 2022, Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification. in C Bolchini, I Verbauwhede & I Vatajelu (eds), Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022. IEEE, pp. 1431-1436, 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022, Virtual, Online, Belgium, 14/03/2022. https://doi.org/10.23919/DATE54114.2022.9774587

APA

Kaufmann, D., Beame, P., Biere, A., & Nordstrom, J. (2022). Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification. In C. Bolchini, I. Verbauwhede, & I. Vatajelu (Eds.), Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022 (pp. 1431-1436). IEEE. https://doi.org/10.23919/DATE54114.2022.9774587

Vancouver

Kaufmann D, Beame P, Biere A, Nordstrom J. Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification. In Bolchini C, Verbauwhede I, Vatajelu I, editors, Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022. IEEE. 2022. p. 1431-1436 https://doi.org/10.23919/DATE54114.2022.9774587

Author

Kaufmann, Daniela ; Beame, Paul ; Biere, Armin ; Nordstrom, Jakob. / Adding Dual Variables to Algebraic Reasoning for Gate-Level Multiplier Verification. Proceedings of the 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022. editor / Cristiana Bolchini ; Ingrid Verbauwhede ; Ioana Vatajelu. IEEE, 2022. pp. 1431-1436

Bibtex

@inproceedings{c1b37a0a7ccf4989b71961a4b057dd78,
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",
note = "Publisher Copyright: {\textcopyright} 2022 EDAA.; 2022 Design, Automation and Test in Europe Conference and Exhibition, DATE 2022 ; Conference date: 14-03-2022 Through 23-03-2022",
year = "2022",
doi = "10.23919/DATE54114.2022.9774587",
language = "English",
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",
publisher = "IEEE",

}

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