Verifying Dividers Using Symbolic Computer Algebra and Don't Care Optimization
Christoph Scholl, Alexander Konrad, Alireza Mahzoon, Daniel GroBe, Rolf Drechsler
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).
Topics & Concepts
Integer programmingComputer scienceSymbolic computationMultiplier (economics)SatisfiabilityKey (lock)Integer (computer science)Algebra over a fieldArithmeticTheoretical computer scienceProgramming languageAlgorithmMathematicsEconomicsMathematical analysisMacroeconomicsPure mathematicsComputer securityFormal Methods in VerificationNumerical Methods and AlgorithmsVLSI and Analog Circuit Testing