SymbFuzz + InterconFuzz

A standalone source package of SymbFuzz and InterconFuzz:

• SymbFuzz: coverage-directed hardware fuzzing. It runs Verilator simulation with a Yosys/Z3 bounded model checker (BMC) that solves for inputs reaching what random simulation misses.
• InterconFuzz: SymbFuzz for SoC interconnects. It wraps a bus, crossbar or NoC in a synthesizable protocol shell:

 fuzz knobs ──▶ manager/host BFMs ──▶ DUT (socket / xbar / NoC) ──▶ subordinate/device responders
                  │ scoreboard                                         │ routing + integrity checks
                  └──────── sticky bug_*_q flags, cov_*_q coverage ◀───┘

• The shell's only inputs are fuzz knobs. The BFMs turn any knob sequence into protocol-legal traffic, so random simulation and BMC witnesses are always legal scenarios.
• Ready/response knobs are forced after MaxStall stalls (a fair environment), so the hang watchdog is a real liveness check.
• Checkers latch sticky bug_*_q registers. A BMC goal bug_x_q=1 is a bug hunt.
• cov_*_q registers give protocol-level coverage.

Supported DUTs: OpenTitan tlul_socket_1n, any OpenTitan tlgen crossbar (a 2×4 test xbar and the real earlgrey xbar_main), PULP axi_xbar, and a FlooNoC 2×2 mesh (frontend probe only, see "NoC status").

Contents

README.md  requirements.txt
CMakeLists.txt  include/  src/      SymbFuzz BMC binary (C++20, Z3)
symfuzz/  symfuzz_run.py  pyproject.toml   SymbFuzz Python engine (+ harness templates)
InterconFuzz/
  rtl/common, rtl/shell             TL-UL shells (socket_1n shell; generic host/device for xbars)
  rtl/axi                           AXI4 shell around PULP axi_xbar (2 managers x 3 subordinates)
  rtl/dut                           DUT copies with `ifdef`-injected bugs (no define = original)
  configs/                          filelists (*.f) per DUT variant
  xbars/                            tlgen specs, generated xbar RTL, bug copies, generated shells
  noc/                              FlooNoC 2x2 mesh probe (config, generated RTL, filelists)
  coverage/  predicates/  protocols/  coverage-filter + bug-flag predicate plugins, bus layouts
  scripts/bmc_hunt.py               BMC matrix: every bug flag as a target, per DUT variant
  scripts/compare_campaigns.py      campaigns: fuzz-only vs fuzz + BMC goals
  scripts/gen_shell.py              shell generator for tlgen crossbars
  third_party/                      only the upstream RTL the filelists use (see below)
RTL_Tst_Cases/                      only the OpenTitan / PULP RTL the filelists use

Third-party RTL included

Only the files the filelists reference, at their original relative paths, with the upstream LICENSE files:

• OpenTitan hw/ip (prim, tlul), Apache-2.0;
• PULP axi and common_cells from the CVA6 5.3.0 vendor tree, SHL-0.51;
• the generated earlgrey xbar_main (OpenTitan 4b5d983);
• FlooNoC c48b645 with its pinned axi (0ccc838) and common_cells (63b7c50).

Files under InterconFuzz/rtl/dut/ and InterconFuzz/xbars/*/bugs/ are modified copies of upstream files. Each one keeps its original license header and has a note describing the injected bugs.

Setup

Required tools:

• Yosys (tested 0.66);
• Verilator 5.x (tested 5.052);
• CMake ≥ 3.16 and a C++20 compiler;
• Python ≥ 3.10;
• sv2v v0.0.13 binary, on PATH or at .venv/bin/sv2v.

# 1. Python environment
python3 -m venv .venv
.venv/bin/pip install -r requirements.txt
.venv/bin/pip install -e . --no-deps          # installs the `symfuzz` package

# 2. BMC binary (build/symbfuzz), linked against the Z3 that pip installed
Z3=$(.venv/bin/python -c "import z3, os; print(os.path.dirname(z3.__file__))")
cmake -S . -B build -DCMAKE_BUILD_TYPE=Release \
      -DZ3_LIB=$(ls $Z3/lib/libz3.so* | head -1) -DZ3_INCLUDE_DIR=$Z3/include
cmake --build build -j
#    (a system Z3 also works: plain `cmake -S . -B build` finds /usr/lib/libz3.so)

# 3. sv2v
#    unzip the release, then put the binary on PATH or copy it to .venv/bin/sv2v

The binary links to the pip Z3 by absolute path. If you move the venv, rebuild or set LD_LIBRARY_PATH=$Z3/lib.

Optional, only for regenerating RTL or for the NoC frontend:

• OpenTitan util/tlgen (sparse clone of lowRISC/opentitan);
• FlooNoC's floogen (pip install --no-deps -e <FlooNoC checkout>);
• the yosys-slang plugin (cmake build, gives slang.so).

Quick start

All commands run from the package root.

# BMC bug hunt (seconds): misroute bug in OpenTitan tlul_socket_1n
.venv/bin/python InterconFuzz/scripts/bmc_hunt.py --dut tlul_socket_1n -v bug_sel_trunc \
    -f bug_misroute_q --max-steps 16 --timeout 60000

# Same for the tlgen crossbar and PULP axi_xbar
.venv/bin/python InterconFuzz/scripts/bmc_hunt.py --dut x2d4 -v bug_uart_mask -f bug_access_q --max-steps 16
.venv/bin/python InterconFuzz/scripts/bmc_hunt.py --dut axi_xbar -v bug_decode_incl -f bug_misroute_q --max-steps 16

# Full campaigns: fuzz-only vs fuzz + BMC goals; results in InterconFuzz/work/compare*/results.json
.venv/bin/python InterconFuzz/scripts/compare_campaigns.py --dut tlul_socket_1n \
    -v clean -v bug_cnt_width -m fuzz -m symb -s 1 --timeout 600
#   --dut: tlul_socket_1n | x2d4 | xbar_main | axi_xbar;   --set key=val overrides config keys

# Plain SymbFuzz on any design (see `python symfuzz_run.py --help`)
.venv/bin/python symfuzz_run.py --config <campaign.yaml>

The DUT variants are clean plus the bug_* names in "Injected bugs". bmc_hunt.py with no -v/-f runs every variant × flag.

In symb mode, SymbFuzz gets every bug flag as a --bmc-goal, seeded from the current simulation state. It also uses the matching --coverage-filter-module (control bits only, payload dropped) and --predicate-module InterconFuzz/predicates/bug_flags.py. Detections go to <campaign>/violations.jsonl with cycle, wall time and source (batch = random/mutation, bmc_replay = BMC witness).

Notes:

• BMC steps are SMT transitions: 2 steps = 1 clock cycle.
• Campaigns of the same DUT share sv2v_cache/<top>__sv2v.v in the working directory, so run them one at a time.

Regenerate a tlgen crossbar shell:

.venv/bin/python InterconFuzz/scripts/gen_shell.py --spec InterconFuzz/xbars/ifz_x2d4.hjson \
    --rtl InterconFuzz/xbars/x2d4/rtl/autogen --out InterconFuzz/xbars/x2d4/shell

Checkers

Flag	Raised when	Shells
bug_misroute_q	a device accepts a request outside its address range	all
bug_corrupt_q	write data fails its self-check / illegal opcode, size or burst	all
bug_a_proto_q	DUT drops valid or changes payload while stalled (request side)	all
bug_rsp_unexpected_q	response for a source/ID with nothing outstanding	all
bug_rsp_mismatch_q	response code, data, size or last disagrees with the golden model	all
bug_d_proto_q	DUT drops valid or changes payload while stalled (response side)	all
bug_hang_q	outstanding work with no progress for HangLimit cycles (fair environment)	all
bug_access_q	request to a non-connected or unmapped region answered without error	xbar, AXI
bug_order_q	same-ID response matches a later transaction, not the head	AXI
bug_w_proto_q	wlast missing or early	AXI

The golden address model has one probe window per device range, one edge window just past each device's end (decode-boundary bugs), and one far unmapped window. Crossbar shells take connectivity from the tlgen spec, so a host reaching a device it isn't connected to is an access-control bug.

Injected bugs

DUT	Define	Bug
tlul_socket_1n	IFZ_BUG_SEL_TRUNC	device-select compare truncated to 1 bit
	IFZ_BUG_NO_HOLD	missing hold-while-outstanding interlock
	IFZ_BUG_ERR_DECODE	> instead of >= for the unmapped region
	IFZ_BUG_MAGIC_MISROUTE	trojan-style: one PutPartial/source/word/mask combo misrouted
	IFZ_BUG_CNT_WIDTH	outstanding counter 2 bits instead of 9 (wraps with 4 in flight)
x2d4 xbar	IFZ_XBUG_UART_MASK	UART decode mask doubled (address-map bug)
	IFZ_XBUG_DMA_STEER	dma's UART decode uses the RAM mask (copy-paste)
	IFZ_XBUG_M1_CONTEND	M:1 socket steers a response by the concurrent grant under contention
axi_xbar	IFZ_ABUG_DECODE_INCL	addr_decode end address inclusive (off-by-one)
	IFZ_ABUG_AR_ORDER	demux drops the same-ID "select occupied" stall on AR (ordering)
	IFZ_ABUG_W_SELECT	W beats follow a pending AW's select instead of the W FIFO head

Results so far (2026-10-07)

• No false alarms. Clean versions of all three DUTs ran with zero violations: socket_1n in 4 campaigns (fuzz and symb, 2 seeds), x2d4 in 18k cycles, axi_xbar in fuzz mode. BMC on clean designs found no counterexample within budget (not a proof).
• socket_1n.
  • SEL_TRUNC, NO_HOLD and ERR_DECODE are found by fuzzing in ≤47 cycles.
  • BMC finds the misroute in 0.4 s (2-cycle witness) and the magic misroute in 0.3 s.
  • The counter-wrap bug is out of reach for BMC from reset (timeout at 20 cycles).
• x2d4. BMC finds UART_MASK and DMA_STEER in 2–4 cycles and M1_CONTEND in 4 cycles (8 s). Fuzzing catches UART_MASK at cycle 28.
• axi_xbar. BMC finds DECODE_INCL in 2 cycles. AR_ORDER and W_SELECT are not found by BMC from reset at 10 cycles.
• The fuzz-vs-symb campaign comparison for the hard bugs was still running when this package was made. Results land in work/compare*/results.json.

SymbFuzz engine changes made for InterconFuzz (already in symfuzz/)

1. design_parser.py.
   • Yosys wraps else if generate branches in an extra genblkN scope that Verilator and xsim don't have. RegisterInfo.sim_name now fixes the simulator paths (OpenTitan prim_fifo_sync hit this).
   • Soundness fix: registers under generate arrays (gen_x[0].u.q) and mem2reg'd array elements (mem_q[3]) used to be dropped. They were then missing from read_state, forcing and the A3 BMC seed, so seeded BMC left them free and returned spurious witnesses. They're now kept, and verilator_path maps them to __BRA__N__KET__ / C++ indices. Earlier seeded-BMC results on designs with generate loops or arrays should be re-run.
2. orchestrator.py.
   • The predicate plugin now runs on batched and replay steps (it previously never ran during campaigns), and violations are tagged batch/bmc_replay.
   • New BMC goals: --bmc-goal reg=val, --bmc-goal-attempts, --bmc-goal-cooldown. Goals are tried before coverage targets on every stall, seeded from the current state, and retired once met or after the attempt budget.
3. cli.py. New options --bmc-goal*, --coverage-filter-module (plugin keep_toggle(hier, sig, bit, width, direction)) and --bmc-priority-target.
4. coverage_db.py. Priority targeting (--bmc-priority-target).
5. drivers/verilator.py, drivers/__init__.py.
   • Per-toggle-bin filter hook.
   • The toggle-name regex accepts array indices (x[0][3] = signal x[0], bit 3).

Why goals instead of coverage bins for bug flags: the dead-signal probe forces all-ones into registers, which marks sticky bug_*_q rise bins as covered even though no bug happened.

NoC status (probe on PULP FlooNoC)

A floogen 2×2 AXI mesh (XY routing) is in noc/.

What works:

• Verilator lints it from the original sources.
• sv2v cannot handle FlooNoC. It rejects function-local typedefs and type-checks inactive generate branches.
• Yosys + yosys-slang reads the unmodified sources: 10.9k cells, about 11.5k registers after clk2fflogic, 9 s. The BMC binary loads the model.
• Found in passing: FlooNoC HEAD's floo_vc_arbiter (VcCredit branch) connects cc_credit_counter.credit_init_i, but common_cells 2.0 renamed that port to clr_i. Any VcCredit configuration should fail to build.

Next steps, in order:

1. A read_slang frontend path in SymbFuzz, including merging slang's bit- and slice-split flop names back into logical signals.
2. Generalize the AXI shell into a generator for floogen meshes. All AXI checkers apply end to end, and the reorder buffers are a prime bug site.
3. A router-level shell around floo_router: XY routing-function compliance, flit conservation, wormhole framing, credit bounds and fairness. BMC is strongest at this level.
4. A global deadlock detector. It needs the inter-router links exported from floogen's top.
5. Traffic-pattern knobs (hotspot, transpose) and per-router turn / VC coverage.
6. A NoC bug benchmark.

Limitations: SymbFuzz is single-clock (GALS/CDC is out of scope for now), and mesh scale calls for router-level BMC plus seeded goals at mesh level.