Skip to main content

Lund University Publications

LUND UNIVERSITY LIBRARIES

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

Kaufmann, Daniela ; Beame, Paul ; Biere, Armin and Nordstrom, Jakob LU (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:
author
; ; and
organization
publishing date
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}},
}