Verifying Dividers Using Symbolic Computer Algebra and Don?t Care Optimization
Sprache des Titels:
Design, Automation and Test in Europe (DATE)
In this paper we build on methods based on Symbolic
Computer Algebra that have been applied successfully to multiplier verification and more recently to divider verification as well. We show that existing methods are not sufficient to verify optimized non-restoring dividers and we enhance those methods by a novel optimization method for polynomials w. r. t. satisfiability don?t cares. The optimization is reduced to Integer Linear Programming (ILP).
Our experimental results show that this method is the key for
enabling the verification of large and optimized non-restoring dividers (with bit widths up to 512).