Publikation
Towards Formal Verification of Optimized and Industrial Multipliers
Alireza Mahzoon; Daniel Große; Christoph Scholl; Rolf Drechsler
In: Design, Automation and Test in Europe (DATE). Design, Automation & Test in Europe (DATE-2020), March 9-13, Grenoble, France, 2020.
Zusammenfassung
Formal verification methods have made huge progress over the last decades. However, proving the correctness of arith-metic circuits involving integer multipliers still drives the veri-fication techniques to their limits. Recently, Symbolic Computer Algebra(SCA) methods have shown good results in the verification of both large and non-trivial multipliers. Their success is mainly based on (1) reverse engineering and identifying basic buildingblocks, (2) finding converging gate cones which start from thebasic building blocks and (3) early removal of redundant terms (vanishing monomials) to avoid the blow-up during backward rewriting.Despite these important accomplishments, verifying optimizedand technology-mapped multipliers is an almost unexplored area.This creates major barriers for industrial use as most of thedesigns are area and delay optimized. To overcome the barriers, we propose a novel SCA-method which supports the formal verification of a large variety of optimized multipliers. Our method takes advantage of a dynamic substitution ordering to avoid the monomial explosion during backward rewriting. Experimental results confirm the efficiency of our approach in the verification of a wide range of optimized multipliers including industrial benchmarks.