Dynamic Variable Ordering during Algebraic Backward Rewriting for Formal Verification of Multipliers

Recently, many efforts have been made to verify the multiplier circuits using Symbolic Computer Algebra (SCA) techniques. One important SCA technique is Algebraic Backward Rewriting, using which one can deduce the input specification of a multiplier circuit from known output specification. Although the resulting input specification has a smaller number of monomials, the intermediate monomials may explode due to the complexity of circuits. However, state-of-the-art tools use adder tree detection techniques to overcome the monomial explosion problem. The adder tree detection technique is limited to the circuit structure and does not work for algebraic unfriendly multipliers. This paper proposes and implements a fanout-free-based xor detection, level promotion, and order selection method to overcome such challenges. We have reduced the internal monomials up to 24.86% and verified up to 512 - bits array multiplier circuits using our unique method.