Phase 2: Spike simulation backend and CVA6 XIF exhaustive verification

[metasmile]

Goal

Implement Spike-based ISA simulation backend for ev, enabling cross-validated exhaustive verification of CVA6 XIF custom instructions against actual RTL behavior.

Motivation

ev currently verifies only encoding-space constraints (field ranges, cross-field constraints). This is necessary but not sufficient. To compete with RISCV-DV — which generates random instruction streams and simulates them against real CPUs — ev must demonstrate that its exhaustive constraint combinations actually execute correctly on target hardware.

Roadmap

Milestone 1: Conditional field activation and R4 opcode support (#10)

The current flat constraint model cannot express CVA6 XIF's conditional fields (CUS_NOP has no operands) or R4-type encodings (CUS_ADD_RS3 with func2 field).

Deliverables:

• Field enable masks: constraints that activate/deactivate fields based on other field values
• Separate func2 field axis in ConstraintSpec
• Weighted distribution constraint (optional, for CUS_EXC)

Milestone 2: CVA6 XIF fixture update (#9 Milestone 1)

Update cva6_xif_ref.xif.yaml to match the actual cvxif_custom_instr.sv encoding table (funct3=000 → multiple ADD variants, CUS_NOP opcode 0x7B, CUS_ADD_RS3 func2 encoding).

Deliverables:

• Updated cva6_xif_ref.xif.yaml with correct encoding
• cross constraint updated for new funct3→funct7 mapping
• All tests passing

Milestone 3: Spike ELF batch simulation backend (#9 Milestone 2)

Implement ev simulate --target spec.xif.yaml that feeds each valid encoding to Spike via batched ELF + C harness.

Architecture:

ev simulate → YAML → expand → valid encodings
                               ↓
                    ELF Generator (packed encoding → ELF data section)
                               ↓
                    + C Harness (loop, decode, emulate coprocessor)
                    + cross-compile (riscv64-unknown-elf-gcc)
                               ↓
                    spike + pk → stdout per encoding pass/fail
                               ↓
                    parse → merge into evaluation results

Deliverables:

• src/synth/backends/spike.rs — Spike backend module
• ELF batch generator (minimal ELF crate or assembly)
• C harness template with instruction decode + coprocessor emulation
• ev simulate CLI subcommand (reuse the removed Simulate variant)
• Spike result parser integrated with TextReporter/JsonReporter

Milestone 4: Spike CI pipeline (#11)

Add Spike simulation step to .github/workflows/build-ev.yml using the updated Docker image with RISC-V toolchain.

Deliverables:

• Build and publish updated Docker image to GHCR
• CI step running ev simulate on a reduced fixture (< 1000 combos)
• Cross-platform validation (local + CI)

Milestone 5: Verification result output and LLM interpretation (#12)

Improve output formats and implement --interpret flag.

Deliverables:

• ev fact decode subcommand for human-readable Fact payload
• --interpret flag with LLM prompt template + API key management
• CSV / trace format via ReporterCapable trait

Dependencies

Milestone	Depends on
M1: conditional fields	—
M2: CVA6 fixture	M1
M3: Spike backend	M2
M4: Spike CI	M3
M5: output + LLM	M3 (optional)

References

• Target real RISC-V cores for exhaustive XIF verification #7 — Original real-core verification issue
• CVA6 XIF exhaustive verification — Spike simulation channel #9 — CVA6 XIF Spike channel (detailed Spike architecture)
• Conditional field activation and R4 opcode support #10 — Conditional field activation
• Spike CI pipeline integration #11 — Spike CI pipeline
• Verification result output and LLM interpretation #12 — Output formatting and LLM interpretation
• ssccs/poc/baremetal_riscv/simulation/ — Reference Spike integration
• cva6/verif/env/corev-dv/custom/cvxif_custom_instr.sv — CVA6 verification encoding