Divider Verification Using Symbolic Computer Algebra and Delayed Don?t Care Optimization
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
ITG/GI/GMM-Workshop Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen (MBMV)
Sprache des Tagungstitel:
Englisch
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-