Improving AMulet2 for verifying multiplier circuits using SAT solving and computer algebra
Abstract: Verifying arithmetic circuits and most prominently multiplier circuits is an important problem which in practice is still considered to be challenging. One of the currently most successful verification techniques relies on algebraic reasoning. In this article, we present AMULET2, a fully automatic tool for verification of integer multipliers combining SAT solving and computer algebra. Our tool models multipliers given as and-inverter graphs as a set of polynomials and applies preprocessing techniques based on elimination theory of Gröbner bases. Finally, it uses a polynomial reduction algorithm to verify the correctness of the given circuit. AMULET2 is a re-factorization and improved re-implementation of our previous verification tool AMULET1 and cannot only be used as a stand-alone tool but also serves as a polynomial reasoning framework. We present a novel XOR-based slicing approach and discuss improvements on the data structures including monomial sharing
- Location
-
Deutsche Nationalbibliothek Frankfurt am Main
- Extent
-
Online-Ressource
- Language
-
Englisch
- Notes
-
ISSN: 1433-2787
- Event
-
Veröffentlichung
- (where)
-
Freiburg
- (who)
-
Universität
- (when)
-
2023
- Creator
- DOI
-
10.1007/s10009-022-00688-6
- URN
-
urn:nbn:de:bsz:25-freidok-2393703
- Rights
-
Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Last update
-
25.03.2025, 1:44 PM CET
Data provider
Deutsche Nationalbibliothek. If you have any questions about the object, please contact the data provider.
Associated
- Kaufmann, Daniela
- Biere, Armin
- Albert-Ludwigs-Universität Freiburg im Breisgau. Lehrstuhl für Rechnerarchitektur
- Universität
Time of origin
- 2023
Other Objects (12)
AMULET 2.0 for verifying multiplier circuits
AMulet 2.0 for Verifying Multiplier Circuits
SAT Solving mit GPU Unterstützung
Advanced Methods for SAT Solving
SAT-Solving mit GPU-Unterstützung
SAT solving with message passing
Symbolic Causality Checking Using SAT-Solving
SAT solving with GPU accelerated inprocessing
Scalable SAT Solving and its Application
SAT Solving with GPU Accelerated Inprocessing
Contributions to the design of multiplier and RF mixer circuits
Certified SAT solving with GPU accelerated inprocessing
AMULET 2.0 for verifying multiplier circuits
AMulet 2.0 for Verifying Multiplier Circuits
SAT Solving mit GPU Unterstützung
Advanced Methods for SAT Solving
SAT-Solving mit GPU-Unterstützung
SAT solving with message passing
Symbolic Causality Checking Using SAT-Solving
SAT solving with GPU accelerated inprocessing
Scalable SAT Solving and its Application
SAT Solving with GPU Accelerated Inprocessing
Contributions to the design of multiplier and RF mixer circuits
Certified SAT solving with GPU accelerated inprocessing
AMULET 2.0 for verifying multiplier circuits
AMulet 2.0 for Verifying Multiplier Circuits
SAT Solving mit GPU Unterstützung
Advanced Methods for SAT Solving
SAT-Solving mit GPU-Unterstützung
SAT solving with message passing
Symbolic Causality Checking Using SAT-Solving
SAT solving with GPU accelerated inprocessing
Scalable SAT Solving and its Application
SAT Solving with GPU Accelerated Inprocessing
Contributions to the design of multiplier and RF mixer circuits