RevSCA-2.0: SCA-Based Formal Verification of Nontrivial Multipliers Using Reverse Engineering and Local Vanishing Removal
Datei | Beschreibung | Größe | Format | |
---|---|---|---|---|
Mahzoon-Grosse-Drechsler_RevSCA-2.0_SCA-Based_Formal_Verification_2022_accepted-version_PDF-A-2b.pdf | 2.25 MB | Adobe PDF | Anzeigen |
Autor/Autorin: | Mahzoon, Alireza Große, Daniel Drechsler, Rolf |
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. |
Schlagwort: | Formal verification; Multiplier; Reverse engineering; Symbolic Computer Algebra; Vanishing monomial | Veröffentlichungsdatum: | 25-Mai-2021 | Verlag: | IEEE | Zeitschrift/Sammelwerk: | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems | Heft: | 5 | Startseite: | 1573 | Endseite: | 1586 | Band: | 41 | Dokumenttyp: | Artikel/Aufsatz | ISSN: | 0278-0070 | Zweitveröffentlichung: | yes | Dokumentversion: | Postprint | DOI: | 10.26092/elib/2300 | URN: | urn:nbn:de:gbv:46-elib69796 | Fachbereich: | Fachbereich 03: Mathematik/Informatik (FB 03) |
Enthalten in den Sammlungen: | Forschungsdokumente |
Seitenansichten
113
checked on 27.11.2024
Download(s)
103
checked on 27.11.2024
Google ScholarTM
Prüfe
Alle Ressourcen in diesem Repository sind urheberrechtlich geschützt.