Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Transaction Level Hierarchy Guided and Functional Coverage Driven Deductive Formal Verification

Tobias Strauch

TL;DR

The paper addresses the scalability challenges of functional coverage and assertion verification in complex SoCs by replacing dynamic verification with a deductive formal verification flow. It introduces a transaction-level hierarchy built on PDVL, centered on virtual transactions (VTRs), and a DFV pipeline that compiles PDVL to Gallina for Coq-based proofs, enabling cross-level proof reuse. The key contributions include PDVL language extensions for FC and assertions, a TL-hierarchy framework, a PDVL-to-Gallina compiler (MRPHS), and demonstration of proof reuse across TL levels, along with maintaining compatibility with SVA-based ABV. The work shows practical feasibility through a PDVL-based SoC case study, highlighting stronger system-level verification capabilities and potential efficiency gains via proof reuse and parallelized theorem proving.

Abstract

We demonstrate how dynamic verification (e.g. simulation) can be replaced by deductive formal verification and how to benefit from the advantages of symbolic verification and the reuse of verification proofs. To do this, we swap the well-known module-hierarchy based concept with a transaction-level (TL) based alternative, which still allows us to describe the design as precisely as on RTL. We enhance the aspect-oriented and TL oriented language PDVL to support the definition of functional coverage (FC) and assertions at all levels of a TL-hierarchy. We then show how to use a deductive formal verification (DFV) flow which compiles PDVL code into Gallina code to be used by the Coq theorem prover. It can be argued that FC can be converted into proof obligations and that proving them is equivalent to 100\% coverage. We also demonstrate how lower-level proofs can be reused when verifying aspects at higher-levels of a TL-hierarchy. We argue that the traditional assertion-based verification (ABV) methodology is still supported and SVA can be proven using DFV.

Transaction Level Hierarchy Guided and Functional Coverage Driven Deductive Formal Verification

TL;DR

The paper addresses the scalability challenges of functional coverage and assertion verification in complex SoCs by replacing dynamic verification with a deductive formal verification flow. It introduces a transaction-level hierarchy built on PDVL, centered on virtual transactions (VTRs), and a DFV pipeline that compiles PDVL to Gallina for Coq-based proofs, enabling cross-level proof reuse. The key contributions include PDVL language extensions for FC and assertions, a TL-hierarchy framework, a PDVL-to-Gallina compiler (MRPHS), and demonstration of proof reuse across TL levels, along with maintaining compatibility with SVA-based ABV. The work shows practical feasibility through a PDVL-based SoC case study, highlighting stronger system-level verification capabilities and potential efficiency gains via proof reuse and parallelized theorem proving.

Abstract

We demonstrate how dynamic verification (e.g. simulation) can be replaced by deductive formal verification and how to benefit from the advantages of symbolic verification and the reuse of verification proofs. To do this, we swap the well-known module-hierarchy based concept with a transaction-level (TL) based alternative, which still allows us to describe the design as precisely as on RTL. We enhance the aspect-oriented and TL oriented language PDVL to support the definition of functional coverage (FC) and assertions at all levels of a TL-hierarchy. We then show how to use a deductive formal verification (DFV) flow which compiles PDVL code into Gallina code to be used by the Coq theorem prover. It can be argued that FC can be converted into proof obligations and that proving them is equivalent to 100\% coverage. We also demonstrate how lower-level proofs can be reused when verifying aspects at higher-levels of a TL-hierarchy. We argue that the traditional assertion-based verification (ABV) methodology is still supported and SVA can be proven using DFV.
Paper Structure (26 sections, 2 figures, 1 table, 9 algorithms)

This paper contains 26 sections, 2 figures, 1 table, 9 algorithms.

Table of Contents

  1. Introduction
  2. Functional coverage and assertions
  3. Our work
  4. Adding relevant language constructs to PDVL
  5. Defining FC and assertions from lower-level up to system-level
  6. Verifying FC and assertions from lower-level up to system-level
  7. Using lower-level assertion definition and associated coverage
  8. Proof by symbolic simulation
  9. PDVL
  10. PDVL to Gallina compiler
  11. TL-hierarchy guided coverage driven DFV
  12. Introducing virtual transactions
  13. VTRs and testbench related language constructs
  14. VTRs as instruction code generator
  15. VTRs and coverage related constructs
  16. ...and 11 more sections

Figures (2)

  • Figure 1: Comparing status quo and transaction-level-hierarchy guided and functional coverage driven deductive formal verification.
  • Figure 2: Transaction level hierarchy example, showing the design under verification (DUV) and transactions as well as the testbench (TB) and virtual transactions.