RevSCA-2.0: SCA-Based Formal Verification of Nontrivial Multipliers Using Reverse Engineering and Local Vanishing Removal
Veröffentlichungsdatum
2021-05-25
Zusammenfassung
The formal verification of integer multipliers is one of the important but challenging problems in the verification community. Recently, the methods based on symbolic computer algebra (SCA) have shown very good results in comparison to all other existing proof techniques. However, when it comes to verification of huge and structurally complex multipliers, they completely fail as an explosion happens in the number of monomials. The reason for this explosion is the generation of redundant monomials known as vanishing monomials. This article introduces the SCA-based approach REVSCA-2.0 that combines reverse engineering and local vanishing removal to verify large and nontrivial multipliers. For our approach, we first come up with a theory for the origin of vanishing monomials, i.e., we prove that the gates/nodes where both outputs of half adders (HAs) converge are the origins of vanishing monomials. Then, we propose a dedicated reverse engineering technique to identify atomic blocks including HAs. The identified HAs are the basis for detecting converging cones and locally removing vanishing monomials, which finally results in a vanishing-free global backward rewriting. The efficiency of REVSCA-2.0 is demonstrated using an extensive set of multipliers with up to several million gates.
Schlagwörter
Formal verification
;
Multiplier
;
Reverse engineering
;
Symbolic Computer Algebra
;
Vanishing monomial
Verlag
IEEE
Fachbereich
Dokumenttyp
Artikel/Aufsatz
Zeitschrift/Sammelwerk
Band
41
Heft
5
Startseite
1573
Endseite
1586
Zweitveröffentlichung
Ja
Dokumentversion
Postprint
Lizenz
Sprache
Englisch
Dateien![Vorschaubild]()
Lade...
Name
Mahzoon-Grosse-Drechsler_RevSCA-2.0_SCA-Based_Formal_Verification_2022_accepted-version_PDF-A-2b.pdf
Size
2.19 MB
Format
Adobe PDF
Checksum
(MD5):1714010a4e75fc1943fb9cb9c3836672