Linear Algebra Approach to Verification of Modular $(2^{n}-1)$ Multipliers

This paper describes an original approach to formal verification of a special class of modular multipliers, namely modulo <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$(2^{n}-1)$</tex> multipliers, critical components of cryptographic and error correction circuits. The proposed method completely avoids the expensive SAT, symbolic computer algebra, and rewriting techniques, typically used in formal verification of arithmetic circuits. Instead, recognizing a regular structure of such multipliers, constructed as an array of adders, the problem is modeled as a system of linear equations. Each adder is represented by a linear equation with an appropriate and easy to compute weight; the resulting linear system is solved by eliminating the intermediate signals, exposing the direct relation between the primary inputs and outputs. The results obtained for large <tex xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">$(2^{n}-1)$</tex> modular multiplier circuits show several orders of magnitude improvement in CPU time compared to those in the published literature.