RevSCA-2.0: SCA-Based Formal Verification of Nontrivial Multipliers Using Reverse Engineering and Local Vanishing Removal
| Autor: | Rolf Drechsler, Daniel Große, Alireza Mahzoon |
|---|---|
| Rok vydání: | 2022 |
| Předmět: |
Reverse engineering
Monomial Computer science Basis (universal algebra) Symbolic computation computer.software_genre Computer Graphics and Computer-Aided Design Set (abstract data type) Algebra ComputingMethodologies_SYMBOLICANDALGEBRAICMANIPULATION Rewriting Electrical and Electronic Engineering computer Formal verification Software Integer (computer science) |
| Zdroj: | IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems. 41:1573-1586 |
| ISSN: | 1937-4151 0278-0070 |
| Popis: | 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 paper introduces the SCA-based approach that combines reverse engineering and local vanishing removal to verify large and non-trivial 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 is demonstrated using an extensive set of multipliers with up to several million gates. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|