Logo des Repositoriums
Zur Startseite
  • English
  • Deutsch
Anmelden
  1. Startseite
  2. SuUB
  3. Forschungsdokumente
  4. RevSCA-2.0: SCA-Based Formal Verification of Nontrivial Multipliers Using Reverse Engineering and Local Vanishing Removal
 
Zitierlink DOI
10.26092/elib/2300
Verlagslink DOI
10.1109/TCAD.2021.3083682

RevSCA-2.0: SCA-Based Formal Verification of Nontrivial Multipliers Using Reverse Engineering and Local Vanishing Removal

Veröffentlichungsdatum
2021-05-25
Autoren
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.
Schlagwörter
Formal verification

; 

Multiplier

; 

Reverse engineering

; 

Symbolic Computer Algebra

; 

Vanishing monomial
Verlag
IEEE
Fachbereich
Fachbereich 03: Mathematik/Informatik (FB 03)  
Dokumenttyp
Artikel/Aufsatz
Zeitschrift/Sammelwerk
IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems  
Band
41
Heft
5
Startseite
1573
Endseite
1586
Zweitveröffentlichung
Ja
Dokumentversion
Postprint
Lizenz
Alle Rechte vorbehalten
Sprache
Englisch
Dateien
Lade...
Vorschaubild
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

Built with DSpace-CRIS software - Extension maintained and optimized by 4Science

  • Datenschutzbestimmungen
  • Endnutzervereinbarung
  • Feedback schicken