R4 format support: func2 field axis for ADD_RS3

[metasmile]

Goal

Add R4-type instruction format support to ev's constraint model. Required for CVA6 XIF's CUS_ADD_RS3 which uses a func2 field (bits [26:25]) separate from funct7.

Background

CVA6 cvxif_custom_instr.sv defines get_func2() (line 87-91) which returns a 2-bit field (func2[1:0]) for R4_FORMAT instructions. CUS_ADD_RS3 uses func2=01. In the current cva6_xif_ref.xif.yaml, this is approximated as funct7=32, which is incorrect — the hardware encoder places func2 in bits [26:25], not in funct7's bit [25].

Deliverables

1. Add func2 field to VerificationSpec / ConstraintSpec as a separate axis
2. Update src/synth/backends/spike.rs C harness to assemble R4 instructions in the correct bit layout:
   • R4 format: {rs3[4:0], func2[1:0], rs2[4:0], rs1[4:0], funct3[2:0], rd[4:0], opcode[6:0]}
3. Create a minimal R4 test fixture (e.g., r4_test.xif.yaml) to validate encoding
4. Update cva6_xif_encoding.xif.yaml to include funct7=32 (ADD_RS3) with proper func2=01

References

• cva6/verif/env/corev-dv/custom/cvxif_custom_instr.sv — get_func2() definition
• cva6_xif_ref.xif.yaml — current funct7=32 approximation
• ibex/vendor/google_riscv-dv/src/isa/riscv_b_instr.sv — R4_FORMAT binary encoding: {rs3, func2, rs2, rs1, funct3, rd, opcode}

Parent Issue

#13 — Phase 2: Spike simulation backend and CVA6 XIF exhaustive verification