PR: fix: structural enumeration correctness and RTL-derived CVA6 verification #43

[metasmile]

Summary

Fixes structural enumeration correctness and re-derives the CVA6 fixtures from the actual hardware decoder, making the reported numbers reproducible and honest.

Changes (9 commits)

• fix: structural enumeration emits only cross-valid combinations — StructuralEnum had a cross-constraint wrap bug (emitted stale child values after a parent advance; funct3=2 was emitted with funct7=0 instead of 96). Rewritten as a topologically ordered odometer with O(1) fix_suffix via precomputed first-valid indices. Now emits exactly the valid set (regression-tested).
• fix: derive CVA6 fixtures from the hardware decoder mask table — fixtures cross-checked against cvxif_instr_pkg.sv / instr_decoder.sv at CVA6 commit 6544a714c. Accepted custom-3 space: funct3=000/funct7=0 (NOP), funct3=001/funct7 in {0..4} (ADD family). Full: 196,608 valid (0.6% density); R4: 2,560.
• fix: spike backend cross-checks assembled words — the generated C program now compares its assembled word against the Rust-computed reference; reason strings corrected ("constraint re-check failed" / "instruction word mismatch"); doc comment states Spike never executes custom-3 (illegal in base ISA).
• test: structural enumeration equivalence and wrap regression — 5 regression tests in /tests.
• bench: full-space CVA6 group + validity guard + reference documentation — cargo bench -- cva6_full; struct_enum_validity guard; the suite is now the performance reference (fixture table, methodology, O(N) vs O(V)).
• docs: CVA6 master report + homepage — decoder mask table, DV/decoder divergence, counting semantics, standard verification environment alignment, reference links.

Measured results (release build, this machine)

Fixture	Raw	Valid	evaluate	struct_enum	Speedup
CVA6 full	33,554,432	196,608	18.0 s	18.5 ms	~973x
CVA6 R4	16,384	2,560	4.93 ms	247 µs	20x
Ibex	524,288	92,160	3.66 s	46.3 ms	79x

Same-language (Rust release, criterion) baseline: the ratio is the O(N) vs O(V) enumeration-strategy gain, not a language effect.

Finding for the CVA6 team

The DV class (cvxif_custom_instr.sv) generates encodings the reference coprocessor decoder rejects: CUS_U_ADD (funct3=000/funct7=2), CUS_S_ADD (funct7=6), CUS_ADD_MULTI (funct7=8), CUS_EXC (funct3=010). Documented in the report.

Quality

• 92 tests pass (73 lib + 14 CLI + 5 structural), clippy and fmt clean.
• Reproducible: cargo bench -- cva6_full on the committed fixtures.
• PR-level review done; two minor nits noted (generated C calls assemble_instr twice when a layout exists; cyclic cross constraints fall back silently).

Related

• Issue Structural enumeration correctness and verification claim accuracy #43 (this work)
• Issue Execute accepted CVA6 custom-3 encodings through the standard tandem simulation flow #44 (follow-up: execute accepted encodings through the CVA6 veri-testharness,spike tandem flow)