RevSCA-2.0: SCA-Based Formal Verification of Nontrivial Multipliers Using Reverse Engineering and Local Vanishing Removal
Date Issued
2021-05-25
Abstract
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.
Subjects
Formal verification
;
Multiplier
;
Reverse engineering
;
Symbolic Computer Algebra
;
Vanishing monomial
Publisher
IEEE
Type
journal article
Journal/Edited collection
Band
41
Issue
5
Start page
1573
End page
1586
Secondary publication
Yes
Document version
Postprint
License
Alle Rechte vorbehalten
Language
English
File(s)![Thumbnail Image]()
Loading...
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