Part III·Single-Cycle, Multi-Cycle, and Pipelined CPUs·Chapter 35 of 66

Part IIISingle-Cycle, Multi-Cycle, and Pipelined CPUs

Lab --- Verification and Cycle-Accurate Simulation

August 3, 2026·24 min read·intermediate

The project of Chapter 34 produced a working five-stage pipelined CPU that passes a hand-picked set of riscv-tests. “Passes a hand-picked set” is not the same as “is correct.” Many bugs hide in instructions or…

The project of Chapter 34 produced a working five-stage pipelined CPU that passes a hand-picked set of riscv-tests. “Passes a hand-picked set” is not the same as “is correct.” Many bugs hide in instructions or combinations the chosen tests never exercise. This lab takes the next step: it sets up the three test infrastructures that the RISC-V community uses to gain confidence that a core is actually correct, and it walks through using each of them on the CPU from Chapter 34. Along the way the reader will build a Verilator C++ testbench, learn the Surfer waveform-viewer workflow, and run a formal proof that the core is equivalent to a golden model for every legal instruction sequence up to a bounded length.

The lab is organized as four sequential exercises. Exercise 1 sets up riscv-tests and runs the RV32I unit tests. Exercise 2 sets up riscv-arch-test and runs the compatibility suite. Exercise 3 sets up Verilator and writes a C++ testbench that runs much faster than the Chisel testbench. Exercise 4 sets up riscv-formal and runs a formal equivalence proof. The lab closes with a Surfer workflow section that ties all four together, since waveform inspection is the common debugging step every time a test fails or a proof returns a counterexample.

The lab assumes the CPU built in Chapter 34 is available as a working Chisel module. The exercises emit Verilog through Chisel’s ChiselStage flow and operate on that Verilog with the verification tools. No new HDL code is required.

01.Setup and Installation

The lab requires two tool families on top of the Chapter 34 setup. The first is the SymbiYosys formal toolchain, which includes the Yosys synthesis tool, the Z3 SMT solver, and the SymbiYosys driver. The second is the three RISC-V verification repositories themselves. Verilator, Surfer, and the RISC-V GNU cross-toolchain all carry over from Chapter 34 and are not reinstalled here.

macOS (Homebrew)

macOS setup via Homebrew

Bash

# Already from Chapter 34: JDK, sbt, Verilator, Surfer, RISC-V GCC
brew install --cask temurin@21
brew install sbt verilator
brew install --cask surfer
brew tap riscv-software-src/riscv
brew install riscv-tools

# New for this lab:
brew install yosys z3 boolector
# SymbiYosys: install from source (no Homebrew formula)
git clone https://github.com/YosysHQ/sby
cd sby && sudo make install && cd ..

# Clone the test repositories
git clone https://github.com/riscv-software-src/riscv-tests
git clone https://github.com/riscv-non-isa/riscv-arch-test
git clone https://github.com/YosysHQ/riscv-formal

Verify each new tool:

Verify macOS new tools

Bash

yosys --version           # Yosys 0.40 or later
sby --version             # SymbiYosys
z3 --version              # Z3 4.x
boolector --version       # optional second SMT solver

Linux (Arch as canonical)

Arch Linux setup

Bash

# From Chapter 34:
sudo pacman -S jdk21-openjdk verilator riscv64-elf-gcc \
    riscv64-elf-binutils riscv64-elf-newlib
yay -S sbt surfer
# New for this lab:
sudo pacman -S yosys z3 boolector
yay -S symbiyosys-git
# Clone the test repositories
git clone https://github.com/riscv-software-src/riscv-tests
git clone https://github.com/riscv-non-isa/riscv-arch-test
git clone https://github.com/YosysHQ/riscv-formal

For Debian or Ubuntu, replace the package manager and source-build the SymbiYosys driver:

Debian/Ubuntu alternative

Bash

sudo apt install yosys z3 boolector verilator
git clone https://github.com/YosysHQ/sby
cd sby && sudo make install && cd ..

For Fedora:

Fedora alternative

Bash

sudo dnf install yosys z3 boolector verilator
git clone https://github.com/YosysHQ/sby
cd sby && sudo make install && cd ..

Windows (ArchWSL)

Windows setup via ArchWSL

Bash

# Inside the ArchWSL terminal:
sudo pacman -S jdk21-openjdk verilator riscv64-elf-gcc \
    riscv64-elf-binutils riscv64-elf-newlib \
    yosys z3 boolector
yay -S sbt surfer symbiyosys-git
git clone https://github.com/riscv-software-src/riscv-tests
git clone https://github.com/riscv-non-isa/riscv-arch-test
git clone https://github.com/YosysHQ/riscv-formal

02.Exercise 1: Running riscv-tests

The riscv-tests suite is the entry point. Each test is a small assembly program that exercises one instruction.

Building the tests

Build the suite

Bash

cd riscv-tests
git submodule update --init --recursive
autoconf
./configure --prefix=$PWD/install
make XLEN=32
make install

The XLEN=32 flag restricts the build to the 32-bit tests. The build produces ELF files under install/share/riscv-tests/isa/. The relevant tests for the Chapter 34 CPU are the rv32ui-p-* tests (user-mode I extension, physical addressing) and the rv32um-p-* tests (M extension).

Interpreting the tests

Each test follows the same convention. The test ends by writing a result code to a memory-mapped tohost address. A code of 0x1 means the test passed. Any other code means it failed, and the suite encodes a failure of sub-test $n$ as $2n + 1$ , so the failing sub-test number is the failure code shifted right by one bit. A failure in sub-test 3 therefore writes 0x7 and a failure in sub-test 5 writes 0xb. Failure codes are always odd and never equal 0x1, so a pass can never be mistaken for a failure. The riscv-tests repository documents the sub-test numbering in comments at the top of each test.

Excerpt from rv32ui-p-add.S

Riscv

# From riscv-tests/isa/rv32ui/add.S

#-------------------------------------------------------------
# Arithmetic tests
#-------------------------------------------------------------
TEST_RR_OP(2,  add, 0x00000000, 0x00000000, 0x00000000);
TEST_RR_OP(3,  add, 0x00000002, 0x00000001, 0x00000001);
TEST_RR_OP(4,  add, 0x0000000a, 0x00000003, 0x00000007);

TEST_RR_OP(5,  add, 0xfffffff0, 0x00000000, 0xfffffff0);
TEST_RR_OP(6,  add, 0xffffffff, 0xffffffff, 0x00000000);
TEST_RR_OP(7,  add, 0xfffffffe, 0xffffffff, 0xffffffff);

# ... and so on, then:
TEST_PASSFAIL

If tohost is written with 0xb, sub-test 5 failed. Open the test source to see what sub-test 5 was checking. In this excerpt, sub-test 5 verifies add 0x0 + 0xfffffff0 = 0xfffffff0, which is a signed addition of $0$ and $-16$ . A failure here points at an incorrect bit width or a missing sign-extension in the ALU.

Failure triage workflow

When a test fails, the recommended workflow is:

Read the failure code from tohost. Identify the sub-test number.
Open the test source and find the sub-test. Note the expected operands and result.
Run the test on Spike (the golden simulator) and confirm the test passes. This rules out a problem with the test itself.
Run the test on the Chapter 34 CPU again with VCD recording enabled.
Open the VCD in Surfer. Find the cycle where the failing sub-test executes. Inspect the operands flowing into the ALU and the result flowing out.
Compare to the expected behavior. The mismatch will point at the bug.

03.Exercise 2: Running riscv-arch-test

The riscv-arch-test framework goes a step further than riscv-tests. Each arch-test runs on the implementation, writes a signature region of memory, and then a Python harness compares the signature against a golden signature produced ahead of time on Spike or Sail. A test passes if the signatures match byte for byte.

Setting up the implementation plugin

Add the implementation target

Bash

cd riscv-arch-test
mkdir -p riscv-target/rv32-pipe

The target directory needs four files. Makefile.include says how to build and run a test, model_test.h is a C header the test code uses to define the signature region, link.ld is the linker script that places the text and signature regions at the addresses the Chapter 34 core’s memory map expects, and a small Python driver extracts the signature from the simulator output.

Skeleton Makefile.include

Makefile

# riscv-target/rv32-pipe/Makefile.include
TARGET_SIM   ?= $(SBT_DIR)/sbt
TARGET_FLAGS ?=

RUN_TARGET = \
    $(TARGET_SIM) -Dcpu.signatureOut=$(*).signature.output \
                  "runMain cpu.ArchTestRunner $(work_dir_isa)/$<"

COMPILE_TARGET = \
    $(RISCV_GCC) -march=$(RISCV_TARGET_MARCH) \
        -mabi=$(RISCV_TARGET_MABI) -DXLEN=32 \
        -nostartfiles -mcmodel=medany \
        -T $(ROOTDIR)/riscv-target/rv32-pipe/link.ld \
        $$(<) -o $$(@) \
        -I $(ROOTDIR)/riscv-test-suite/env \
        -I $(TARGETDIR)/$(RISCV_TARGET) \
        $(RISCV_TEST_OPTS)

model_test.h essentials

// riscv-target/rv32-pipe/model_test.h
#ifndef _COMPLIANCE_MODEL_H
#define _COMPLIANCE_MODEL_H

#define RVMODEL_DATA_BEGIN \
    .align 4; .global begin_signature; begin_signature:

#define RVMODEL_DATA_END \
    .align 4; .global end_signature; end_signature:

#define RVMODEL_HALT \
    li t0, 0x80001000; li t1, 1; sw t1, 0(t0); \
    1: beq x0, x0, 1b

#define RVMODEL_BOOT
#define RVMODEL_IO_INIT
#define RVMODEL_IO_WRITE_STR(_R, _STR)
#define RVMODEL_IO_CHECK()
#define RVMODEL_IO_ASSERT_GPR_EQ(_S, _R, _I)

#endif

Running the suite

Run the arch-test suite

Bash

cd riscv-arch-test
make RISCV_TARGET=rv32-pipe RISCV_DEVICE=I XLEN=32
make RISCV_TARGET=rv32-pipe RISCV_DEVICE=M XLEN=32

The framework produces a per-test signature file, compares it against the golden signature, and prints a pass or fail line for each test. At the end of the run a summary tallies the pass and fail counts per device.

A typical first run on a freshly-implemented core sees somewhere between 20% and 80% of the tests pass, depending on the maturity of the implementation. Each failure is an opportunity to extend the debug-and-fix loop from Exercise 1.

04.Exercise 3: Verilator C++ Testbench

ChiselTest is convenient for early development but slow for large test runs. Verilator can run the same Chisel-generated Verilog at ten to fifty times the cycle rate when driven from a hand-written C++ testbench. This section sets up the Verilator harness.

Emitting Verilog from Chisel

Emit Verilog from Chisel

Scala

// src/main/scala/cpu/Emit.scala
package cpu

import circt.stage.ChiselStage

object Emit extends App {
  ChiselStage.emitSystemVerilogFile(
    new Core(memSize = 65536),
    args = Array("--target-dir", "build"),
    firtoolOpts = Array("-disable-all-randomization",
                        "-strip-debug-info")
  )
}

Run the emit step

Bash

sbt "runMain cpu.Emit"
ls build/    # should contain Core.sv

The Verilator harness

Verilator C++ testbench

// sim/sim_main.cpp
#include <verilated.h>
#include <verilated_vcd_c.h>
#include "VCore.h"

#include <iostream>
#include <fstream>
#include <vector>

// VCD timeline counter. One clock cycle is two timesteps.
static uint64_t steps = 0;

int main(int argc, char **argv) {
    Verilated::commandArgs(argc, argv);

    VCore *top = new VCore();
    VerilatedVcdC *vcd = nullptr;

    bool tracing = false;
    for (int i = 1; i < argc; ++i) {
        if (std::string(argv[i]) == "--trace") tracing = true;
    }

    if (tracing) {
        Verilated::traceEverOn(true);
        vcd = new VerilatedVcdC();
        top->trace(vcd, 99);
        vcd->open("trace.vcd");
    }

    // Reset for 5 cycles
    top->reset = 1;
    for (int i = 0; i < 10; ++i) {
        top->clock = i & 1;
        top->eval();
        if (vcd) vcd->dump(steps++);
    }
    top->reset = 0;

    const uint64_t maxCycles = 1'000'000;
    while (!top->io_halt && steps / 2 < maxCycles) {
        top->clock = 0; top->eval();
        if (vcd) vcd->dump(steps);
        top->clock = 1; top->eval();
        if (vcd) vcd->dump(steps + 1);
        steps += 2;
    }

    std::cout << "halted=" << (int)top->io_halt
              << " cycles=" << steps / 2 << std::endl;

    int rc = top->io_halt ? 0 : 1;
    if (vcd) { vcd->close(); delete vcd; }
    delete top;
    return rc;
}

Build and run the testbench

Bash

verilator --cc --exe --build --trace \
    -Wno-fatal -CFLAGS "-O2" \
    --top-module Core build/Core.sv sim/sim_main.cpp \
    -o sim_core
./obj_dir/sim_core --trace
ls trace.vcd        # opens in Surfer

The Verilator binary runs the simulation at native CPU speed, producing the same VCD as the ChiselTest version but ten to fifty times faster for the same number of cycles. The speed matters when running the full rv32ui, rv32um, and arch-test suites in sequence.

05.Exercise 4: Formal Verification with riscv-formal

The riscv-formal framework is the most demanding verification step in this lab. It proves (within a bounded length) that the implementation’s behavior matches a golden model on every legal instruction sequence. Where simulation checks one specific sequence at a time, formal verification checks all sequences at once.

How riscv-formal works

The framework supplies a thin SystemVerilog wrapper around the implementation, declaring assertions that compare the implementation’s architectural state (registers, PC, memory writes) against a golden model after each retired instruction. The implementation must expose a RISC-V Formal Interface (RVFI) that publishes, for each retired instruction, the PC, the instruction word, the registers read, and the registers written. The RVFI is a small set of additional output signals that do not affect the core’s functional behavior.

SymbiYosys then drives Yosys (which compiles the wrapped design into a logical model) and an SMT solver (Z3 or Boolector) to ask: “Is there any sequence of $k$ instructions such that the implementation’s RVFI output disagrees with the golden model?” If the solver finds such a sequence, it returns a counterexample. If no such sequence exists within the bound, the core is proven equivalent to the golden model up to bound $k$ .

Adding the RVFI to the CPU

The Chapter 34 CPU does not expose the RVFI signals. The first step is to add them. The RVFI is a registered output that publishes, after each WB stage retirement, the relevant information about the retired instruction.

RVFI bundle and wiring

Code

// src/main/scala/cpu/RvfiBundle.scala
class RvfiBundle extends Bundle {
  val valid    = Bool()           // 1 when an instruction retired
  val order    = UInt(64.W)       // monotonically increasing
  val insn     = UInt(32.W)
  val trap     = Bool()
  val halt     = Bool()
  val pcRdata  = UInt(32.W)
  val pcWdata  = UInt(32.W)
  val rs1Addr  = UInt(5.W)
  val rs2Addr  = UInt(5.W)
  val rs1Rdata = UInt(32.W)
  val rs2Rdata = UInt(32.W)
  val rdAddr   = UInt(5.W)
  val rdWdata  = UInt(32.W)
  val memAddr  = UInt(32.W)
  val memRmask = UInt(4.W)
  val memWmask = UInt(4.W)
  val memRdata = UInt(32.W)
  val memWdata = UInt(32.W)
}

The Core module adds an rvfi output of this bundle. Inside the writeback stage, the bundle is populated from the MEM/WB pipeline register and gated by the valid bit. Each cycle the WB stage retires an instruction, the bundle publishes the information for one cycle. When no retirement happens (a bubble in WB), rvfi.valid is zero.

Configuring the proof

checks.cfg fragment

Plain Text

# checks.cfg (one section per instruction class)
[isa]
RV32I
[checks]
insn_add
insn_addi
insn_and
insn_andi
insn_beq
insn_bge
insn_bgeu
insn_blt
insn_bltu
insn_bne
insn_jal
insn_jalr
insn_lw
insn_sw
insn_or
insn_ori
insn_sll
insn_slli
insn_slt
insn_slti
# ... and so on for the entire base I subset
[options]
isa rv32i
depth 30

The depth parameter sets the bound. The checks list selects which equivalence checks to run. Each check verifies one instruction.

Running the proof

Run SymbiYosys

Bash

cd riscv-formal/cores/rv32-pipe
make    # generates per-instruction .sby files
# Run the proof for one instruction
sby -f insn_add.sby
# Or run them all in parallel
make -j8 verify

A typical proof for a single instruction takes between a few seconds and a few minutes depending on the depth and the complexity of the instruction. Memory instructions (loads and stores) are typically slower than ALU operations. Branches sit in the middle.

SymbiYosys output excerpt

Plain Text

[insn_add] Running engine_0
[insn_add] Solver: z3
[insn_add] Checking assertions in step 0..
[insn_add] Checking assertions in step 1..
...
[insn_add] Checking assertions in step 30..
[insn_add] Status: PASSED
[insn_add] DONE (PASS, rc=0)

A FAIL result includes a counterexample VCD. Open the VCD in Surfer to see the sequence of instructions that triggered the divergence. The counterexample is typically a short, surprising sequence (8 to 15 instructions) that exercises a corner case the test suites missed.

06.Surfer Workflow and Hotkeys

Every exercise so far ends with the same step: when something goes wrong, open the VCD in Surfer. Becoming fluent with Surfer makes the debug loop much shorter. This section is a quick reference.

Opening a trace

Open a VCD with Surfer

Bash

surfer trace.vcd
# Or from a remote machine:
surfer --server trace.vcd          # then connect from a browser

Surfer ships as both a native desktop application and a WebAssembly module that runs in the browser. The desktop application reads VCD and FST files directly. The browser version connects to a small server that streams the file to the browser.

Adding signals

Open the variables panel on the left, navigate into the Core module hierarchy, and double-click a signal to add it to the waveform view. Group related signals by drag-and-drop inside the waveform view. For the Chapter 34 CPU, the recommended initial signal set is:

Core.clock, Core.reset
Core.fetch.pc, Core.fetch.io_imemData
Pipeline registers: Core.ifId, Core.idEx, Core.exMem, Core.memWb
Hazard and forwarding: Core.decode.io_stall, Core.ex.fwd.io_fwdA, Core.ex.fwd.io_fwdB
Branch resolution: Core.ex.io_takeBranch, Core.ex.io_branchPC
Writeback: Core.wb.io_wAddr, Core.wb.io_wData, Core.wb.io_wEnable

Useful hotkeys

Table 1. Surfer keyboard hotkeys most useful for CPU debugging. Hotkey assignments are documented in Surfer’s online manual.

Hotkey	Action
`F`	Fit the visible time range to the trace duration.
`+, -`	Zoom in or out by a factor of two.
`Left, Right arrow`	Move the cursor one cycle.
`Shift+Left, Shift+Right`	Move the cursor to the previous or next signal transition on the focused signal.
`Home, End`	Jump to the start or end of the trace.
`/`	Open the variable search panel.
`Ctrl+G`	Go to a specific timestamp.
`M`	Add a marker at the cursor. Markers are labeled M1, M2, M3, and so on.
`Shift+M`	Jump to the next marker.
`R`	Show signal radix selector for the focused signal (binary, decimal, hexadecimal, ASCII).
`Ctrl+S`	Save the current view layout to a Surfer state file.
`Ctrl+O`	Open a saved state file.

A typical debug session

The pattern for debugging a failing test goes:

Open the VCD. Press F to fit the view.
Find the cycle where Core.wb.io_wEnable is high and Core.wb.io_wAddr matches the destination register of the failing instruction. The corresponding Core.wb.io_wData is the value the test saw.
If the value is wrong, scroll left to find the corresponding cycle in EX. Inspect the ALU inputs and outputs.
If the ALU inputs are wrong, scroll left further to find the cycle in ID. Inspect the register-file outputs and the forwarding-unit selectors.
Compare each step against the expected behavior.

07.Putting the Four Exercises Together

The four exercises sit at different levels of the verification hierarchy. The riscv-tests suite catches obvious bugs quickly with a small set of carefully-chosen programs. The riscv-arch-test suite catches more subtle bugs by checking signature regions against a golden trace. The Verilator testbench speeds up both of the above so that the full sweep runs in seconds rather than minutes. The riscv-formal proof catches the bugs the test suites miss by exhaustively exploring all instruction sequences up to a bounded length.

A complete verification flow runs them in that order. Fix the riscv-tests failures first, then the riscv-arch-test failures, then run Verilator to regression-test the full sweep at speed, then run the formal proof. Each layer typically uncovers a few bugs the previous layer did not catch. By the time all four layers pass, the confidence that the CPU is correct is far higher than any single layer alone could provide.

08.Worked Examples

Example: Diagnosing a tohost failure code

A run of rv32ui-p-sltu prints halted=1 cycles=842, and the testbench reports the tohost value as 0x13. What does this tell the debugger?

Solution. The test halted (so it did not time out), and the failure code 0x13 is 19 in decimal, which shifted right by one bit identifies sub-test 9 of sltu.S. Open the test source. Sub-test 9 of sltu is typically the comparison sltu 0xffffffff, 0xfffffffe which should produce 0 (because in unsigned comparison 0xffffffff > 0xfffffffe). If the CPU produces 1, the comparator is answering the opposite question and reporting greater-than where less-than was asked. Both operands have the same leading bit, so reading them as signed would also produce 0, which rules a signedness mistake out. The bug is in the ALU’s SLTU implementation, specifically the comparator direction.

Example: Reading a SymbiYosys counterexample

A formal proof of insn_jalr returns a counterexample at depth 8. The counterexample trace shows that on cycle 18, the implementation publishes rvfi.pcWdata=0x00000084 for a JALR, but the golden model expects rvfi.pcWdata=0x00000080. What is the likely bug?

Solution. JALR’s target is computed as (rs1 + imm) & ~1 (the least significant bit is cleared). The difference between 0x00000084 and 0x00000080 is bit 2, not bit 0, so the cleared-bit-zero rule is not the cause. The likely bug is that the implementation is using the wrong source for rs1. If the forwarding unit incorrectly priced a stale value from MEM/WB instead of the fresher value from EX/MEM, the target would be off by exactly the difference between the two producers’ results. Open the counterexample VCD and inspect the forwarding selectors on the offending cycle.

Example: Verilator speed measurement

A riscv-tests run takes 14 seconds in ChiselTest and 0.4 seconds in Verilator. The test executes about 1,000,000 simulated clock cycles. Compute the cycle rate for each backend.

Solution. ChiselTest: $1{,}000{,}000\,\text{cycles} / 14\,\text{s} \approx 71{,}000\, \text{cycles per second}$ . Verilator: $1{,}000{,}000 / 0.4 = 2{,}500{,}000\,\text{cycles per second}$ . The Verilator backend runs about 35 times faster. The speedup matters in regression sweeps where the full RV32I plus RV32M suite of about 60 tests runs end to end. At 14 seconds per test the suite takes 14 minutes. At 0.4 seconds per test it takes 24 seconds.

09.Exercises

Exercises

Build and run riscv-tests. Build the riscv-tests suite for XLEN=32. Run every rv32ui-p-* test on the Chapter 34 CPU. Report the pass and fail counts. For each failing test, identify the sub-test that failed and write a one-paragraph root-cause note.
Triage a deliberate bug. Modify the Chapter 34 CPU to reverse the forwarding priority (MEM/WB before EX/MEM). Run riscv-tests. List the tests that now fail and the sub-tests within them. Restore the correct priority.
Build and run riscv-arch-test. Set up the arch-test framework with the rv32-pipe target. Run the rv32i_m/I suite. Report the pass and fail counts. For each failure, compare the implementation’s signature against the golden signature byte for byte and identify the first differing byte.
Verilator harness. Write the C++ testbench described in a later section. Build it with Verilator and run it on the rv32ui-p-add test. Measure the wall-clock time and compare to the ChiselTest version. Report the speedup factor.
Verilator regression script. Write a shell script that runs every rv32ui-p-* and rv32um-p-* test through the Verilator harness and collects the pass/fail results in a CSV file. Re-run the script before and after each CPU change to track regressions.
Add the RVFI to the CPU. Extend the Chapter 34 CPU with the RVFI bundle described in a later section. Wire the bundle through to a top-level output port. Verify that on every retiring instruction the rvfi.valid bit is high and the rvfi.insn field matches what the writeback stage saw.
Run a formal proof. Configure SymbiYosys to prove insn_add at depth 15. Run the proof. If it fails, debug using the counterexample VCD. If it passes, run the next instruction (insn_addi).
Sweep proof depths. Run the insn_add proof at depths 5, 10, 15, 20, 25, and 30. Plot the proof time against the depth on a log scale. Fit a polynomial model and predict the time at depth 40.
Find a bug formally. Introduce a deliberate bug in the ALU (for example, ALU_SLT comparing as unsigned). Run the insn_slt proof. Capture the counterexample VCD and walk through it cycle by cycle in Surfer. Write a one-page debugging narrative.
Surfer state files. Save a Surfer state file that loads your preferred signal selection for the Chapter 34 CPU. Re-open the file on a fresh session and confirm the layout reloads correctly. Share the state file with a partner and confirm it works on their machine.
Coverage analysis. Verilator can collect line and toggle coverage. Build the testbench with --coverage and run the full riscv-tests suite. Use verilator_coverage to generate a coverage report. Identify the modules and lines with the lowest coverage. Write additional unit tests to improve coverage on those lines.
Combine all four. Build a Makefile target verify-all that runs riscv-tests, riscv-arch-test, the full Verilator regression, and the formal proof for every supported instruction, then prints a one-line summary of pass and fail counts for each. Make the target the standard regression entry point for the rest of the book’s projects.
Compare to Spike. For one test of your choice, run the test on both Spike and the Chapter 34 CPU. Record the architectural state (PC, register file, memory writes) at each retirement. Verify the two traces match. If they do not, identify the first divergence and explain its cause.
Run a Linux boot (stretch). Configure the Chapter 34 CPU with enough memory and a machine-mode CSR file to attempt a Linux boot. Use a publicly-available 32-bit RISC-V kernel image. Identify how far the boot proceeds before the CPU hits an unsupported instruction. Document the gap between the CPU’s current capability and a Linux-capable core.

Book mode

	yosys --version # Yosys 0.40 or later
	sby --version # SymbiYosys
	z3 --version # Z3 4.x
	boolector --version # optional second SMT solver

	# From Chapter 34:
	sudo pacman -S jdk21-openjdk verilator riscv64-elf-gcc \
	riscv64-elf-binutils riscv64-elf-newlib
	yay -S sbt surfer

	# New for this lab:
	sudo pacman -S yosys z3 boolector
	yay -S symbiyosys-git

	# Clone the test repositories
	git clone https://github.com/riscv-software-src/riscv-tests
	git clone https://github.com/riscv-non-isa/riscv-arch-test
	git clone https://github.com/YosysHQ/riscv-formal

	sudo apt install yosys z3 boolector verilator
	git clone https://github.com/YosysHQ/sby
	cd sby && sudo make install && cd ..

	sudo dnf install yosys z3 boolector verilator
	git clone https://github.com/YosysHQ/sby
	cd sby && sudo make install && cd ..

	# Inside the ArchWSL terminal:
	sudo pacman -S jdk21-openjdk verilator riscv64-elf-gcc \
	riscv64-elf-binutils riscv64-elf-newlib \
	yosys z3 boolector
	yay -S sbt surfer symbiyosys-git

	git clone https://github.com/riscv-software-src/riscv-tests
	git clone https://github.com/riscv-non-isa/riscv-arch-test
	git clone https://github.com/YosysHQ/riscv-formal

	cd riscv-tests
	git submodule update --init --recursive
	autoconf
	./configure --prefix=$PWD/install
	make XLEN=32
	make install

	cd riscv-arch-test
	make RISCV_TARGET=rv32-pipe RISCV_DEVICE=I XLEN=32
	make RISCV_TARGET=rv32-pipe RISCV_DEVICE=M XLEN=32

	verilator --cc --exe --build --trace \
	-Wno-fatal -CFLAGS "-O2" \
	--top-module Core build/Core.sv sim/sim_main.cpp \
	-o sim_core

	./obj_dir/sim_core --trace
	ls trace.vcd # opens in Surfer

	// src/main/scala/cpu/RvfiBundle.scala
	class RvfiBundle extends Bundle {
	val valid = Bool() // 1 when an instruction retired
	val order = UInt(64.W) // monotonically increasing
	val insn = UInt(32.W)
	val trap = Bool()
	val halt = Bool()
	val pcRdata = UInt(32.W)
	val pcWdata = UInt(32.W)
	val rs1Addr = UInt(5.W)
	val rs2Addr = UInt(5.W)
	val rs1Rdata = UInt(32.W)
	val rs2Rdata = UInt(32.W)
	val rdAddr = UInt(5.W)
	val rdWdata = UInt(32.W)
	val memAddr = UInt(32.W)
	val memRmask = UInt(4.W)
	val memWmask = UInt(4.W)
	val memRdata = UInt(32.W)
	val memWdata = UInt(32.W)
	}

	# checks.cfg (one section per instruction class)
	[isa]
	RV32I

	[checks]
	insn_add
	insn_addi
	insn_and
	insn_andi
	insn_beq
	insn_bge
	insn_bgeu
	insn_blt
	insn_bltu
	insn_bne
	insn_jal
	insn_jalr
	insn_lw
	insn_sw
	insn_or
	insn_ori
	insn_sll
	insn_slli
	insn_slt
	insn_slti
	# ... and so on for the entire base I subset

	[options]
	isa rv32i
	depth 30

	cd riscv-formal/cores/rv32-pipe
	make # generates per-instruction .sby files

	# Run the proof for one instruction
	sby -f insn_add.sby

	# Or run them all in parallel
	make -j8 verify

	[insn_add] Running engine_0
	[insn_add] Solver: z3
	[insn_add] Checking assertions in step 0..
	[insn_add] Checking assertions in step 1..
	...
	[insn_add] Checking assertions in step 30..
	[insn_add] Status: PASSED
	[insn_add] DONE (PASS, rc=0)

	surfer trace.vcd
	# Or from a remote machine:
	surfer --server trace.vcd # then connect from a browser