Divider Verification Using Symbolic Computer Algebra and Delayed Don’t Care Optimization (extended abstract)
Conference: MBMV 2023 – Methoden und Beschreibungssprachen zur Modellierung und Verifikation von Schaltungen und Systemen - 26. Workshop
03/23/2023 - 03/24/2023 at Freiburg
Proceedings: ITG-Fb. 309: MBMV 2023
Pages: 4Language: englishTyp: PDF
Authors:
Konrad, Alexander; Scholl, Christoph (University of Freiburg, Germany)
Mahzoon, Alireza; Drechsler, Rolf (University of Bremen, Germany)
Grosse, Daniel (Johannes Kepler University Linz, Austria)
Abstract:
Recent methods based on Symbolic Computer Algebra (SCA) have shown great success in formal verification of multipliers and – more recently – of dividers as well. Here we give an overview of our work which enhances SCAbased 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). Whereas the basic methods using SCA failed for divider verification, using those novel methods we are able to verify (formally and fully automatically) large gate level implementations of several divider architectures (with bit widths up to 512).