Definition
A Design Under Verification (DUV) is the hardware design whose behavior is being checked by a verification methodology. The verification plan enumerates a large set of features in the DUV that need to be verified, where each feature is associated with coverage events the verification team expects to observe during the verification process and the methods used to verify the feature. [DUV-definition] [DUV-feature-coverage]
Role in Coverage-Driven Verification
Coverage-Driven Verification (CDV) is based on three main components: a verification plan comprising features in the DUV that need to be verified; random stimuli generators directed towards the verification goals using test-templates (i.e., general specifications of the desired test structure and properties); and coverage analysis tools that detect the occurrence of events in the verification plan and provide feedback regarding the state and progress of the verification process. The verification plan is implemented using random stimuli generators that produce a large number of test-cases, and coverage tools that look for the occurrence of events in the verification plan. [CDV-components] [DUV-RSG-coverage]
The random stimuli generators are directed towards verification goals by using test-templates. The test-templates allow the generators to focus on areas in the DUV ranging from large generic areas, like the floating-point unit, to very specific areas, like a bypass between stages of the pipeline. Coverage analysis identifies gaps in the implementation of the plan. Its feedback is used to modify test-templates that do not fulfill their goals, and to create new ones. [DUV-test-templates]
Goals of Stimuli Generation Against the DUV
When stimuli are applied to a DUV, stimuli generation must pursue several goals drawn from the verification plan: achieve every item in the test scenarios matrix; ensure those scenarios are actually happening during simulation; ensure that any anomalies propagate to an existing checker (hitting a bug without exposing it is worthless); additionally, hit and expose problems not anticipated in the verification plan; provide information that helps recreate and understand problems that are identified; and ensure that nothing gets broken over time as the DUV evolves. [stim-goals-matrix] [stim-goals-bug-exposure] [stim-goals-recreate] [stim-goals-stability]
Running Example: A Processor as DUV
A PowerPC processor is used as a canonical DUV example. Architecturally it is a RISC design with a small set of instructions (~400), one simple operation per instruction, fixed-length 32-bit (one-word) instructions, specific load/store instructions for memory access, large register files (32 general-purpose registers and 32 floating-point registers used only for floating-point operations), several special-purpose registers (condition, link, status, etc.), and a complex memory model with multi-level address translation and coherency rules. [PowerPC-arch-view]
Microarchitecturally the DUV pipeline is multi-threaded, in-order, four instructions wide (Fetch, Decode, Dispatch), with four execution units: Branch (B), Simple Arithmetic (R), Complex Arithmetic (M), and Load/Store (S). The pipeline stages include Data Fetch, Execute, and Write Back, and the design interfaces an instruction cache and a data cache. [PowerPC-microarch]
Verification Plan Requirements on the DUV
A typical verification plan for a processor DUV extracts two core requirements: (1) check that all pairs of instructions execute correctly together, which is a basic architectural requirement appearing in most processor verification plans but is harder to satisfy than it appears; and (2) check that all forwarding mechanisms between pipeline stages work properly, which is a basic microarchitectural requirement and a common source of bugs in previous designs. [verify-plan-pairs] [verify-plan-forwarding]
Role in Dynamic Simulation-Based Verification
In dynamic verification, the main functional-verification technique for large and complex systems, a large number of tests are generated using random test generators, simulated on the design-under-verification, and checked against its specification. Confidence in correctness is acquired by running a set of test cases that encompass a sufficiently large and representative sample of cases. [dynamic-verification-role] [simulation-confidence]
Functional verification is widely acknowledged as a design-cycle bottleneck: up to 70% of development time and resources are typically spent on functional verification, because fixing flaws after release risks reputation harm, costly recall/replacement of a large installed base, and litigation over injuries. [verification-bottleneck]
Coverage measures thoroughness of testing for the DUV and is the prime indicator of test-set quality. Higher coverage implies greater chances of exposing a design flaw, and is especially difficult to obtain when interactions among different functions of the DUV are non-determinative or hard to reproduce. [coverage-measure] [interaction-coverage-hard]
Knowledge Requirements
Compared with simulation-based approaches, formal verification requires deep knowledge of the DUV's internals in order to write useful assertions. This is a central motivation for automating formal verification of well-defined classes of circuits, because it eases the migration from simulation to formal methods. [DUV-deep-knowledge]
Role in Property-Based Verification
In formal property checking, the intended behavior of a DUV can be expressed as safety properties. Interval Property Checking (IPC) checks bounded safety properties with SAT-based techniques and uses arbitrary starting states rather than only the initial state. If a property holds from an arbitrary state, it also holds from any reachable state, giving exhaustive verification for that property; counterexamples from unreachable states can be addressed by adding invariants. [IPC-DUV-verification]
A complete property suite aims to cover every possible input scenario, or transaction sequence, with a chain of properties that predicts states and outputs at every point in time. Under this view, any two designs satisfying all properties in a complete suite are formally equivalent. The equivalence of the property suite and the DUV is established by chaining the generated properties, with each property consisting of an assume part (assumption A) and a prove part (consequent C). [complete-property-suite] [property-DUV-chaining]
Completeness analysis checks include whether successor properties exist with matching assumptions, whether the successor is uniquely determined, and whether each property uniquely describes the DUV's outputs and states. [complete-property-suite]
Architectural-State Abstraction
For processor verification, the DUV can be described through a high-level operation view: each property captures the effect of executing a single instruction on the internal state and outputs. The state of the DUV is described in terms of an Architectural State, corresponding to the programmer-visible registers of the design. Mapping functions connect this architectural state to the implementation, for example by hiding pipeline forwarding logic behind an architectural register-file view. [architectural-state-abstraction]
This abstraction makes operation properties resemble a high-level specification while still being checked against the RTL. In an architectural-style formulation, 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. [architectural-style]
To adapt the general processor model to the actual DUV, the user supplies mapping functions and basic pipeline data (constants). During property-suite generation, architecture register R(i) is replaced by an instantiation of Data_R(sfwd, i), where sfwd is the forwarding target stage (usually decode), and the resulting properties prove instruction correctness on the implementation level with an A \u21d2 C implication structure at successive instruction timepoints. [DUV-mapping-functions]
Consistency Assertions for the DUV
While instruction properties describe the processing of a single instruction through the pipeline, a set of consistency assertions is automatically generated alongside them to cover the overall correctness of the DUV. These assertions ensure the correct interaction of multiple instructions and the consistent pipeline behavior when no instruction is present in a dedicated stage. For example, they check that empty stages will not update any state elements, and that instructions do not overwrite each other or cause empty pipeline stages to have an effect on the visible registers or issue-interface transactions. Consistency assertions also help the user find an appropriate architectural mapping by giving feedback for debugging when a property fails. [consistency-assertions] [consistency-feedback]
The overall verification is fail-safe: it cannot succeed if the DUV is not correct, but even for a correct design, finding the appropriate mapping functions can be difficult, and failing consistency assertions can guide the user to mapping functions that need revision. [consistency-fail-safe]
Processor Verification Environment
For a processor DUV, a typical verification environment places generators and drivers around the design. Generators produce instructions, I/O traffic, and memory traffic; drivers deliver those transactions into the appropriate interfaces of the DUV (instruction driver, I/O driver, memory driver). The DUV is thus exercised through its external interfaces by the coordinated outputs of multiple generators. [proc-verify-env] [proc-verify-generators]
Number of Generators Around the DUV
The stimuli generation strategy for a DUV must choose how generators are organized: distributed generators (each interface has its own generator that works independently \u2014 simple and easy to reuse, but hard to reach corner cases in a coordinated fashion), a single unified generator (one generator controls all interfaces, so all interfaces can work together toward a common goal, but complex and hard to reuse), or synchronized generators (each interface has its own generator, but they share information and synchronize \u2014 each generator can be reused separately while still working toward a common goal). [gen-distributed] [gen-single] [gen-synchronized]
Abstraction Levels for Stimuli to the DUV
Stimuli for the DUV can be produced at different abstraction levels: program or algorithmic level (groups of sequences across time), sequence level (groups of instructions), command and data / instruction level (individual instructions), or bit level (no abstraction \u2014 groups of bits). Higher abstraction levels are typically closer to the system-level view, while bit-level generation is closer to the designer's wire-level view. [abstraction-levels]
Issues in Stimuli Generation for the DUV
Open design choices when generating stimuli for a DUV include: how many generators to deploy, the level of abstraction at which to generate, online versus offline generation, dynamic versus static generation, and test length. These issues directly shape how the DUV is exercised and what aspects of its behavior are reachable from a test. [stim-issues]
Execution Engine and Test Generation
In dynamic verification systems, a test generator engine accepts test templates specifying test parameters directed at different functions of the DUV, and a template arbitrator unit selects the template for which the next transaction is generated. The combined test case is then executed by an execution engine on an implementation of the DUV; the execution engine may be a simulator of the DUV or a realization of the design. [execution-engine-DUV] [template-arbitrator]
Templates can be weighted so that selection order is determined probabilistically, and may include baseline, unbreakable, or sparseness-constrained sections, prologue/epilogue sections, and bounded inter-template occurrence constraints, enabling dynamic interleaving that exercises multiple functions of the DUV in combination. [template-interleaving-rules]
An abstract knowledge base can hold a formal description of the DUV specification, including testing constraints and coverage criteria, optionally with a general model of a DUV that biases the generator toward "interesting" cases. [knowledge-base-DUV]
Role in Pre-Silicon and Post-Silicon Verification
Pre-silicon and post-silicon verification share a common DUV focus but differ in execution speed and observability. On silicon platforms, limited observability does not allow measuring coverage on the silicon directly; acceleration platforms are leveraged to measure coverage of post-silicon tools, and shortly before first silicon samples come back from the fab, a regression suite of exerciser test-templates is created based on the coverage achieved on the accelerators. That regression suite is then used to continue the verification process on the silicon platform. [post-silicon-coverage-gap] [pre-post-silicon-platform]
A unified pre- and post-silicon methodology attaches to each line-item in the verification plan one or more target platforms on which it will be verified, and converts those line-items to test-templates in the languages of the generation tools used by each platform. The major differences between platforms dictate differences in the way test-templates are written for pre- and post-silicon tools: a test-template could be very specific and describe a small set of targeted tests, or it could be more general leaving more room for randomization. A pre-silicon test-template is typically more directed to ensure that the targeted scenarios are reached within the fewer cycles available on simulation, while a post-silicon test-template must allow for enough interesting variation to effectively use the many processor cycles available on silicon. [unified-methodology] [test-template-platform-differences]
Threadmill as a Post-Silicon Exerciser
Threadmill was developed to enable a unified methodology by supporting a verification process guided by a verification plan and enabling validation engineers to guide the exerciser through test-templates. Like its pre-silicon counterpart Genesys-Pro, the main input to Threadmill is a test-template that specifies the desired scenarios. Because pre- and post-silicon tests have different characteristics, Threadmill's test-template language omits constructs that require long generation time (such as events), and omits many testing knowledge items included in Genesys-Pro models. Other Threadmill inputs include the architectural model and testing knowledge and the system topology. The execution process starts with an off-line builder application that converts the data in the test-template and the architectural model into data structures embedded into an executable exerciser image. [Threadmill-builder] [Threadmill-language-differences]
The exerciser image is composed of three major components: a thin, OS-like layer of basic services required for Threadmill's bare-metal execution; a representation of the [exerciser-image-components]
An exerciser is a self-contained program that runs on the DUV and exercises it by testing interesting scenarios. It generates the test-cases, runs them, performs the checking, and contains OS services required by the test-cases. The exerciser runs in an endless loop, which makes it a good post-silicon solution since it is only loaded once on the DUV. [exerciser-DUV]
Role in Coverage-Guided Fuzzing of Hardware
In cross-level verification flows for hardware peripherals, the DUV (e.g., an RTL implementation of a RISC-V PLIC generated from SpinalHDL and compiled to SystemC RTL with Verilator) is placed inside a Coverage-Guided Fuzzing (CGF) testbench alongside a readily available TLM reference model. The fuzzer (e.g., LLVM libFuzzer) generates TLM-based transactions that are mapped to the DUV's inputs through a SystemC/C++ TLM-RTL transactor, which translates between TLM transaction payloads and RTL signals over clock cycles. The testbench collects coverage information in a feedback loop, and when a behavioral difference between the TLM reference and the RTL DUV is identified, the CGF stops and the input pattern is made available for debugging the mismatch. Coverage metrics (line, function, branch) on the DUV are reported in absolute and relative numbers and can be used to assess verification quality and to choose between fast and accurate co-simulations. The same RTL DUV, together with the transactor, can be integrated as a drop-in replacement in a full system Virtual Prototype, enabling co-simulation with the TLM reference and execution of embedded software and operating systems against the DUV. [CGF-DUV-testbench] [DUV-TLM-transactor] [DUV-mismatch-debug] [DUV-coverage-metrics] [DUV-drop-in-VP]
Relation to Assertion Generation
In SystemVerilog Assertion workflows, creating useful assertions requires expertise in both temporal logic and the design under verification. Recent tool-augmented approaches generate assertions from natural-language specifications by gathering design context (e.g., semantic search over an AST-indexed vector database and structural queries via formal tools such as JasperGold) and refining assertions with formal proof feedback over multiple verification rounds, illustrating that the DUV's structure and signals are central to assertion correctness. Such approaches are evaluated on design-to-SVA benchmarks, achieving high syntax and functional correctness. [SVA-DUV-context] [ProofLoop-evaluation]
Verification Tools and Tool Chains
The generated property suite can be formally verified against the RTL of the DUV using commercial formal-verification tools that support the required spectrum of techniques, from the verification of SystemVerilog assertions all the way to automatic completeness analysis. Such tools offer IPC and k-induction proof engines with sufficient capacity and performance to handle complete verification of processors, and have been applied to industrial processor designs. [verification-tools] [IPC-k-induction]
The overall effort for verifying a DUV can be reduced significantly compared to manual complete formal verification by adopting a structured, architecture-driven approach to property-suite generation. [structured-verification]