RTL Verification
ConceptRTL (Register-Transfer Level) verification checks that a hardware design expressed at the register-transfer level behaves as intended, and is reported to consume 60-70% of modern hardware development time. The evidence describes a spectrum of verification approaches: simulation-based flows (including cross-level testing with an ISS reference and test-generation frameworks such as riscv-dv), sequence-based stimulus generators like SGen, automated generation methods that use ILP, genetic algorithms, Bayesian networks, or coverage-directed techniques, recent LLM-based agentic systems (Pro-V, PRO-V-R1) that couple LLMs with programmatic tools, and formal techniques such as Contract Shadow Logic that target security properties for processors vulnerable to speculative execution attacks.
First seen 5/26/2026
Last seen 9/5/2026
Evidence 23 chunks
Wiki v4
WIKI
Overview
RTL (Register-Transfer Level) verification is the activity of checking that a hardware design, described at the register-transfer level of abstraction, behaves as intended. Evidence describes it as a primary bottleneck in modern hardware development, reported to consume 60-70% of development time. [C1] Bugs that escape RTL verification are described as lengthening design cycles and producing significant follow-up costs.
The same evidence observes that, although Large Language Models (LLMs) have shown promise for RTL automation, their performance and research focus have overwhelmingly centered on RTL generation rather than verification. [C1]
NEIGHBORHOOD
3 nodes · 2 edgesgraph · RTL verification · depth=1
RELATIONSHIPS
10 connectionsRTL verification predominantly uses simulation-based methods.
The paper focuses on RTL verification of RISC-V processors.
riscv-dv is used to perform RTL verification of RISC-V IP.
SGen is used to verify RTL designs and catches RTL bugs.
RVVTS is extended to support RTL verification, enabling application to RVV RTL implementations.
Synthesizing Formal Models of Hardware from RTL for Efficient Verification of Memory Model Implementations (hsiao:micro:2021) ← uses 97% 1e
The paper synthesizes formal models from RTL for verification.
RTL verification uses ISA specifications to verify that implementations match the specification.
Cross-level co-simulation is used for RTL verification of RISC-V processors
riscv_asm_program_gen generates programs used for RTL verification of RISC-V IP.
ConfigDrivenV implements automated RTL verification.
CITATIONS
13 sources13 citations — click to expand
[1] RTL verification is described as a primary bottleneck consuming 60-70% of development time, and LLM performance/research has overwhelmingly centered on RTL generation rather than verification. PRO-V-R1: Reasoning Enhanced Programming Agent for RTL Verification
[2] PRO-V-R1 is the first trainable open-source agentic framework for autonomous RTL verification, comprising PRO-V sys (modular agentic system coupling LLM reasoning with programmatic tool use), a data-construction pipeline using existing RTL datasets to build simulation-validated SFT trajectories, and an RL algorithm using verification-specific rewards from program-tool feedback. PRO-V-R1: Reasoning Enhanced Programming Agent for RTL Verification
[3] PRO-V-R1 achieves 57.7% functional correctness and 34.0% robust fault detection, compared with the base model's 25.7% and 21.8% respectively, and outperforms large-scale proprietary LLMs in functional correctness with comparable robustness for fault detection. PRO-V-R1: Reasoning Enhanced Programming Agent for RTL Verification
[4] Existing RTL verification methods relying on large-scale proprietary models such as GPT-4o to generate Python-based functional references incur high cost and data-privacy risks, and no end-to-end open-source solution for autonomous RTL verification existed prior to PRO-V-R1. PRO-V-R1: Reasoning Enhanced Programming Agent for RTL Verification
[5] Contract Shadow Logic is a formal verification technique that improves RTL verification scalability and is applicable to different defense mechanisms against speculative execution attacks, leveraging computer-architecture design insights to check security properties formulated as software-hardware contracts for secure speculation. RTL Verification for Secure Speculation Using Contract Shadow Logic
[6] Contract Shadow Logic was evaluated on multiple RTL designs including three out-of-order processors and shows significant advantage over the baseline and two state-of-the-art verification schemes (LEAVE and UPEC) in finding attacks on insecure designs and deriving complete proofs on secure designs. RTL Verification for Secure Speculation Using Contract Shadow Logic
[7] The Contract Shadow Logic scheme is described as accessible to computer architects and as requiring minimal formal-method expertise. RTL Verification for Secure Speculation Using Contract Shadow Logic
[8] SGen is a sequence-based assembly generator written in C++11 that bridges directed and fully random stimulus methods without a constraint engine, using C++11 lambda functions in a random interface class to describe complex relationships between random variables. Micro-processor verification using a C++11 sequence-based stimulus engine
[9] SGen generates tests of 25k-50k instructions per run with an average execution time of 709 ms across 500 runs and an average throughput of 31k instructions per second, adding no significant compute or license overhead to simulation times. Micro-processor verification using a C++11 sequence-based stimulus engine
[10] SGen is used to verify the Cavium ThunderX2 core and is reported to be better at uncovering certain types of errors than existing tools (e.g., PPIGen), generating far more failures for the same number of runs with similar bucket counts. Micro-processor verification using a C++11 sequence-based stimulus engine
[11] Prior automated test-program generation work for RTL verification includes Genesys-Pro (Adir et al.), evolutionary test program induction (Corno et al.), genetic bias generation for biased random instruction generation (Bose et al.), coverage-directed test generation using Bayesian networks (Fine and Ziv; Braun, Fine, and Ziv), constraint-based random stimuli generation (Naveh et al.), graph-based functional test program generation for pipelined processors (Mishra and Dutt), and ILP-based approaches to automating simulation-based design verification. Towards Automating Simulation-Based Design Verification Using ILP
[12] Functional vector generation techniques for HDL models include linear programming and 3-SAT approaches (Fallah, Devadas, and Keutzer) and extended finite state machine model-based generation (Cheng and Krishnakumar). Micro-processor verification using a C++11 sequence-based stimulus engine
[13] ISA-specification and architectural-modeling work that relates to RTL verification includes synthesizing formal hardware models from RTL for memory-model verification (Hsiao et al., MICRO 2021), reverse-engineering instruction encodings (Hsieh et al., USENIX 2001), the Instruction-Level Abstraction (ILA) for SoC verification (Huang et al., TODAES 2019), and axiomatic hardware-software contracts for security (Mosier et al., ISCA 2022). ISA specification related work notes