PR: feat: add neq/lt/gt/le/ge/oneof constraints, fixtures, axis fix, CLI refactor #7

[metasmile]

Summary

Three-phase pipeline hardening plus CLI refactor. Fixes the critical axis ordering bug where BTreeMap alphabetical sorting caused numeric axis indices to mismatch YAML field declaration order.

Changes

Phase 1 — Bug fixes

• Removed duplicate FieldDomainCheck struct (dead code)
• Removed redundant build_all re-invocation in failure path
• Added overflow guard and MAX_COMBINATIONS (10M) limit to expand_all

Phase 2 — New constraint types + RISC-V fixtures

6 new constraint types: neq, lt, gt, le, ge, oneof

Two real-world RISC-V core fixtures:

• ibex_alu_ext.xif.yaml — 456 combinations, oneof + neq constraints
• cva6_xif_mac.xif.yaml — 32,768 combinations, signed accumulator

Phase 3 — Axis ordering fix

• ConstraintSpec: axis: usize → field: String (field-name references)
• All YAML fixtures and tests updated accordingly

CLI refactor

• ev check → ev verify (static constraint verification)
• ev simulate --target (Spike backend, placeholder)
• ev synth --target (standalone SV synthesis, formerly --synth flag)
• run.sh simplified: default = full pipeline, --demo flag for SSCCS demo only

Test Results

72 passed, 0 failed

[metasmile]

Code Review Summary

spec.rs

The Cross variant uses mapping: HashMap<i64, Vec<i64>> which serde handles natively — clean YAML representation. All internal Check structs now store field_name instead of numeric axis indices, making describe() output human-readable.

registry.rs

ConstraintBuilder signature changed to accept an axis_of map. build_all now takes the field map and calls build_axis_index internally — registry consumers only deal with field names. Two prior bugs removed: duplicate FieldDomainCheck and redundant build_all re-invocation. CrossC::allows() uses unwrap_or(true) for unmapped keys, matching the design intent that unmapped field_a values leave field_b unrestricted.

evaluate.rs

Removed duplicate field domain validation (the FieldDomainCheck struct was never reached because the inline loop returned early). build_all re-invocation replaced with direct check.describe() for failure reasons. Six new constraint unit tests cover pass/fail boundary conditions. The cross_constraint test covers mapped pass, mapped fail, and unmapped pass across 3×4 = 12 combinations.

synth/mod.rs

sv_constraint_assertion no longer needs field_names lookup — every constraint variant includes the field name directly. Cross constraint generates SystemVerilog inside assertions: (funct3 == 0) -> (funct7 inside {0}).

main.rs

Check renamed to Verify, --synth flag removed, Synth subcommand added. run_synth() and print_synthesis_report() extracted to eliminate code duplication. Simulate subcommand removed to avoid exposing unimplemented!().

CLI tests

All ev check → ev verify. Three tests added: synth_help_succeeds, synth_text_with_mock_backend, synth_json_with_mock_backend, verify_cva6_xif_ref_fixture. verify_help_mentions_synth removed since synth is now a separate subcommand.

cva6_xif_ref.xif.yaml

Based on actual CVA6 core RTL (cvxif_instr_pkg.sv analysis). Uses real field names (funct3, funct7) with oneof + cross to model the coprocessor's hierarchical encoding. rs1/rs2/rd reduced to 0..7 to stay under MAX_COMBINATIONS.

run.sh

--ci mode removed (default execution is identical). cva6_xif_ref verification added to verify_fixtures.

Overall

All changes are consistent with the existing architecture (registry builder pattern, capability traits). 72 tests pass with zero clippy warnings. The Cross constraint is the first practical demonstration of SSCCS Field Composition principles applied to real RISC-V XIF encoding verification.