Transaction Level Hierarchy Guided and Functional Coverage Driven Deductive Formal Verification

TL;DR

This paper introduces a transaction-level hierarchy approach combined with functional coverage and deductive formal verification, enabling precise, reusable proofs for hardware design verification without relying solely on simulation.

Contribution

It proposes a novel transaction-level hierarchy and an enhanced language PDVL for functional coverage, integrating deductive formal verification with proof reuse capabilities.

Findings

DFV flow compiles PDVL into Coq for proof generation

Functional coverage can be transformed into proof obligations

Reusability of proofs across hierarchy levels demonstrated

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.