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
- Standort
-
Deutsche Nationalbibliothek Frankfurt am Main
- Umfang
-
Online-Ressource
- Sprache
-
Englisch
- Anmerkungen
-
ISSN: 1433-2787
- Ereignis
-
Veröffentlichung
- (wo)
-
Freiburg
- (wer)
-
Universität
- (wann)
-
2023
- Urheber
- Beteiligte Personen und Organisationen
- DOI
-
10.1007/s10009-022-00688-6
- URN
-
urn:nbn:de:bsz:25-freidok-2393703
- Rechteinformation
-
Open Access; Der Zugriff auf das Objekt ist unbeschränkt möglich.
- Letzte Aktualisierung
-
25.03.2025, 13:44 MEZ
Datenpartner
Deutsche Nationalbibliothek. Bei Fragen zum Objekt wenden Sie sich bitte an den Datenpartner.
Beteiligte
- Kaufmann, Daniela
- Biere, Armin
- Albert-Ludwigs-Universität Freiburg im Breisgau. Lehrstuhl für Rechnerarchitektur
- Universität
Entstanden
- 2023
Ähnliche Objekte (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