Transformation-Aided Verification of MAC Designs using Symbolic Computer Algebra

Abstract:
The increasing complexity of modern digital circuits requires robust verification to ensure reliability and prevent costly failures. Among various formal verification methods, Symbolic Computer Algebra (SCA) offers a powerful approach by representing circuits using polynomials. However, a significant challenge in SCA verification is the exponential term expansion during substitution, which drastically increases verification time. This paper addresses this challenge by investigating the impact of circuit transformations on SCA verification efficiency. We propose a transformation-aided verification process, showcasing its effectiveness through a case study on Multiply-and-Accumulate MAC-based designs. Specifically, we examine the transformation of NAND/NOR-based designs and demonstrate its substantial impact on verification time for certain MAC circuits. Experimental results reveal interesting findings, notably a many-fold performance gain for some benchmarks.