AMulet 2.0 for Verifying Multiplier Circuits
Daniela Kaufmann, Armin Biere
Abstract
Abstract AMulet 2.0 is a fully automatic tool for the verification of integer multipliers using computer algebra. Our tool models multiplier circuits given as and-inverter graphs as a set of polynomials and applies preprocessing techniques based on elimination theory of Gröbner bases. Finally it uses a polynomial reduction algorithm to verify the correctness of the given circuit. AMulet 2.0 is a re-factorization and improved re-implementation of our previous multiplier verification tool AMulet 1.0 .
Topics & Concepts
CorrectnessMultiplier (economics)PreprocessorComputer scienceFactorizationAlgorithmArithmeticPolynomialMathematicsAlgebra over a fieldProgramming languagePure mathematicsMacroeconomicsMathematical analysisEconomicsFormal Methods in VerificationNumerical Methods and AlgorithmsLow-power high-performance VLSI design