Polynomial word-level verification of arithmetic circuits
Mohammed Barhoush, Alireza Mahzoon, Rolf Drechsler
Abstract
Verifying the functional correctness of a circuit is often the most time-consuming part of the design process. Recently, world-level formal verification methods, e.g., Binary Moment Diagram (BMD) and Symbolic Computer Algebra (SCA) have reported very good results for proving the correctness of arithmetic circuits. However, these techniques still frequently fail due to memory or time requirements. The unknown complexity bounds of these techniques make it impossible to predict before invoking the verification tool whether it will successfully terminate or run for an indefinite amount of time.
Topics & Concepts
CorrectnessComputer scienceFormal verificationArithmeticWord (group theory)Theoretical computer scienceProcess calculusPolynomialAlgorithmProgramming languageMathematicsGeometryMathematical analysisFormal Methods in VerificationVLSI and Analog Circuit TestingEmbedded Systems Design Techniques