Overview
Effective Processor Verification with Logic Fuzzer Enhanced Co-simulation presents a simulation-based verification flow for RISC-V processors. The flow combines Dromajo reference-model co-simulation with Logic Fuzzer, an RTL-level technique that inserts small pieces of logic into a design without breaking processor functionality, with the goal of reaching a broader range of microarchitectural states. [Paper venue and scope] [Logic Fuzzer definition]
Verification background
The paper frames processor verification around randomized tests and reference-model comparison. A random instruction generator produces randomized assembly instruction streams from a set of configurations; such tests can sweep a broad range of implemented functionality, but pure randomness gives little control over whether deep bugs caused by complex unit interactions will be reached. The paper notes that template-based generators can add constraints to steer test direction and depth. [Random instruction generation]
For pass/fail checking, the paper describes reference model comparison: running code on both the RTL design under test and a high-level golden model, then checking that architectural state matches. The paper characterizes the reference model as fast, uncomplicated, implementation-independent, and updated at instruction-level granularity. [Reference model comparison]
It distinguishes several comparison styles:
- End-of-simulation comparison compares architectural state only after the test finishes. The paper describes this setup as cheap and simple, but warns that an architectural error may be overwritten before the final comparison and that debugging may start far from the actual divergence. [End-of-simulation comparison]
- Trace comparison compares execution logs such as program-counter flow and register or memory writebacks. The paper states that trace comparison can fail for asynchronous stimuli such as interrupts and debug requests, because independently running models can receive the stimulus at different points and produce different traces. [Trace comparison limitation]
- Co-simulation runs the RTL and reference model in parallel and exchanges messages between them. On a commit event, the RTL signals the reference model to commit an instruction and compare state; a failed comparison immediately halts execution near the divergence. The setup also needs messaging for asynchronous interrupts so that the RTL can tell the emulator to follow the RTL execution path. [Co-simulation mechanism]
Dromajo-based co-simulation
The paper uses Dromajo as an emulator for co-simulation with RTL processors implementing the RISC-V RV64GC instruction set. Dromajo provides APIs intended to support integration with different RTL processor implementations. The paper also states that Dromajo can execute applications such as Linux benchmarks under fast software simulation at 17 MIPS, generate checkpoints after a selected number of cycles, and resume those checkpoints for hardware/software co-simulation. [Dromajo role]
The Dromajo verification flow is divided into checkpoint generation and co-simulation. First, Dromajo accepts a RISC-V ELF binary, runs standalone for a selected amount of time, and dumps the model’s architectural state to a checkpoint. During co-simulation, Dromajo is instantiated and encapsulated in the RTL as a submodule; both Dromajo and the RTL load the checkpoint into main memory, and after the boot code completes, both cores have identical architectural states. [Dromajo checkpoint flow]
Dromajo checkpoints include architectural state such as registers and CSRs, memory, interrupt-related state such as PLIC/CLINT state, and performance counters including cycle and instruction counts. The checkpoint is represented as a memory image and a bootrom image; the bootrom is a valid RISC-V program and leverages the RISC-V debug specification to change supervisor registers. The paper notes that, because most RV64 CPUs support the debug specification, Dromajo checkpoints can be shared across different CPUs with minimal initialization changes beyond loading a different memory and bootrom. [Dromajo checkpoint contents]
The paper also emphasizes productivity benefits of checkpoint-based co-simulation. It says checkpoints can avoid recompiling benchmarks, split a Linux boot sequence into multiple checkpoints, apply phase-analysis and simulation-point concepts, and allow long-running programs to be checkpointed and run in parallel to reduce simulation cost. It specifically notes that SPEC benchmark phases could be co-simulated by loading simulation points. [Checkpoint productivity]
Dromajo integration
Dromajo is compiled into a shared library, linked into a simulator, and called from Verilog through DPI wrapper functions. The paper describes cosim_init() as being invoked from an initial Verilog block, where it calls Dromajo’s initialization API with a configuration-file path. Its illustrated interaction also includes step() calls on committed instructions and a raise_interrupt() call for asynchronous interrupts, with execution halting on mismatch. [Dromajo integration]
The authors state that using Dromajo’s checkpointed infrastructure gave the evaluated cores a fully deterministic architectural state; instead of bringing up binaries during simulation, memories are prepopulated before simulation starts. [Deterministic checkpoint state]
Logic Fuzzer
Logic Fuzzer inserts small pieces of logic into the RTL implementation while preserving processor functionality. The paper says fuzzable logic is logic that does not affect architectural functionality, and that fuzzing such logic can drive the processor into a broader range of microarchitectural states. [Logic Fuzzer definition]
One example in the paper replaces instruction-cache tag and data arrays with table mutators accessed through DPI. The branch history table is forced to provide a taken prediction, the branch target buffer is forced to provide an address with a specific tag, and the fuzzer tables are programmed to provide a random instruction stream when that tag is observed. [Logic Fuzzer table-mutator example]
Evaluation and comparison to formal methods
The paper’s evaluation methodology states that Dromajo co-simulation enhanced with Logic Fuzzer was evaluated on three open-source RISC-V processors; the excerpted evidence begins the list with CVA6, previously known as Ariane. [Evaluation methodology]
The paper contrasts its simulation-based approach with formal verification. It describes formal methods as exhaustive over possible execution paths, but limited by scalability to modular-level designs or designs of moderate size and complexity. By contrast, simulation-based verification is scalable but only explores the finite execution paths induced by supplied stimuli, such as directed unit tests, real applications, and randomly generated instructions. [Formal verification comparison]