Design Under Verification
ConceptThe Design Under Verification (DUV) is the hardware or hardware/software implementation whose behavior is being checked by a verification methodology. It is the central artifact evaluated by execution engines in dynamic simulation-based verification and is the implementation to which SystemVerilog Assertions, formal properties, and generated test cases are applied. In processor verification, the DUV is typically an RTL pipeline whose behavior is checked against an architectural-state specification via mapping functions, with consistency assertions and structural queries used to cover interaction effects. Stimuli generation for a DUV must address how many generators to use, the abstraction level at which to generate, online versus offline generation, dynamic versus static generation, and test length.
First seen 5/29/2026
Last seen 7/12/2026
Evidence 15 chunks
Wiki v4
WIKI
Definition
A Design Under Verification (DUV) is the hardware design or circuit (and, in some frameworks, software or mixed hardware/software elements) whose behavior is being checked by a verification methodology. In property-suite and RTL-verification settings, properties describe the DUV's internal-state changes and output behavior for operations such as processor instructions. The DUV may be an RTL implementation checked against formal properties or SystemVerilog Assertions (SVA). [DUV-property-view] [DUV-RTL-impl] [DUV-includes-software]
Goals of Stimuli Generation Against the DUV
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
7 connectionsConsistency assertions provide feedback on the DUV and help ensure correct verification.
Dynamic test generation is fully aware of the state of the DUV and generates based on this information.
The approach generates properties that are checked against the design under verification.
Online generation uses information about the state of the environment and DUV for improving generation quality.
The execution engine runs the generated test case on the design-under-verification.
The state of the DUV is described using the architectural state abstraction.
A computer processor is given as an example of what the design-under-verification could be.
CITATIONS
21 sources21 citations — click to expand
[1] A Design Under Verification is the hardware/software implementation whose behavior is checked by a verification methodology, with properties describing its internal-state changes and output behavior; it may be an RTL implementation checked against formal properties or SVA. Previous wiki article (Design Under Verification v3)
[2] Stimuli generation goals for a DUV include achieving every item in the test-scenarios matrix, ensuring anomalies propagate to checkers, exposing unanticipated bugs, aiding bug recreation, and ensuring nothing breaks over time. Stimuli Generation (Part I) - COMS30026 Design Verification
[3] The PowerPC processor used as a running-example DUV is a RISC design with ~400 instructions, fixed-length 32-bit instructions, 32 GPR and 32 FPR, special-purpose registers, and a complex multi-level translation/coherency memory model. Stimuli Generation (Part I) - COMS30026 Design Verification
[4] Microarchitecturally, the PowerPC DUV is multi-threaded, in-order, four-instructions-wide (Fetch, Decode, Dispatch), with four execution units (Branch, Simple Arithmetic, Complex Arithmetic, Load/Store) and Data Fetch / Execute / Write Back stages. Stimuli Generation (Part I) - COMS30026 Design Verification
[5] Verification plan requirements for a processor DUV include checking all pairs of instructions execute correctly together and that all forwarding mechanisms between pipeline stages work properly. Stimuli Generation (Part I) - COMS30026 Design Verification
[6] Stimuli-generation strategies for a DUV differ by how many generators are used (distributed, single/unified, or synchronized) and at what abstraction level (program/algorithmic, sequence, command-and-data/instruction, or bit level). Stimuli Generation (Part I) - COMS30026 Design Verification
[7] Distributed generators are simple and reusable but cannot easily reach coordinated corner cases; a single unified generator can target common goals across interfaces but is complex and hard to reuse; synchronized generators combine reuse with coordination. Stimuli Generation (Part I) - COMS30026 Design Verification
[8] A typical processor verification environment places instruction, I/O, and memory generators together with corresponding drivers to feed transactions into the DUV's external interfaces. Stimuli Generation (Part I) - COMS30026 Design Verification
[9] Issues in stimuli generation for a DUV include how many generators to use, level of abstraction, online vs. offline generation, dynamic vs. static generation, and test length. Stimuli Generation (Part I) - COMS30026 Design Verification
[10] In dynamic verification, random tests are generated and simulated on the DUV; coverage measures thoroughness of testing and is the prime indicator of test-set quality. Previous wiki article (Design Under Verification v3)
[11] Formal verification of a DUV requires deep knowledge of its internals to write useful assertions, motivating automation. Previous wiki article (Design Under Verification v3)
[12] Interval Property Checking (IPC) checks bounded safety properties of a DUV with SAT-based techniques using arbitrary starting states; a property holding from an arbitrary state also holds from any reachable state. Previous wiki article (Design Under Verification v3)
[13] A complete property suite forms a chain of assume/prove properties covering all input scenarios; any two designs satisfying all properties in a complete suite are formally equivalent. Previous wiki article (Design Under Verification v3)
[14] Architectural-state abstraction for processor DUV verification describes state in terms of programmer-visible registers; mapping functions connect this to the RTL, hiding e.g. pipeline forwarding. Previous wiki article (Design Under Verification v3)
[15] Architecture register R(i) is replaced by Data_R(sfwd, i) during property-suite generation, where sfwd is the forwarding target stage (usually decode); resulting properties use an A ⇒ C implication at successive instruction timepoints. Previous wiki article (Design Under Verification v3)
[16] Consistency assertions are auto-generated alongside instruction properties to cover DUV-wide correctness, including empty-stage behavior and inter-instruction interactions, and provide debugging feedback for architectural mappings. Previous wiki article (Design Under Verification v3)
[17] Test-generator engines accept test templates directed at DUV functions; a template arbitrator selects the next template, and the execution engine runs the test on a simulator or realization of the DUV. Previous wiki article (Design Under Verification v3)
[18] Templates can be weighted, include baseline/unbreakable/sparseness-constrained sections and prologue/epilogue, and support bounded inter-template occurrence constraints to exercise multiple DUV functions in combination. Previous wiki article (Design Under Verification v3)
[19] An abstract knowledge base can hold a formal DUV specification with testing constraints, coverage criteria, and a biasing model toward interesting cases. Previous wiki article (Design Under Verification v3)
[20] Tool-augmented LLM-based SVA generation (ProofLoop) gathers design context via AST-indexed semantic search and JasperGold structural queries, then refines assertions over up to three verification rounds, achieving 93.7% syntax and 82.0% functional correctness on FVEval Design2SVA benchmarks. From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation
[21] Property suites for a DUV can be verified using commercial formal tools supporting SVA verification, IPC and k-induction proof engines, and automatic completeness analysis, applied to industrial processor designs. Previous wiki article (Design Under Verification v3)