Design Under Verification
ConceptA Design Under Verification (DUV) is the hardware design or circuit whose behavior is checked by a formal or assertion-based verification methodology. Verification of the DUV requires deep knowledge of its internal structure and signals, and is supported by complementary techniques such as automatic property generation and consistency assertions.
First seen 5/29/2026
Last seen 6/8/2026
Evidence 5 chunks
Wiki v2
WIKI
Definition
A Design Under Verification (DUV) is the hardware design or circuit 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]
Knowledge Requirements
NEIGHBORHOOD
No graph connections found for this entity yet. It may appear in future ingestion runs.
explore full graph →RELATIONSHIPS
3 connectionsThe approach generates properties that are checked against the design under verification.
Consistency assertions provide feedback on the DUV and help ensure correct verification.
The state of the DUV is described using the architectural state abstraction.
CITATIONS
14 sources14 citations — click to expand
[1] A Design Under Verification is the hardware design or circuit whose behavior is being checked by a verification methodology, such as an RTL implementation checked against formal properties or SystemVerilog Assertions. Automated Formal Verification of Processors Based on Architectural Models
[2] Formal verification requires a deep knowledge of the internals of the design under verification in order to write assertions, motivating automation for well-defined circuit classes. Automated Formal Verification of Processors Based on Architectural Models
[3] Interval Property Checking (IPC) checks bounded safety properties with SAT-based techniques using arbitrary starting states, and counterexamples from unreachable states can be handled by adding invariants. Automated Formal Verification of Processors Based on Architectural Models
[4] A complete property suite covers every possible input scenario with a chain of properties predicting states and outputs; any two designs fulfilling all properties of a complete suite are formally equivalent. Automated Formal Verification of Processors Based on Architectural Models
[5] The equivalence of the property suite and the DUV is established by chaining generated properties, each consisting of an assume part (A) and a prove part (C), hooked up at the timepoint when the processor is ready to execute the next instruction. Automated Formal Verification of Processors Based on Architectural Models
[6] Completeness analysis checks (1) that a successor property with matching assumptions exists, (2) that the successor property is uniquely determined, and (3) that each property describes the outputs and states of the design uniquely. Automated Formal Verification of Processors Based on Architectural Models
[7] For processor DUVs, the architectural state corresponds to programmer-visible registers, and mapping functions connect this architectural view to the implementation (e.g., hiding pipeline forwarding logic behind a register-file view). Automated Formal Verification of Processors Based on Architectural Models
[8] Architectural-style verification explicitly models architectural state and interfaces to memories or ports, and defines a next_state macro describing the effect of instructions and interrupts on that state. Automated Formal Verification of Processors Based on Architectural Models
[9] Consistency assertions are automatically generated to cover overall DUV correctness, ensuring correct interaction of multiple instructions, consistent pipeline behavior when stages are empty, and that empty stages do not update state elements. Automated Formal Verification of Processors Based on Architectural Models
[10] The overall verification is fail-safe — it cannot succeed if the DUV is not correct — and failing consistency assertions help the user debug mapping functions that need revision. Automated Formal Verification of Processors Based on Architectural Models
[11] Tool-augmented SVA-generation approaches gather design context (e.g., semantic search over an AST-indexed vector database and structural queries) and refine assertions using formal proof feedback over multiple verification rounds. From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation
[12] Evaluation on design-to-SVA benchmarks shows that solver-in-the-loop LLM-based assertion generation can achieve 93.7% syntax correctness and 82.0% functional correctness, confirming the central role of the DUV's structure in assertion quality. From Language to Logic: Bridging LLMs & Formal Representations for RTL Assertion Generation
[13] Commercial formal-verification tools (e.g., OneSpin 360MV) support the full spectrum required to verify a DUV, from SVA verification to automatic completeness analysis, and provide IPC and k-induction proof engines suitable for complete processor verification. Automated Formal Verification of Processors Based on Architectural Models
[14] The structured architecture-driven property-generation approach significantly reduces the verification effort for a DUV compared to manual complete formal verification. Automated Formal Verification of Processors Based on Architectural Models