Formal Verification of Truncated Multipliers Using Algebraic Approach and Re-Synthesis
Tiankai Su, Cunxi Yu, Atif Yasin, Maciej J. Ciesielski · 2017
This paper presents a formal approach to verify multipliers that approximate integer multiplication by output truncation. The method is based on extracting polynomial signature of a truncated multiplier using algebraic rewriting. To efficiently compute the polynomial signature, a multiplier reconstruction approach is used to construct the precise multi- plier from the truncated one. The method consists of three basic steps: 1) determine the weights (binary encoding) of the output bits; 2) reconstruct the truncated multiplier using functional merging and re-synthesis; and 3) construct the polynomial signature of the resulting circuit. The method has been tested on multipliers up to 256 bits with three truncation schemes: Deletion, D-truncation, and Truncation with Rounding. Experimental results are compared with the state-of-the-art SAT, SMT, and computer algebraic solvers.