Publikation
Transformation-Aided Verification of MAC Designs using Symbolic Computer Algebra
Lennart Weingarten; Kamalika Datta; Rolf Drechsler
In: Design and Verification Conference & Exhibition Europe (DVCon Europe). Design and Verification Conference Europe (DVCon Europe), October 14-15, München, Germany, 2025.
Zusammenfassung
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.