PR: feat: CVA6 XIF exhaustive verification with Spike cross-validation #9#14
Merged
Conversation
- funct3/funct7 mapping updated to match cvxif_custom_instr.sv:
funct3=0: funct7∈{2,6,8} (ADD_MULTI, U_ADD, S_ADD)
funct3=1: funct7=0 (CUS_ADD)
funct3=2: funct7=96 (CUS_EXC)
- funct7 range extended to [0,127] to cover funct7=96
- Test expected value updated from 3072 to 2560
- 72 tests passing
Milestone 1 of #9
- synth/sim.rs: RunSimulation trait (Nexus-style capability interface) + SimulationResult, MockSimBackend + Optional capability traits: BatchCapable, ProfileCapable, CoverageCapable - spike.rs: SpikeBackend implements RunSimulation + ELF batch generation, cross-compile, Spike execution, result parsing - main.rs: resolve_sim_backend() with EV_SIM_BACKEND env var + default: MockSimBackend (no external tool needed) + EV_SIM_BACKEND=spike → SpikeBackend - reporter.rs: hash_evaluations() for simulation result content IDs - 73 tests passing, all CI checks clean
Problem: SpikeBackend's C harness had CVA6 funct3/funct7 encoding hardcoded, making the backend non-generic. Fix: - generate_c_constraints() converts each ConstraintSpec to C code - generate_c_constraint_expr() handles all 10 constraint types (range, even, eq, neq, lt, gt, le, ge, oneof, cross) - All fields included in encoding array with field index macros - get_spike_version() now respects EV_SPIKE_BIN env var - 73 tests passing, clippy 0 warnings
- _idx closure was unused (all field references use direct format strings) - _field_names parameter retained for future signature compatibility
- Yosys only supports SV 2005, assert property is SV 2012 - Changed to // synthesis translate_off + pattern - All constraint types updated (range, even, eq, neq, lt, gt, le, ge, oneof, cross) - Tests updated to match new output format - ev synth now works with Yosys for all fixture types
- ev verify --json → Fact { fact_type: "verification_result" }
- ev synth --json → Fact { fact_type: "synthesis_result" }
- ev simulate --json → Fact { fact_type: "simulation_result" }
- JsonReporter wraps VerificationReport in Fact payload
- SimulationResult implements From<&SimulationResult> for Fact
- Nexus FIH protocol compatible: same Fact type across all channels
- Data transfer layer ready for future Nexus integration
- 73 tests passing, clippy 0 warnings
Bug: Spike results indexed 0..valid_rows.len() but merge_results used static_evaluations indices directly, causing all valid encodings beyond the first 512 to be marked as 'no result'. Fix: - merge_results_with_indices maps Spike output indices back to original evaluation indices via valid_indices - C harness uses setbuf(stdout, NULL) to prevent buffered output loss - Verified: EV_SIM_BACKEND=spike on ssccs-poc Docker image → static=2560 passed, spike=2560 passed (identical) - Debug artifacts removed
- Fix misleading doc comment on generate_c_source (not public) - Use static const + const pointer in C code (correct const semantics) - Avoid C warning: const int64_t* passed to int64_t*
- Fact.payload is now opaque Vec<u8> (not serde_json::Value) - Consumers interpret based on fact_type (JSON, CBOR, binary) - Tests decode payload via serde_json::from_slice for verification - CLI tests updated to check fact envelope structure - External tool JSON requirement handled by conversion layer
Coverage gap analysis between ev exhaustive and riscv-dv random approaches. Documents complementary strengths and areas not yet modeled by ev.
- MAX_COMBINATIONS raised from 10M to 34M for 33M-combination space - cva6_xif_ref.xif.yaml: rs1/rs2/rd range [0, 31] (full RV32GPR) - 163,840 valid encodings (was 2,560 at [0,7]) - Spike simulation: 33M combos in 32s on M1 Max native - Slow test marked #[ignore], run with -- --include-ignored
- 33M combinations exhaustive (was 262K) - 196,608 valid encodings with full register range - Spike simulation channel: 196,608/196,608 pass - Fact payload as opaque blob (no embedded schema) - CVA6 verification suite encoding reference
…ec sheet - Replaces two outdated documents with one comprehensive reference - Covers architecture, encoding, fixture model, constraints, results - Updated comparison table with current figures (33.5M, 196K valid, 32s) - No Korean remaining
- Spike from source (riscv-isa-sim) - riscv-pk cross-compiled for RISC-V - gcc-riscv64-linux-gnu with aliases - Smoke test: ev simulate with mock backend in Docker build
- run.sh now includes 'ev simulate --target all_pass' in verify_fixtures - cva6_xif_ref description updated (full register range, correct funct7) - CI needs only 'bash run.sh' — all tests are centralized in run.sh - EV_SIM_BACKEND=spike activates real Spike simulation in CI
- Use << 'EOF' heredoc for Python snippets (no quote escaping issues) - Decode Vec<u8> payload before accessing fields - cva6_xif_ref (33M combos) moved to --verify mode only
- Use command substitution () instead of heredoc for Python parsing - Avoid pipe+heredoc conflict (heredoc eats stdin) - json output: parse Fact payload and display Total/Passed/Failed - simulate mock: display backend origin from Fact envelope - cva6_xif_ref (33M combos) excluded from default run
…ss constraint, simulate)
3 tasks
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
1 participant
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
Exhaustive verification of the CVA6 CV-X-IF reference coprocessor encoding space, with Spike RISC-V simulation cross-validation. Adds the
ev simulatesubcommand for ISA simulation, thecrossconstraint type for cross-field mapping, and theRunSimulationcapability trait for pluggable simulation backends.Changes
Core engine
funct3=0 -> funct7 in {2,6,8,32})serde_json::ValuetoVec<u8>blob (no embedded schema, ready for Nexus)assert propertywith// synthesis translate_off+$errorfor Yosys compatibilityCVA6 XIF verification
cva6_xif_ref.xif.yamlbased on actual CVA6 verification suite encoding tablesSimulation channel
EV_SIM_BACKEND=mock|spikeCLI
ev verify— static constraint verificationev simulate— ISA simulation verificationev synth— SystemVerilog generation + Yosys synthesisev verify --jsonoutputs Fact envelope (Vec<u8>payload)CI and packaging
run.shcentralized all tests; CI runsbash run.shTest Results
Related Issues