In the field of communication system products, most datapath Digital Signal Processing algorithms are initially developed at a high-level in MATLAB® or C/C++. Subsequently, design engineers use these models as a reference for implementing Register Transfer Level designs. The conventional approach to verify their equivalence involves extensive Universal Verification Methodology dynamic simulations, which can last for months and require significant verification efforts. However, some elusive errors might still occur because it is infeasible to explore all input combinations with this method. On the other hand, Formal Equivalence Verification aims to verify that a Register Transfer Level design is functionally equivalent to the reference high-level C/C++ model across all possible legal states. With recent advancements in formal solver technology, Formal Equivalence Verification provides a distinct benefit by using mathematical methods to ensure that the Register Transfer Level (timed) matches the original high-level C/C++ model (untimed). This drastically reduces the verification time and ensures the exhaustive coverage of the design state space. This paper presents an in-depth exploration of complex Finite State Machine with datapath verification, specifically focusing on Multiplier-Accumulator, Tone Generator, and Automatic Gain Control, by employing the formal equivalence methodology. Although these signal processing blocks were previously verified throughout Universal Verification Methodology dynamic simulations, Formal Equivalence Verification was able to identify hard-to-find bugs in just a few weeks by utilizing the new workflow, thereby streamlining the verification process.

A Case Study on Formal Equivalence Verification Between a C/C++ Model and Its RTL Design / Raia, Gaetano; Rigano, Gianluca; Vincenzoni, David; Martina, Maurizio. - ELETTRONICO. - 1:(2024), pp. 373-389. (Intervento presentato al convegno Formal methods tenutosi a Milano (Italy) nel 9-13 September 2024) [10.1007/978-3-031-71177-0_23].

A Case Study on Formal Equivalence Verification Between a C/C++ Model and Its RTL Design

Maurizio Martina
2024

Abstract

In the field of communication system products, most datapath Digital Signal Processing algorithms are initially developed at a high-level in MATLAB® or C/C++. Subsequently, design engineers use these models as a reference for implementing Register Transfer Level designs. The conventional approach to verify their equivalence involves extensive Universal Verification Methodology dynamic simulations, which can last for months and require significant verification efforts. However, some elusive errors might still occur because it is infeasible to explore all input combinations with this method. On the other hand, Formal Equivalence Verification aims to verify that a Register Transfer Level design is functionally equivalent to the reference high-level C/C++ model across all possible legal states. With recent advancements in formal solver technology, Formal Equivalence Verification provides a distinct benefit by using mathematical methods to ensure that the Register Transfer Level (timed) matches the original high-level C/C++ model (untimed). This drastically reduces the verification time and ensures the exhaustive coverage of the design state space. This paper presents an in-depth exploration of complex Finite State Machine with datapath verification, specifically focusing on Multiplier-Accumulator, Tone Generator, and Automatic Gain Control, by employing the formal equivalence methodology. Although these signal processing blocks were previously verified throughout Universal Verification Methodology dynamic simulations, Formal Equivalence Verification was able to identify hard-to-find bugs in just a few weeks by utilizing the new workflow, thereby streamlining the verification process.
2024
978-3-031-71177-0
File in questo prodotto:
File Dimensione Formato  
articolo_raia24.pdf

accesso aperto

Descrizione: versione editoriale
Tipologia: 2a Post-print versione editoriale / Version of Record
Licenza: Creative commons
Dimensione 471.55 kB
Formato Adobe PDF
471.55 kB Adobe PDF Visualizza/Apri
paper_106.pdf

accesso aperto

Descrizione: accepted
Tipologia: 2. Post-print / Author's Accepted Manuscript
Licenza: PUBBLICO - Tutti i diritti riservati
Dimensione 634.93 kB
Formato Adobe PDF
634.93 kB Adobe PDF Visualizza/Apri
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/2992530