Verifying Dividers Using Symbolic Computer Algebra and Don't Care Optimization

Christoph Scholl, Alexander Konrad, Alireza Mahzoon, Daniel Große, Rolf Drechsler

In: Design, Automation and Test in Europe Conference (DATE). Design, Automation & Test in Europe (DATE-2021) February 1-5 Grenoble France 2021.


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).

Deutsches Forschungszentrum für Künstliche Intelligenz
German Research Center for Artificial Intelligence