Polynomial Formal Verification of Structurally Simple Multipliers

Abstract

Formal verification of integer multipliers remains a challenging problem in electronic design automation, as logic-based approaches such as Satisfiability Solvers (SAT) and Binary Decision Diagrams (BDDs) often scale poorly on such circuitry. In recent times, Polynomial Formal Verification (PFV) has been investigated for efficient verification. While polynomial space and time complexities have been demonstrated for various arithmetic circuits, no such bounds have been established for multiplier verification using Symbolic Computer Algebra (SCA). This paper identifies a class of structural multipliers, termed as Structurally Simple Multiplier (SSM), for which SCA exploiting backward rewriting admits provable linear complexity for the first time, to the best of our knowledge. This class covers standard multipliers and compressor networks built from weight-preserving adders. We prove that rewriting these at the atomic block level maintains weight-respecting linearity, ensuring verification remains linear in time and space. For netlists, these blocks are detectable in linear time via structural AIG encoding. These results provide explicit conditions under which SCA-based verification of multipliers is guaranteed to remain tractable. Experimental results validate our theoretical bound and outperform state-of-the-art methods in both execution time and memory efficiency.