RevSCA: Using Reverse Engineering to Bring Light intoBackward Rewriting for Big and Dirty Multipliers

Alireza Mahzoon, Daniel Große, Rolf Drechsler

In: Design Automation Conference (DAC). Design Automation Conference (DAC-2019) June 2-6 Las Vegas United States 2019.


In recent years, formal methods based on Symbolic Computer Alge-bra (SCA) have shown very good results in verification of integermultipliers. The success is based on removing redundant terms(vanishing monomials) early which allows to avoid the explosionin the number of monomials during backward rewriting. However,the SCA approaches still suffer from two major problems: (1) highdependence on the detection of Half Adders (HAs) realized as AND-XOR gates in the multiplier netlist, and (2) extremely large searchspace for finding the source of the vanishing monomials. As a con-sequence, if the multiplier consists of dirty logic, i.e. for instanceusing non-standard libraries or logic optimization, the existing SCAmethods are completely blind on the resulting polynomials, andtheir techniques for effective division fail.In this paper, we presentRevSCA.RevSCAbrings back lightinto backward rewriting by identifying the atomic blocks of thearithmetic circuits using dedicated reverse engineering techniques.Our approach takes advantage of these atomic blocks to detectall sources of vanishing monomials independent of the design ar-chitecture. Furthermore, it cuts the local vanishing removal timedrastically due to limiting the search space to a small part of thedesign only. Experimental results confirm the efficiency of our ap-proach in verification of a wide variety of integer multipliers withup to 1024 output bits.

German Research Center for Artificial Intelligence
Deutsches Forschungszentrum für Künstliche Intelligenz