fix: correct funct7/funct3 mappings + Zbt + new constraint types for Ibex RV32IMCB (#38)

[metasmile]

Summary

Cross-check rv32imcb.xif.yaml against ibex_decoder.sv OPCODE_OP case statement and fix all discrepancies. Closes #38.

Extends ev with new constraint types (bitmask, enable_set) and adds OP-IMM verification coverage.

Changes

Ibex RV32IMCB R-type fixture fixes

funct7	Before (main)	After	Fix
4	[1,5,6]	[1,4,5,6,7]	Added PACK(4), PACKH(7)
20	[1,2,4,5,6,7]	[1,2,4,5,6]	Removed ORC.B(7) — ORC.B is funct7=21
32	duplicate entry	single entry	Fixed YAML duplicate key
36	[1,5,6,7]	[1,4,5,6,7]	Added PACKU(4)
52	[1,5,6,7]	[1,5]	Removed GORC(6,7) — GORC is funct7=20
2..127 (bit1=1)	(missing)	[1,5] (64 entries)	Zbt ternary: funct7[1]=1 → CMIX/CMOV/FSL/FSR

524,288 total → 313,344 passed, 210,944 failed (accurately reflects Ibex decoder)

New: Ibex RV32IMCB I-type fixture

tests/fixtures/ibex/rv32imcb_imm.xif.yaml — models OPCODE_IMM decode space:

• RV32I base: ADDI(0), SLTI(2), SLTIU(3), XORI(4), ORI(6), ANDI(7)
• funct3=001: SLLI + SLOI + BSETI + BCLRI + BINVI + SHFLI + CLZ/CTZ/CPOP/CRC*
• funct3=101: SRLI + SRAI + RORI + SROI + GREVI + GORCI + FSRI (Zbt)
• 65,536 combinations, 55,616 passed, 9,920 failed

New constraint types

• bitmask: field & mask == value — bit-level field conditions

  • spec.rs: Bitmask variant + serde
  • registry.rs: BitmaskC + Check impl + builder registration
  • synth/mod.rs: SV assertion generation
  • synth/backends/spike.rs: C constraint generation

• enable_set: Like enable_mask but sets fields to specified values (not just zero)

  • compose.rs: domain expansion processing
  • Tests: bitmask_constraint (evaluate), expand_enable_set_forces_value_on_trigger_match (compose)

CI

• Restored ibex rv32imcb test in run.sh
• Added ibex rv32imcb imm test to run.sh
• cargo test: 77 passed, 0 failed
• bash run.sh: EXIT_CODE=0

Verification

rv32imcb:      524,288 total,  313,344 passed, 210,944 failed
rv32imcb_imm:  65,536 total,   55,616 passed,   9,920 failed

[metasmile]

Code Review — PR #39

General observations:

1. bitmask constraint — clean design, follows existing patterns precisely. Tests verify correctness. One consideration: negative mask values would produce surprising results (e.g. mask: -2). Consider adding a doc note or a positive-mask assertion in the builder if this becomes an issue.

2. enable_set constraint — correct generalization of enable_mask. Compose-time processing follows the exact same pattern. The NoopC check registered for runtime is the right approach. Note that enable_set currently runs BEFORE enable_mask in compose.rs; if both fire on the same trigger, enable_mask will overwrite enable_set's values with zeros. This is fine for non-overlapping use-cases today but could be surprising later.

3. rv32imcb.xif.yaml — Zbt entries (64 funct7 values with funct3∈{1,5}) are correct per ibex_decoder.sv RTL, but the cross constraint enumerates them individually. Since each entry is identical ([1, 5]), this is highly redundant. A future conditional constraint type (if funct7 & 2 == 2 then funct3 ∈ {1,5}) would eliminate 63 lines. Not a blocker for this PR.

4. rv32imcb_imm.xif.yaml — Important new coverage for OP-IMM space. The cross constraint maps funct3→funct7, which correctly allows funct3=0,2,3,4,6,7 to pass unrestricted. One note: this fixture currently has no test coverage in verify_large_fixtures — wait, it's in the run.sh now with _verify_check. Good.

5. _verify_check in run.sh — The awk parsing (/^passed:/ {print $2}) is portable across macOS and Linux. The VERIFY_FAILED accumulator correctly survives || true. However, this only checks verify_large_fixtures — the other _timed commands (cva6 xif ref r4, etc.) still have no assertion. Future work could extend this pattern to all fixtures.

6. C and SV backends — Bitmask and EnableSet codegen in both spike.rs and synth/mod.rs matches the existing patterns exactly.

7. Test count: 63 lib tests + 14 CLI tests = 77 passed, 0 failed. Two new tests (bitmask_constraint, expand_enable_set_forces_value_on_trigger_match) both pass.