Alexander Konrad, Christoph Scholl, Alireza Mahzoon, Daniel Große, Rolf Drechsler,
"Divider Verification Using Symbolic Computer Algebra and Delayed Don?t Care Optimization"
: ITG/GI/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV), 2023
Original Titel:
Divider Verification Using Symbolic Computer Algebra and Delayed Don?t Care Optimization
Sprache des Titels:
Englisch
Original Buchtitel:
ITG/GI/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV)
Original Kurzfassung:
Recent methods based on Symbolic Computer Algebra (SCA) have shown great success informal verification of multipliers and ?more recently? of dividers as well. Here we give an overview of our work published in [1?3] which enhances SCA based verification by the computation of satisfiability don?t cares for so-called (Extended) Atomic Blocks(EABs) and by Delayed Don?t Care Optimization (DDCO) for optimizing polynomials during backward rewriting. The optimization is reduced to Integer Linear Programming (ILP). Where as the basic methods using SCA failed for divider verification, using those novel method sweareable to verify (formally and fully automatically) large gate level implementations of several divider architectures (with bit widths up to 512).
Forschungs-