Formal Verification Using Don't-Care and Vanishing Polynomials
Cunxi Yu, Maciej J. Ciesielski · 2016
The paper describes a method of verifying sequential arithmetic circuits by adding a special type of redundancy, called “Vanishing Polynomials” and “Don't Care Polynomials”. The proof of functional correctness consists in transforming the polynomial expression at the primary outputs into a unique polynomial in the primary inputs and comparing the computed expression against the expected specification. Experimental results show that the technique is efficient and scalable; for example, a 512-bit serial squarer requiring over 2000 clock cycles was verified in just 330 seconds. The runtime complexity is linear and memory complexity is quadratic in the number of gates.