D
Data
Text
Transaction-Level Hierarchy Guided Deductive Formal Verification
A hardware verification method that replaces dynamic simulation with deductive formal verification by expressing functional coverage and assertions across a transaction-level (TL) hierarchy in the aspect-oriented PDVL language, compiling that code into Gallina for the Coq theorem prover, treating functional-coverage points as proof obligations whose discharge is equivalent to 100% coverage, and reusing lower-level proofs when verifying higher levels of the TL hierarchy.