Verifying Dividers using Symbolic Computer Algebra and Don’t Care Optimization
Christoph Scholl1,a, Alexander Konrad1,b, Alireza Mahzoon2,a, Daniel Große3 and Rolf Drechsler2,b
1University of Freiburg, Germany
ascholl@informatik.uni-freiburg.de
bkonrada@informatik.uni-freiburg.de
2University of Bremen, Germany
afmahzoon@informatik.uni-bremen.de
bdrechsle@informatik.uni-bremen.de
3Johannes Kepler University Linz, Austria
daniel.grosse@jku.at
ABSTRACT
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).
