RV64IMAC + Zicsr + U/S/M privilege, ACT4 compliance, riscv-formal verification - #7
Merged
Conversation
Added mermaid diagrams to illustrate CPU architecture and pipeline stages.
Enhance README with architecture flowcharts
Fixes real bugs found in the reused decoder/alu/register_file modules (SLT/SRA signedness, unmasked shift amounts, inverted regfile write-enable, x0 never hardwired, missing sign-extension on every immediate type including a 12-vs-13-bit zero-pad bug specific to S-type offsets, SLLI/SRLI/SRAI reading garbage shift amounts) and widens them to WORD_SIZE=64. Adds the RV64I-only instructions (LWU/LD/SD, the *W/*IW word-arithmetic family) and two new purpose-built memory modules (imem/dmem) with combinational reads and real byte-enable writes, since the existing Wishbone-attached wb4_sram.sv is registered and can't support single-cycle timing. design/core.sv is a full rewrite: a genuine single-cycle datapath (no FSM) wiring fetch/decode/execute/memory/writeback together in one clock edge-to-edge cycle. Verified with 7 testbenches (44 checks total, all passing under iverilog, zero warnings under verilator --lint-only -Wall) targeting the specific regressions above rather than just "does it run" -- negative immediates, the SLT/SRA fixes, the S-type offset bug via an independent load-path cross-check, JALR's LSB-clear, and ADDW/SRAW vs their 64-bit equivalents on identical inputs. Co-Authored-By: Claude Sonnet 5 <noreply@anthropic.com>
Matches the SoC's 64-bit Wishbone bus so LD/SD complete as single-beat accesses; adds sel_i-gated per-lane writes for narrower stores, and a simulation-only zero-fill so uninitialized reads show 0 instead of X.
Covers a full-word round trip, a byte-enable write leaving other lanes on the same line untouched, address-line isolation, and out-of-range address asserting err_o.
Minimal transmit-only peripheral for this milestone: TX_DATA (0x8000) prints via $write on write, TX_STATUS (0x8008) is hardwired ready. Registered 1-wait-state ack, matching wb4_sram's bus timing so the CPU doesn't need to know which slave it's talking to.
Drives the Wishbone port directly and checks tx_history[]/ tx_history_count against a two-character write sequence, plus sel-gating and TX_STATUS/TX_DATA reads.
Routes the CPU's single master port to wb4_sram or uart_tx by addr_i[15]. Both slaves are registered (1-wait-state), so which slave an in-flight request belongs to is latched at issue time rather than re-derived from addr_i when the delayed ack/data shows up.
Drives the CPU-facing port against two modeled 1-wait-state slaves with distinguishable fake responses, checking routing in both directions and that the slave-select latch updates correctly across back-to-back RAM/UART transactions.
Replaces the single-cycle datapath's private combinational imem/dmem with a 3-state FSM (fetch/exec/mem) that masters the shared Wishbone bus. decoder/alu/register_file are unchanged; only the sequencing is new: commit_now gates register writes and pc updates to the one edge each instruction actually retires on, and pc[2] selects which half of a 64-bit fetch line is the 32-bit instruction actually being executed. Fixes a duplicate-transaction bug found while bringing this up: cyc_o/ stb_o were tied to the registered FSM state, which drops one cycle later than a registered slave's ack becomes visible -- long enough for a slave to see cyc/stb still asserted and service the same request twice (caught via the UART printing "HH" for a single-byte write). Fixed by gating cyc_o/stb_o with !wb_ack_i so they drop combinationally the instant ack is observed.
Runs a hand-assembled program through the real core against real wb4_sram/uart_tx/wb_addr_decoder instances (not core_alu_ops_tb.sv and friends' private imem0 -- those no longer even compile against this core.sv). Proves multi-cycle fetch, a taken branch that actually skips, a RAM load/store round trip over the bus, and a UART write all work end-to-end through the address decoder.
Connects core's Wishbone master port to wb_addr_decoder, wb4_sram, and uart_tx -- the same wiring already proven in core_wb_tb.sv, promoted to a real module. No new logic, only connections. wb4_sram is instantiated at its default 4096-word (32KB) size, which is what wb_addr_decoder's addr_i[15] address split is derived from.
Instantiates soc directly and relies entirely on wb4_sram's own $readmemh of firmware/crt0.hex -- i.e. this exercises the actual toolchain-built firmware image, not a synthetic one. Checks the UART's captured tx_history against the expected "Hello, World!\n" bytes. Must be run from one level below the repo root so the hardcoded "../firmware/crt0.hex" path resolves.
Writes each byte of "Hello, World!\n" to the UART's TX_DATA register (0x8000) and halts with ebreak. Uses a flat, repeated li+sb sequence rather than a string constant walked in a loop, since this milestone links with a bare -Ttext=0x0 and no linker script, so there's no established convention yet for where a .data section would land.
--verilog-data-width=8 matches wb4_sram's memory[] element width (was 4, sized for the old 32-bit memory). --reverse-bytes=8 corrects objcopy's byte order: its verilog writer packs address-ascending bytes as the most-significant part of each hex token, which is backwards from the little-endian memory[i][7:0]==byte@lowest_address convention $readmemh needs here.
Two issues found by actually running the build for the first time: - objcopy's byte-reversal choked on .riscv.attributes (26 bytes, not a multiple of 8) when applied to the whole ELF. Added -j .text so only the section we actually want loaded into memory gets converted. - More importantly, --reverse-bytes=8 itself was wrong. Verified by hand against objdump -d output: objcopy's verilog writer already emits bytes in the order this design's memory[i][7:0]==byte@lowest_ address convention needs, with no extra flag. The previous commit's --reverse-bytes=8 was based on an untested assumption and was actually producing the wrong byte order; removed it. End to end result: soc_tb.sv now loads the real toolchain-built firmware and observes "Hello, World!\n" over the UART, 15/15 checks passing.
Instructions now go into a real wb4_sram instance (packed two per 64-bit word, matching core.sv's pc[2] half-select) instead of the old private imem0, which no longer exists. Also widens the halted-wait timeout from 50 to 150 cycles -- multi-cycle fetch/mem phases cost more edges per instruction than the single-cycle version did.
Same change as core_alu_ops_tb: instructions poked into a real wb4_sram instead of the now-gone imem0, timeout widened to 150 cycles.
Instructions poked into a real wb4_sram instead of the now-gone imem0/dmem0. This one's timeout increase is load-bearing, not just margin: 7 of its 12 instructions are loads/stores, which now cost 5 edges each instead of 1, and the inherited timeout of 50 was exactly at that budget with zero slack -- it timed out before the fix.
Instructions poked into a real wb4_sram instead of the now-gone imem0, timeout widened to 150 cycles. Caught a transcription bug in the repacking itself while verifying: memory[7] initially had idx14 and idx15 swapped into the wrong halves AND idx15's encoding wrong (accidentally duplicated idx13's addi x7,x0,222 instead of encoding idx15's addi x7,x0,111). Net effect was a stray jal landing straight on the "skipped by jal" sentinel instead of skipping it -- caught by x8/x9 failing their checks, fixed by correctly re-deriving the pairing by hand (word = idx/2, lower half = even idx, upper half = odd idx) instead of trusting the first pass.
Same change as core_alu_ops_tb: instructions poked into a real wb4_sram instead of the now-gone imem0, timeout widened to 150 cycles.
RAM spans 0x0000-0x7FFF, matching wb_addr_decoder.sv's addr[15] split; .text is placed first so it lands at 0x0 for core.sv's reset vector (needs crt0.o to be the first object passed to ld -- this script alone doesn't guarantee that). Also defines _bss_start/_bss_end/_stack_top for crt0.s to consume. Replaces the previous bare -Ttext=0x0 link, which had no .data/.rodata/.bss/stack story at all.
Sets up sp (top of RAM, per the new link.ld) and zero-fills .bss, then calls main() -- the two things any nontrivial C function needs before it's safe to call into C at all. gp is deliberately left uninitialized; see firmware/Makefile's -mno-relax for why that's safe here. The actual hello-world logic moves to firmware/hello.c. Previously this file wrote each UART byte directly since there was no linker script to trust; that's no longer necessary now that one exists and is verified.
Freestanding (no libc): writes each byte of "Hello, World!\n" through a volatile pointer to the UART's TX_DATA register at 0x8000. volatile is load-bearing -- without it the compiler could treat the repeated writes as dead stores and drop all but the last one. Compiled at -O0 deliberately: reloads everything from the stack on every loop iteration instead of keeping values in registers, which makes this a real stress test of crt0.s's stack setup rather than something an optimizer could reduce to barely touching the stack at all.
Adds a gcc compile step for hello.c and links it with crt0.o against the new link.ld (replacing the old bare -Ttext=0x0 link). Also now converts .rodata and .data, not just .text -- hello.c's string constant lives in .rodata and needs to actually reach memory. -mno-relax on both the assembler and gcc invocations, consistently -- see crt0.s's header for why that removes the need to set up gp.
300 cycles was sized for the old hand-written assembly (2 instructions per UART byte). The -O0 C build reloads everything from the stack on every loop iteration -- around 7 memory ops per byte, each costing 5 bus edges -- and legitimately needs closer to 9500 cycles to finish; caught as a mid-run timeout (printed "Hell" then stalled), not a functional bug.
CSR_ADDR (12 bits, instr[31:20]) and CSR_UIMM (5 bits, instr[19:15]) follow the same precedent SHAMT/WSHAMT already set here: same bit range as an existing field, but a different kind of value -- a zero-extended index/literal, never sign-extended.
CSRRW/CSRRS/CSRRC/CSRRWI/CSRRSI/CSRRCI, consecutive after the highest existing code (SRAW, 52) -- 53 through 58, 5 slots left before INSTR_CODE_SIZE needs to widen from 6 to 7 bits for M-extension.
Same SYSTEM opcode as ECALL/EBREAK, disambiguated by funct3 -- all 6 Zicsr funct3 values are nonzero while ECALL/EBREAK's existing mask forces funct3=000, so neither family can ever collide with the other. Mirrors the existing IMM_AL_INSTR_CREATE family's shape exactly.
…ne and core FSM Adds design/c_expand.sv, a new standalone combinational module expanding any 16-bit RV64 Zca compressed instruction into the equivalent standard 32-bit encoding decoder.sv already recognizes (plus an illegal-encoding flag) -- decoder.sv itself needs zero changes, since every compressed instruction is just a compressed encoding of an operation it already handles. Rewrites core.sv's fetch/FSM to support variable-length (2- or 4-byte) instructions: state_t widens to 3 bits with a new S_FETCH_HI state (appended last, preserving every existing state's numeric value so the 15 pre-existing hardcoded-state-literal testbench call sites keep working unmodified), a 4-way halfword mux replaces the old pc[2]-keyed 2-way mux, a dword-crossing 32-bit instruction triggers a second bus fetch, pc_plus_4 generalizes to pc_plus_len, and a reserved/illegal compressed encoding now plugs into the existing illegal-instruction trap mechanism from the U/S/M milestone. Verified via a verilator --lint-only -Wall --top-module core pass and design/c_expand_tb.sv (52/52 passing, covering every RV64 Zca mnemonic, every HINT case, and every reserved/illegal codepoint), plus a full regression gate confirming the state_t widening didn't disturb any existing testbench.
encode_c*() family (16-bit RVC encoders, independently written from c_expand.sv's own expansion logic) plus readability constants in testbench/riscv_encode.sv, and testbench/core_c_ext_tb.sv: a hand- assembled program mixing compressed and uncompressed instructions at varying alignments, deliberately placing one 32-bit instruction at pc[2:1]==2'b11 to force a genuine two-beat S_FETCH+S_FETCH_HI fetch (confirmed via a white-box visit check), plus a HINT (C.NOP), a C.J with a poison instruction at the skipped address, a real C.SW/C.LW round trip, a C.AND among popular registers, and a C.BEQZ that must not branch. 14/14 checks passing on Icarus and Verilator.
testbench/c_encode_check.s sweeps all 38 RV64 Zca mnemonics (every catalog instruction plus branch/jump fillers), using explicit c.xxx mnemonics for deterministic one-instruction-per-line coverage rather than relying on the real assembler's automatic compression of ordinary mnemonics under -march=rv64imac. c_encode_crosscheck_tb.sv compares the resulting golden hex against encode_c*(), confirming every hand-derived bit-scramble formula matches the real assembler exactly. 38/38 passing. Adds the matching ASFLAGS_C/c_encode_check.hex target (--verilog-data- width=2, since these are 16-bit words) to testbench/Makefile.
firmware/c_test.s is deliberately ordinary RISC-V assembly (no c.xxx mnemonics) -- under -march=rv64imac the real assembler automatically compresses most of it, confirmed against the real objdump output. A real jal-with-link paired with a real compressed return (c.jr) proves pc_plus_len against genuinely linked addresses, not hand-picked ones. testbench/core_c_toolchain_tb.sv wires it up mirroring core_a_toolchain_tb.sv's pattern. 6/6 checks passing on Icarus and Verilator. Adds the matching C_ASFLAGS/c_test target to firmware/Makefile.
testbench/soc_c_regression_tb.sv re-runs the existing SoC-level hello- world regression against firmware/hello_c.hex -- the SAME crt0.s/hello.c source, recompiled unmodified under real -march=rv64imac (no C.xxx mnemonics anywhere), so whatever compression happened is the real toolchain's own automatic instruction selection over ordinary code, not a hand-picked subset. A byte-identical 15/15 pass against the same expected UART output as soc_tb.sv proves the compressed and uncompressed builds of the identical source are behaviorally indistinguishable to this core -- the strongest available proof that general compressed-code density works end to end. This completes the RV64C (compressed instructions) milestone, and with it RV64IMAC + Zicsr + full U/S/M privilege modes on the single-stage in-order baseline: full regression (37/37 passing across every existing and new testbench), a fresh verilator --lint-only -Wall --top-module soc pass (clean), and a re-run of the ACT4 riscv-arch-test compliance suite (75/76, unchanged from before this milestone) confirming the new fetch/ FSM routing didn't disturb any existing instruction family. Also fixes verification/riscv-arch-test/run_act_tests.sh's design-file list (was missing the new c_expand.sv dependency) and updates README.md's roadmap section to reflect RV64IMAC + Zicsr + U/S/M as done, Sv39 next.
design/c_expand_tb.sv thoroughly unit-tests c_expand.sv's o_illegal detection in isolation, but nothing exercised the integration point -- core.sv's own is_illegal_instr C-extension term, trap_taken's redirect, mcause==2, and trap_val reporting the raw 16-bit halfword rather than instruction's inert placeholder. testbench/core_c_illegal_trap_tb.sv closes this: a genuinely reserved compressed encoding (16'h0000) traps through the real core, and a minimal M-mode handler (mepc+2, not +4 -- the faulting instruction is 16 bits) resumes execution exactly past it. 4/4 passing on Icarus and Verilator.
The C-extension milestone was only ever regression-checked against the original RV64IM+priv 76-test suite -- the official Zca compliance tests existed upstream the whole time but were never enabled (sail.json/ quantiumv-rv64im.yaml explicitly declared Zca unsupported since ACT4 setup predated the C milestone). Same gap exists for A-extension's Zaamo/Zalrsc, not yet closed. Enabling Zca and regenerating (550 targets, 0 build failures) surfaced 110 self-checking ELFs including all 32 RV64 Zca mnemonics as dedicated per-instruction compliance tests -- all 32 pass. Also 2 real FAILs, both root-caused via direct commit-by-commit tracing before being explained rather than assumed: - ExceptionsZc-00: confirmed via trace (zero illegal-instruction traps in ~1250 commits, test runs to full completion) this is fully accounted for by the already-documented, deliberate MISALIGNED_LDST:false gap -- the test is ~2400 lines of misaligned compressed load/store testing. Not a new bug. - S-00: confirmed via the same technique (zero compressed instructions, zero traps, in ~1600 commits) this has nothing to do with C at all -- a genuinely new finding, a pre-existing gap somewhere in CSR/ privilege mechanics (mret/sret/scause/sstatus/satp), never exercised by any prior test run. Flagged as a background task, not fixed here -- out of scope for this milestone. Also excludes Sm/ExceptionsS (both hang the Sail reference model when Zca is enabled -- same class of pre-existing Sail-side issue already documented for ExceptionsSm, confirmed Sm-00 is the identical test that worked fine before Zca). Result: 107 passed, 2 failed (both explained above), 1 known-gap unknown (the existing EBREAK sim-halt gap), of 110 total.
…R enforcement mstatus.MPRV was never cleared when MRET/SRET dropped privilege below M-mode, and mstatus.TSR (Trap SRET) was declared storage but never enforced -- both are genuine RISC-V privileged-spec requirements, found by root-causing the official riscv-arch-test ACT4 S-00 compliance failure via commit-by-commit trace + DWARF source correlation, not by inspection. Each fix independently unblocked a large chunk of S-00's combinatorial CSR test matrix (commit depth 1601 -> 5675 -> 8732 before hitting the next check). csr_file_priv_random_tb.sv's independent shadow model was out of sync with the MPRV rule too -- fixed to match, closing a real regression it would otherwise have masked. S-00 still doesn't fully pass ACT4: the next blocker is mstatus.FS reading hardwired-zero (this core has no F/D extension), which the privileged spec explicitly permits as one of two legal choices when S-mode exists without F -- confirmed via spec text, a full sail.json/ UDB config audit, and an empirical ELF regeneration against the already-correct MSTATUS_FS_LEGAL_VALUES:[0] declaration that produced an identical result. Not an RTL bug; left as a documented, accepted gap alongside the existing misaligned-access one.
…ding
Add a hand-written, spec-shaped RVFI (RISC-V Formal Interface) output
port list to core.sv, gated entirely behind `ifdef RISCV_FORMAL -- zero
effect on any normal build, confirmed via a full 38-testbench regression
with the change in place. Pure combinational taps off signals that
already drive the real commit (commit_now, reg_write_data, current_priv,
mem_paddr/mem_sel, etc.), matching RVFI's one-pulse-per-retired-
instruction model directly since commit_now already has that shape.
First slice: base-ISA (isa=rv64i) coverage only, no CSR trace ports yet.
verification/riscv-formal/quantiumv/: wrapper.sv + checks.cfg, a real
genchecks.py run against them generates all 56 expected rv64i checks
with zero errors, and sby successfully drives Yosys through elaboration.
Actual formal PASS/FAIL not reached yet -- blocked on two confirmed,
isolated Yosys-frontend gaps against this codebase's modern SystemVerilog
(nested macro token-pasting in decoder.sv's IS_INSTR, and `return {...}`
inside an automatic function in c_expand.sv) -- both reproduced in
isolation as genuine Yosys limitations, not RTL bugs. Full status,
workaround progress, and next steps documented in this dir's README.md.
…ntend gaps
Yosys's own built-in Verilog-2005-based frontend cannot parse two
constructs this codebase genuinely uses (decoder.sv's nested macro
token-pasting in IS_INSTR, c_expand.sv's `return {...}` inside an
automatic function) -- both confirmed via isolated repros as real Yosys
frontend limitations, not RTL bugs, and a newer built-in Yosys (0.62)
doesn't fix either on its own. Fix: read_slang (a separate, complete SV
frontend plugin) instead of read -sv, wired in via checks.cfg's
[script-defines]/[script-sources] since genchecks.py hardcodes its own
read command with no override hook. Confirmed: the full 7-file design
elaborates and optimizes with zero errors, zero RTL changes.
Also switched solver from the unconfigured default (boolector, not
installed) through z3 (25+ min with zero progress on the simplest
possible check, and a second concurrent z3 run crashed the WSL service
itself -- recovered cleanly, no data loss) to bitwuzla, which resolves
the identical check in ~2 minutes. bmc3 (ABC's native BMC) turned out
incompatible with these generated checks entirely (needs an option only
smtbmc/btor engines support).
End-to-end pipeline now genuinely works: a real BMC run completes and
returns a verdict. insn_add_ch0 currently FAILs with a real
counterexample, not yet root-caused -- leading hypothesis is a reset-
completeness gap in core.sv's C-extension capture registers
(crossed_q/instr_line_q/instr_hi_q have no rst branch by deliberate
design, an accepted non-issue for simulation testbenches but possibly
not for formal's adversarial initial-state exploration). Full status,
exact repro commands, and the concrete next investigative step are in
this dir's README.md.
…n constraint Root-caused the counterexample: wb_dat_s2m was left fully free, so the solver could pick fetch data that legitimately decodes as a compressed instruction. This core correctly advances pc by 2 in that case, but the base-ISA-only insn_add.v spec model always assumes pc+4 (fed from rvfi_insn, which reports the C-expanded 32-bit equivalent, not the raw 16-bit encoding) -- a formal-harness gap, not an RTL bug. Constrained wb_dat_s2m's low bits to rule out compressed encodings for the current isa=rv64i check scope, matching riscv-formal's own picorv32 wrapper precedent. Confirmed: insn_add_ch0 now passes at full configured depth (15) with bitwuzla -- the first check in this integration to pass end-to-end.
…branch/jump scope gap Ran all 56 generated isa=rv64i checks for the first time: 35 passed, 21 failed. Root-caused every failure via native witness replay. Branch/jump (8 checks): riscv-formal's spec models require strict 4-byte target alignment unless RISCV_FORMAL_COMPRESSED is defined. This core implements Zca unconditionally (IALIGN=16), so the RTL was correct and the check was too strict. Fixed with one checks.cfg define, verified via source read to be scoped to exactly those 8 models. Load/store (11 checks) -- two real core.sv bugs, both fixed: 1. core.sv never checked data-access alignment at all. mem_sel's shift had no carry into a second bus word, so a misaligned load/store silently truncated and committed corrupted data instead of trapping, which the spec disallows. Added a real misalignment trap (mcause 4/6, mtval = faulting address), gating mem_phase_needed. New coverage in testbench/core_misaligned_trap_tb.sv. 2. The ifdef RISCV_FORMAL RVFI memory tap mixed two incompatible addressing conventions (exact vs. aligned address). Fixed alongside a RISCV_FORMAL_ALIGNED_MEM checks.cfg define. Two second-order bugs surfaced while implementing fix #1, caught by the existing simulation regression rather than by riscv-formal: the misalignment check initially misfired during an AMO's S_AMO_WRITE phase (mem_paddr is repurposed for the modify value there), and the RVFI address tap initially truncated to 32 bits while the spec model computes a full 64-bit expected address from the solver's free rs1_rdata. Both fixed; full 38-testbench regression and verilator lint stay clean. 54/56 checks now pass. Remaining two (ill_ch0, reg_ch0) are open, understood formal-harness/solver-performance issues, not RTL bugs -- see verification/riscv-formal/quantiumv/README.md.
…pper guard exemption ill_ch0's stock check needs rvfi_insn==0 reachable (riscv-formal's canonical illegal-instruction test vector). Two things made it unreachable, both fixed: 1. core.sv's rvfi_insn reported the C-expanded 32-bit equivalent for compressed instructions. The RVFI spec requires the raw 16-bit encoding (zero-extended) instead -- a genuine spec-compliance gap, harmless everywhere else only because the insn_add_ch0-era wrapper guard kept is_compressed=0 for every other check's entire trace. 2. That same wrapper guard also excluded the specific bit pattern (16'h0000, C.ILLEGAL) ill_ch0 needs the solver to explore. Fixed the rvfi_insn tap, and added a per-check-instance macro (RISCV_FORMAL_CHECK_<checkch>) so the wrapper guard lifts only for ill_ch0, leaving it intact for every other check. Confirmed via a 5-check spot-check that nothing else regressed; full regression and verilator lint stay clean. 55/56 checks now pass. Only reg_ch0 remains open (solver timeout, not a counterexample) -- see verification/riscv-formal/quantiumv/README.md.
…crash) Neither bitwuzla (30min, no progress) nor z3 (crashed after ~2.5min, BrokenPipeError, no verdict) converge on reg_ch0. boolector -- the solver riscv-formal itself best-tests this specific check against -- isn't available as a built binary in this environment, only nix source recipes. Documenting exact attempts so the next pass tries boolector first rather than re-running solvers already shown not to work here.
…ecks now pass Built boolector from source (CaDiCaL SAT backend + btor2tools, plain upstream build, no nix CLI available in this environment to use nix build instead): reg_ch0's register-file-consistency property is the heaviest check in the suite, and neither bitwuzla (30min, no progress) nor z3 (crashed after ~2.5min) could produce a verdict at all -- not just slower, genuinely unable to converge. boolector solves it in ~18 minutes, confirming the check itself was always sound. genchecks.py has no per-check solver override hook, so checks.cfg keeps bitwuzla as the global default (dramatically faster for the other 55 checks); reg_ch0 needs a one-line manual solver swap on its generated .sby file, documented in the README alongside the boolector build steps. Full riscv-formal isa=rv64i sweep is now clean: 56/56 checks pass.
…ugs it was masking While prepping to scale checks.cfg to rv64imac, tested whether the RISCV_FORMAL_ALLOW_COMPRESSED guard (added for insn_add_ch0, narrowed for ill_ch0) could be removed entirely now that rvfi_insn correctly reports raw compressed encodings. It could -- but removing it and re-running the full 56-check isa=rv64i suite surfaced two real bugs the guard had been masking: 1. mepc/sepc were not WARL-masked (csr_file.sv). A CSR write like csrrw mepc, x1 didn't clear bit 0, so software could set mepc/sepc to an odd (architecturally invalid) address, which then loaded straight into pc on mret/sret. Fixed by masking bit 0 on the CSR-write arm (trap-entry arm already guaranteed even). Mirrored into csr_file_priv_random_tb.sv's shadow model. 2. commit_now had no !halted gate (core.sv). Its own comment already claimed this couldn't happen, but nothing enforced it: riscv-formal models wb_ack_i as a free input (standard convention), so the solver could assert a post-halt ack and push state back into S_EXEC, producing a bogus extra retirement. Fixed by adding !halted to commit_now's gate. Both verified via full regression + verilator lint before any formal re-run. All 56 checks then confirmed passing with the guard fully removed -- wrapper.sv/checks.cfg simplified accordingly (no RISCV_FORMAL_ALLOW_COMPRESSED/RISCV_FORMAL_CHECK_* machinery left). The actual rv64imac scale-up is still pending -- this was the first prep step, which mattered more than expected.
…o_wdata shift bug + spec-model amominu/amomaxu width bug Staged the rv64imac scale-up (AMO in isolation via a hand-built isa_rv64ia.txt + a patch enabling generate.py's non-LR/SC insn_amo() calls, then C via the upstream isa_rv64ic.txt manifest) rather than attempting the combined isa string directly -- no isa_rv64imac.txt manifest exists upstream and no LR/SC spec model exists at all. Real core.sv bug found and fixed: amo_wdata's byte-lane shift used amo_addr_q[2:0], but amo_addr_q is deliberately captured rounded to a dword boundary (low 3 bits always zero) -- silently corrupted .W AMO writes at any word-but-not-dword-aligned address. Predates this session's AMO RVFI work entirely; never caught before because no formal check or sim testbench exercised that exact address pattern. Fixed with a new amo_byte_off_q register holding the true unrounded offset. Spec-model bug found and fixed (in the patch, not the RTL): amominu_w/ amomaxu_w's unsigned comparison used the full sign-extended 64-bit rvfi_mem_rdata instead of a [31:0] slice, picking the wrong AMO "winner" even though the core's actual result was ISA-correct -- confirmed by hand-computing the expected result from the failing witness. C-extension: 30/30 PASS cleanly, first real exercise of the rvfi_insn raw-encoding tap and RISCV_FORMAL_ALIGNED_MEM against actual compressed-instruction spec models. M-extension (mul/div/rem) still in progress in the background -- div/rem needed a checks.cfg depth+memory fix (divider is 64 cycles/op), mul-family hit SAT-hardness neither bitwuzla nor boolector converge on even at a 20h budget. Documented as an open, actively worked issue in the README rather than blocking this commit on it -- already independently verified via simulation and the ACT4 riscv-arch-test compliance suite.
…ent upstream checker gap for trap-target CSRs
design/csr_file.sv: new o_mcause/o_scause ports (mirroring existing
o_mepc/o_sepc), plus four ifdef RISCV_FORMAL-only *_next combinational
ports -- transcriptions of each register's own always_ff priority-mux,
needed because RVFI wants both the pre-instruction (rdata) and
post-instruction (wdata) value in the same cycle rvfi_valid pulses, but
the real always_ff only makes the new value visible the following cycle.
design/core.sv: threads the 6 new csr_file0 ports through, adds the 16
new rvfi_csr_{mepc,mcause,sepc,scause}_{rmask,wmask,rdata,wdata} ports.
mstatus deliberately deferred (12 fields, 5 write sources -- its own
round). Full 39/40 regression + verilator lint (with and without
-DRISCV_FORMAL) confirm zero effect on normal builds.
checks.cfg: new [csrs] section (mepc/mcause/sepc/scause, `any` test) plus
the two-number [depth] entry check_cons()'s CSR code path actually needs
(missing this silently skips check generation with no error). Added
[assume !pattern] blocks scoping each check to the privilege level where
the CSR access legally succeeds, after witness replay confirmed the
generic `any` checker has no privilege-mode awareness at all and produces
spurious counterexamples on privilege-gated CSR access traps that this
core handles correctly.
A second, deeper issue remains open and undocumented as a known
limitation, not chased further: mepc/mcause/sepc/scause are also written
by the trap mechanism itself, a path the checker can't observe or
exclude, so a trap between a captured write and the next read breaks its
single-write-shadow model regardless of privilege scoping -- matches why
riscv-formal's own csr_spec 1.12 defaults don't test these CSRs via any
working check either. This logic is already verified via
csr_file_priv_random_tb.sv (14000 checks) and ACT4; only the additional
exhaustive-proof tier is blocked, not RTL correctness.
M-extension (mul/div/rem) checks are deprioritized per explicit direction
after mul_ch0 exhausted a 20h boolector budget with zero convergence
signal -- left running unattended in the background, no longer tracked.
…nd truth per repo owner)
The main<-dev merge (dev-wins conflict resolution) pulled in a non-conflicting hunk from main containing an OLDER, orphaned SLLW/SRLW/SRAW definition (4-bit, wrong values: 4'b1011/1100/1101) appended after dev's real, correct 5-bit definition (5'b01011/01100/01101). Verilog `define redefinition silently lets the later definition win with no error, which would have corrupted the actual ALU opcode encoding for RV64's word-shift instructions. Confirmed via diff against dev's pre-merge tree that this was the only file the merge changed beyond dev's original content -- every other conflicted file resolved to exactly dev's version.
There was a problem hiding this comment.
Pull request overview
This PR substantially expands the QuantiumV core’s implemented RISC-V feature set and strengthens verification by adding/expanding formal (riscv-formal) and compliance (ACT4 riscv-arch-test) infrastructure, along with new toolchain-built firmware/tests and supporting RTL decode/execute updates.
Changes:
- Add/extend verification infrastructure: riscv-formal wrapper/config and ACT4 runner/configs.
- Add toolchain-built firmware programs and new/updated simulation testbenches for privilege, M/A/C features and edge cases.
- Extend RTL decode/ALU/divider/defaults to support new instruction families and behaviors, plus update repo metadata/docs.
Reviewed changes
Copilot reviewed 62 out of 64 changed files in this pull request and generated 5 comments.
Show a summary per file
| File | Description |
|---|---|
| verification/riscv-formal/quantiumv/wrapper.sv | Adds RVFI wrapper around core for riscv-formal integration. |
| verification/riscv-formal/quantiumv/riscv-formal-amo.patch | Patch to riscv-formal insn generation to enable AMO modeling. |
| verification/riscv-formal/quantiumv/isa_rv64ia.txt | Adds AMO instruction manifest for rv64ia formal runs. |
| verification/riscv-formal/quantiumv/checks.cfg | Adds riscv-formal configuration, depths, defines, and Yosys script hooks. |
| verification/riscv-arch-test/run_act_tests.sh | Adds ACT4 ELF runner script driving act_runner_tb.sv. |
| verification/riscv-arch-test/quantiumv-rv64im/test_config.yaml | Adds ACT4 generation config for the QuantiumV target. |
| verification/riscv-arch-test/quantiumv-rv64im/sail.json | Adds Sail reference-model configuration for ACT4. |
| verification/riscv-arch-test/quantiumv-rv64im/rvtest_config.h | Adds DUT capability header for ACT4 environment. |
| verification/riscv-arch-test/quantiumv-rv64im/rvmodel_macros.h | Adds DUT-specific halt/tohost/IO/interrupt macros for ACT4 tests. |
| verification/riscv-arch-test/quantiumv-rv64im/quantiumv-rv64im.yaml | Adds Unified DB architecture config for ACT4. |
| verification/riscv-arch-test/quantiumv-rv64im/link.ld | Adds link script matching the core’s RAM-at-0 memory map. |
| verification/riscv-arch-test/quantiumv-rv64im/gcc-norelax-wrapper.sh | Adds wrapper forcing -mno-relax for ACT4 builds. |
| verification/riscv-arch-test/act_results.log | Adds a captured ACT4 run results log. |
| testbench/soc_c_regression_tb.sv | Adds SoC-level C-extension regression using hello_c.hex. |
| testbench/priv_encode_crosscheck_tb.sv | Adds assembler cross-check for priv-mode encodings (mret/sret/wfi/sfence.vma). |
| testbench/priv_encode_check.s | Adds assembler-only fixture for priv-mode encoding golden hex. |
| testbench/Makefile | Extends fixture-building targets for CSR/M/A/C/priv encode cross-checks. |
| testbench/m_encode_crosscheck_tb.sv | Adds assembler cross-check for all RV64M R-type encodings. |
| testbench/m_encode_check.s | Adds assembler-only fixture for RV64M encoding golden hex. |
| testbench/core_priv_toolchain_tb.sv | Adds toolchain-built privilege-mode end-to-end firmware test. |
| testbench/core_misaligned_trap_tb.sv | Adds end-to-end misaligned load/store trap test coverage. |
| testbench/core_m_w_edgecases_tb.sv | Adds end-to-end *W divide-by-zero edge case coverage. |
| testbench/core_m_toolchain_tb.sv | Adds toolchain-built M-extension end-to-end firmware test. |
| testbench/core_isa_coverage_gap_tb.sv | Updates ISA coverage-gap TB to remove ECALL fallthrough assumption. |
| testbench/core_c_toolchain_tb.sv | Adds toolchain-built C-extension end-to-end firmware test. |
| testbench/core_c_illegal_trap_tb.sv | Adds end-to-end illegal compressed instruction trap test coverage. |
| testbench/core_c_ext_tb.sv | Adds end-to-end compressed fetch/expand pipeline test program. |
| testbench/core_a_toolchain_tb.sv | Adds toolchain-built A-extension end-to-end firmware test. |
| testbench/c_encode_crosscheck_tb.sv | Adds assembler cross-check for Zca (compressed) encodings. |
| testbench/c_encode_check.s | Adds assembler-only fixture for Zca encoding golden hex. |
| testbench/act_runner_tb.sv | Adds generic ACT4 ELF runner harness for DUT execution and result extraction. |
| testbench/a_encode_crosscheck_tb.sv | Adds assembler cross-check for RV64A (atomics) encodings. |
| testbench/a_encode_check.s | Adds assembler-only fixture for RV64A encoding golden hex. |
| README.md | Updates top-level roadmap/status text to reflect new milestones. |
| firmware/priv_test.s | Adds toolchain-built privilege-mode verification program. |
| firmware/Makefile | Adds new firmware targets/flags for M/A/C/priv and compressed hello build. |
| firmware/m_test.s | Adds toolchain-built M-extension verification program. |
| firmware/c_test.s | Adds toolchain-built C-extension verification program. |
| design/wb4_sram_tb.sv | Strengthens SRAM TB aliasing check by writing a marker first. |
| design/divider.sv | Adds multi-cycle iterative divider for DIV/REM families. |
| design/divider_random_tb.sv | Adds randomized property test for divider correctness. |
| design/defaults/instructions_and_masks.sv | Adds masks/patterns for M/priv/A instruction families. |
| design/defaults/instruction_format.sv | Adds C_INSTR_SIZE definition for compressed instructions. |
| design/defaults/instruction_codes.sv | Expands instruction code space and adds new codes. |
| design/defaults/alu_ops.sv | Expands ALU op encoding and adds MUL/MIN/MAX ops. |
| design/decoder.sv | Extends decode table for M, privilege, and A instructions. |
| design/alu.sv | Extends ALU datapath for MUL/MULH*/MIN/MAX selection operations. |
| design/alu_tb.sv | Extends ALU directed tests for MUL and MIN/MAX correctness. |
| .gitignore | Ignores riscv-arch-test work output directory. |
| .gitattributes | Forces LF for .sh to avoid CRLF breakage under WSL/Linux. |
💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.
…-through First cache this core has ever had. Direct-mapped, physically-indexed/ physically-tagged (no virtual addressing yet), separate instruction and data caches per explicit design decision -- built now, ahead of the teammate's separate Sv39/MMU work landing. New modules (all in design/, matching existing flat-file convention): - icache.sv: read-only, no write path at all. Sequential multi-beat refill on miss (wb4_sram has no burst support). - dcache.sv: write-through, no-write-allocate. A store is always exactly one downstream beat, hit or miss -- never slower than the cacheless baseline. A store hit also updates the cached copy in place; a store miss doesn't allocate a line. - cache_complex.sv: thin wrapper routing core.sv's single time- multiplexed Wishbone port to whichever sub-cache applies (mirrors wb_addr_decoder.sv's own sel_uart_q latch idiom). No arbiter needed on the shared downstream port -- core.sv's FSM is single-issue, so I$ and D$ miss traffic structurally never overlaps. core.sv gained exactly one new port: wb_ifetch_o, a side-band signal (high during S_FETCH/S_FETCH_HI) letting the cache layer tell which logical stream a transaction belongs to, since the existing Wishbone master port doesn't otherwise carry that information. No other core.sv FSM changes -- every bus-driving state already tolerates arbitrary miss/refill latency. soc.sv: cache_complex spliced between wb_addr_decoder and wb4_sram, not before the decoder -- keeps uart_tx.sv's real side-effecting MMIO registers structurally uncacheable rather than requiring the cache to duplicate the decoder's own address-range test. Real bug found via icache_tb.sv's own out-of-range test hanging (not failing): wb4_sram.sv's ack_o/err_o are mutually exclusive, never asserted together, but the cache's error-handling originally checked mem_err_i nested inside `if (mem_ack_i)`, making the error path unreachable. Fixed in both caches. AMO/LR/SC need zero special-casing, confirmed empirically (not just argued): core_a_ext_cache_tb.sv directly probes dcache0.write_hit_q during an AMO's write phase and confirms it's always a cache hit, never its own refill, matching the address-identity argument that amo_addr_q is captured once and reused bit-identically for both phases. Verification: unit + randomized property tests for icache/dcache/ cache_complex, 3 curated cache-routed regression tests (C-extension dword-crossing fetch, M-extension divide-stall composition, the AMO invariant above), full existing 39-test regression clean, and -- strongest evidence the cache is externally transparent -- soc_tb.sv/ soc_c_regression_tb.sv pass completely UNMODIFIED with the real cache spliced in. Full-SoC verilator lint clean. Known, accepted limitation (documented in soc.sv's own header, deliberately not solved this round): no I$/D$ coherence for self-modifying code, since this ISA has no Zifencei. Today's firmware never self-modifies, so nothing currently exercises this, but it's a real gap if that ever changes.
…nd truth per repo owner) -- main rebased again
bitglitcher
self-requested a review
August 17, 2026 06:03
- checks.cfg: design/*.sv paths now @baseDir@-relative (matching wrapper.sv's existing convention) instead of an absolute Windows path; documented the sync step and verified via a real genchecks.py run (91 checks generated, every substituted path resolves to a real file). - checks.cfg: yosys-slang plugin path documented as a genuine external nix-store binary dependency, not a fixable path convention. - test_config.yaml: documented why compiler_exe must stay absolute -- confirmed via act's own config.py that this field resolves via shutil.which() relative to CWD, not config-relative like udb_config/ linker_script. - quantiumv-rv64im.yaml / sail.json: fixed backwards MISALIGNED_LDST / misaligned.supported comments. Confirmed via the UDB's own param definition that false correctly means "always excepts" -- the value was already right, only the polarity explanation was wrong. Re-ran the full ACT4 suite and full regression + verilator lint as a gate; no RTL touched, all clean. Along the way, confirmed the misalignment-trap RTL fix genuinely closed the old ExceptionsZc-00 gap (the deliberate misaligned load now traps correctly) but surfaced a separate, distinct comparison failure elsewhere in that same test -- documented as a new open item in project memory, not silently dropped.
bitglitcher
approved these changes
Aug 17, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Brings
mainup to the current state ofdev: the core now implements the full RV64IMAC ISA with Zicsr and U/S/M privilege modes, backed by real-toolchain compliance testing and a growing formal verification suite.rvfi_insnspec-compliance,mepc/sepcWARL masking,commit_nowgating,amo_wdatabyte-lane shift, MPRV/TSR CSR bugs)Test plan
RISCV_FORMAL)verification/riscv-formal/quantiumv/README.md)