Overview

Register-Transfer Level (RTL) is the abstraction at which digital hardware designs are described in terms of the movement of data between registers and the logical/arithmetic operations applied to that data. Hardware designs are not directly executable on a host machine, so they are implemented at RTL and evaluated using an RTL simulator or formal engine. RTL designs are usually expressed in a hardware description language (HDL) such as Verilog, VHDL, Chisel, or SystemVerilog. [RTL abstraction and HDL expression]

Role in hardware fuzzing

Hardware fuzzing adapts coverage-guided fuzzing (CGF) from software testing to the verification of RTL processor designs. In this setting, the processor design is simulated at RTL rather than executed directly, and inputs are mutated in a feedback loop that rewards coverage of new hardware states. [RTL in hardware fuzzing]

ProcessorFuzz uses Control and Status Register (CSR) transitions as the coverage signal for fuzzing RTL designs. The paper motivates this approach by noting that prior processor-fuzzing works target Register-Transfer Level (RTL) designs but suffer from limitations such as lack of support for widely used HDLs and misleading coverage signals. ProcessorFuzz is HDL-agnostic and requires no instrumentation of the RTL design, and was evaluated on three open-source RISC-V processors: Rocket, BOOM, and BlackParrot. [CSR-based RTL fuzzing]

ProcessorFuzz contrasts two simulation speeds in this workflow. Prior approaches relied on RTL simulation to decide whether a test input was interesting, which the paper characterizes as time-consuming. ProcessorFuzz instead uses ISA-level simulation to rapidly determine interesting inputs, since ISA simulation is significantly faster than RTL simulation. [ISA versus RTL simulation]

Instruction distillation and ACO-based RTL fuzzing (Instiller)

Prior CPU-fuzzing work faces the issue that the length of register-transfer level (RTL) input instructions keeps growing, and longer inputs are ineffective for fuzzing. Instiller (Instruction Distiller) is an RTL fuzzer built on a variant of Ant Colony Optimization (VACO) that distills input instructions so that the input instruction length stays short and efficient for fuzzing. It also addresses the weakness of prior work in simulating realistic interruptions during fuzzing by inserting interruptions and exceptions when generating inputs, and adds hardware-based seed selection and mutation strategies. In experiments against real-world CPU cores, Instiller achieves 29.4% more coverage than DifuzzRTL, 17.0% more mismatches, and generates 79.3% shorter input instructions than DifuzzRTL, with the distillation yielding a 6.7% increase in execution speed on average. [Instiller RTL fuzzing]

Differential fuzzing at RTL (DifuzzRTL)

DifuzzRTL employs differential fuzz testing to uncover vulnerabilities in CPU designs and introduces a register-coverage metric tailored for RTL designs, effectively guiding input generation to comprehensively explore CPU states and detect vulnerabilities. [DifuzzRTL]

Coverage-directed RTL fuzzing with selective symbolic execution (FuSS)

FuSS is a coverage-directed hardware fuzzing framework that uses selective symbolic execution. It consists of five major components: design instrumentation, fuzzing until reaching a coverage plateau, hardware-program context mapping, source analysis, and selective symbolic execution. FuSS addresses the coverage plateau problem faced by property-checking-based fuzzing approaches (such as ignoring fuzzing results during property checking, state space explosion during property checking of complex corner cases, and reliance on pre-defined properties) by using the current fuzzing trajectory to construct a minimal input sequence that activates rare scenarios dynamically using selective symbolic execution. [FuSS framework]

Transient execution fuzzing at RTL (DejaVuzz)

Hardware bugs are difficult to fix once the design is manufactured, so detecting transient execution vulnerabilities during the Register Transfer Level (RTL) development phase is crucial, because early detection allows for timely remediation before integration into production hardware. DejaVuzz is an effective and efficient pre-silicon processor fuzzer for transient execution vulnerabilities that is powered by two operating primitives: dynamic swappable memory and differential information flow tracking. Dynamic swappable memory serves as an isolation primitive that transparently switches instruction sequences to control the microarchitecture to trigger desired transient execution behaviors, resolving conflicts between instruction sequences by time-sharing the address space. [DejaVuzz RTL fuzzing]

Existing fuzzers define several coverage metrics to reflect general processor behavior, including mux toggle coverage, control register coverage, and hardware behavior coverage, but these general metrics are unsuitable for transient execution bugs because they are unaware of the propagation of sensitive data. Existing transient execution bug fuzzers (such as IntroSpectre and TEESec) dump the microarchitecture at each cycle and assess whether leakage has occurred based on the presence of the secret values in the log, while SpecDoctor observes execution behavior by hashing the final state of the timing components after transient execution and evaluates leakage by comparing the consistency of hash values between different variants. [Transient execution coverage metrics]

DejaVuzz applies an RTL simulator to convert the Design Under Test (DUT) into a software model and then uses the model to execute generated instruction sequences; during simulation, it leverages instrumentation to measure coverage to guide mutations. [DejaVuzz DUT simulation]

Microarchitectural state transitions for timing bug localization

One technique automatically extracts microarchitectural state transitions from a processor's register-transfer level (RTL) design and instruments the design to monitor these transitions as coverage metrics, enabling precise detection and localization of timing vulnerabilities in processor designs. [RTL state-transition coverage]

Bug detection by RTL/ISA trace comparison

When ProcessorFuzz determines that an input produces a unique CSR transition, it launches RTL simulation and generates an extended RTL trace log. It then compares that RTL trace log with an extended ISA trace log; any difference between the logs is treated as a potential processor-design bug that requires further investigation by a verification engineer. Inputs that do not produce a unique transition are discarded and the fuzzer proceeds to the next iteration. [RTL and ISA trace comparison]

Tooling for RTL simulation and comparison

In the ProcessorFuzz evaluation, RTL simulation for all processor designs used Verilator, an open-source RTL simulator. The evaluated open-source RISC-V processors were designed in different HDLs, including Chisel and SystemVerilog. The paper also compares ProcessorFuzz against DIFUZZRTL, a register-coverage-guided approach, using the same mutation engine so that the comparison focuses on coverage-feedback mechanisms rather than input-generation mechanisms. [RTL simulation tooling and comparison]

Role in hardware security (logic locking)

Traditional hardware logic-locking schemes are applied on the gate-level netlist produced after logic synthesis, and so lack semantic knowledge of the design function. Register-Transfer Level (RTL) locking schemes operate earlier in the flow and therefore have access to semantic hardware information, but recent work has shown that data-driven, machine-learning (ML) attacks can exploit this semantic information to attack RTL locks. The paper "Designing ML-Resilient Locking at Register-Transfer Level" investigates the resilience of ASSURE, a state-of-the-art RTL locking method, against ML attacks, and proposes two ML-resilient RTL locking schemes that build on ASSURE. It also develops ML-driven security metrics, evaluated against an RTL adaptation of the ML-based SnapShot attack. [RTL locking and ML attacks]

Role in formal verification of processors

In formal verification flows, the architecture-level specification of a processor is related to its RTL implementation through user-defined mapping functions that refer to RTL objects such as pipeline stages, stall signals, and cancel signals. This separation yields a readable, proven-correct ISA description on the architecture side, with the mapping functions anchoring abstract concepts to concrete RTL signals. [Architecture-to-RTL mapping]

A complete property suite can be automatically generated from an architecture description together with these mapping functions, and used to formally verify the RTL implementation. The Kühne et al. approach generates properties that are complete by construction, and the tool FISACO implements the property generation. Interval Property Checking (IPC), which is similar to bounded model checking, is used as the underlying proof engine, and the OneSpin 360 MV tool is used to formally verify whole processor designs. The approach is demonstrated on an industrial control processor from the embedded automotive domain. [Automatic property generation for RTL]

Because simulation alone is not well suited to covering the full functionality of a pipelined processor (achieving sufficient design quality requires very large simulation campaigns and offers no guarantee that all possible bugs have been considered), formal techniques are positioned as offering the highest quality of verification for RTL processor implementations. [Formal vs. simulation-based RTL verification]

The architecture description itself lists the components of the processor (architecture registers, flags, memory and bus interfaces, and interface transaction types) and then defines each instruction by its execution condition (TRIGGER), updates to the program counter and architecture registers/flags, and one transaction per interface. The mapping functions for components such as the program counter and instruction register typically point to dedicated signals in the RTL, but the mapping of an architecture register file requires a model of pipelining because of forwarding mechanisms in RTL designs. [Architecture description structure]

Formal verification of RTL reliability under single-event upsets (SEUs)

Formal verification can be applied at the Register Transfer Level (RTL) to evaluate hardware reliability in the presence of Single Event Upsets (SEUs). One method combines writing SystemVerilog Assertions (SVA) properties with model checking to find all SEUs that may violate the corresponding properties. Cadence JasperGold FPV, a commercial formal verification tool that supports Register Transfer Level (RTL) models and SVA, is used to perform model checking. The method is used to assess the reliability of all register bits in a RISC-V Ibex Core and can exhaustively search the whole state space to find all candidate SEUs that may cause Silent Data Corruptions (SDCs), crashes, and hangs in a reasonable time. The evaluation results can be used to determine a cost-efficient protection strategy: use the most effective and most expensive technology to protect the most vulnerable bits, use a less effective but cheaper technology to protect less vulnerable bits, and leave reliable bits unprotected. The method proposes formal backward tracing to identify all faults causing catastrophic results, and develops SVA properties that can search crucial faults causing SDCs, crashes, and hangs. These properties can be adapted to other RISC-V processors with signal remapping, so the method is, in principle, general to other RISC-V processors. It is found that misaligned instructions can amplify fault effects and that some bits are more vulnerable than others. [RTL SEU reliability evaluation]

Role in test generation (functional constraints for ATPG)

An automatic functional-constraint extractor has been proposed that operates at the register-transfer level to produce functional constraints usable by ATPG tools. The generated pseudo-functional test patterns are then used to improve the verification process. [RTL functional constraints for ATPG]