Goal
Update tests/fixtures/ibex/alu_ext.xif.yaml from the current "hypothetical" fixture to a spec based on the actual Ibex RISC-V core parameters and standard extensions.
Background
Ibex (lowRISC) does not implement the CV-X-IF custom instruction interface used by CVA6. Instead, Ibex supports standard RISC-V extensions (M, B, C, Zc, Zbkb, etc.) selectable via compile-time parameters. The current fixture (ibex/alu_ext.xif.yaml) is marked as "hypothetical Ibex ALU extension" but does not correspond to any actual Ibex configuration.
Approach
Rather than modeling a non-existent XIF interface, update the fixture to model Ibex's actual combinatorial parameter space: the set of valid RV32IMCB extension combinations and their instruction encoding constraints.
Ibex has the following key parameters (from ibex_pkg.sv):
RV32M: RV32MNone, RV32MSlow, RV32MFast, RV32MSingleCycleRV32B: RV32BNone, RV32BBalanced, RV32BOTEarlGrey, RV32BFullRV32ZC: RV32Zca, RV32ZcaZcb, RV32ZcaZcmp, RV32ZcaZcbZcmpRegFile: RegFileFF, RegFileFPGA, RegFileLatch
The fixture should model the constraint space of instruction encoding validity across these parameter combinations — demonstrating that ev can verify not just XIF custom instructions but also standard RISC-V extension configuration spaces.
Tasks
- Review
ibex/rtl/ibex_pkg.sv for parameter definitions and encoding constraints
- Review
ibex/doc/03_reference/instruction_decode_execute.rst for instruction decode rules
- Update
tests/fixtures/ibex/alu_ext.xif.yaml with real Ibex constraints
- Add to
run.sh verification if not already present
bash run.sh validation
References
ibex/rtl/ibex_pkg.sv — Parameter definitionsibex/doc/03_reference/instruction_decode_execute.rst — Decode/executeibex/dv/uvm/core_ibex/riscv_dv_extension/testlist.yaml — Existing test list
Goal
Update
tests/fixtures/ibex/alu_ext.xif.yamlfrom the current "hypothetical" fixture to a spec based on the actual Ibex RISC-V core parameters and standard extensions.Background
Ibex (lowRISC) does not implement the CV-X-IF custom instruction interface used by CVA6. Instead, Ibex supports standard RISC-V extensions (M, B, C, Zc, Zbkb, etc.) selectable via compile-time parameters. The current fixture (
ibex/alu_ext.xif.yaml) is marked as "hypothetical Ibex ALU extension" but does not correspond to any actual Ibex configuration.Approach
Rather than modeling a non-existent XIF interface, update the fixture to model Ibex's actual combinatorial parameter space: the set of valid RV32IMCB extension combinations and their instruction encoding constraints.
Ibex has the following key parameters (from
ibex_pkg.sv):RV32M: RV32MNone, RV32MSlow, RV32MFast, RV32MSingleCycleRV32B: RV32BNone, RV32BBalanced, RV32BOTEarlGrey, RV32BFullRV32ZC: RV32Zca, RV32ZcaZcb, RV32ZcaZcmp, RV32ZcaZcbZcmpRegFile: RegFileFF, RegFileFPGA, RegFileLatchThe fixture should model the constraint space of instruction encoding validity across these parameter combinations — demonstrating that ev can verify not just XIF custom instructions but also standard RISC-V extension configuration spaces.
Tasks
ibex/rtl/ibex_pkg.svfor parameter definitions and encoding constraintsibex/doc/03_reference/instruction_decode_execute.rstfor instruction decode rulestests/fixtures/ibex/alu_ext.xif.yamlwith real Ibex constraintsrun.shverification if not already presentbash run.shvalidationReferences
ibex/rtl/ibex_pkg.sv— Parameter definitionsibex/doc/03_reference/instruction_decode_execute.rst— Decode/executeibex/dv/uvm/core_ibex/riscv_dv_extension/testlist.yaml— Existing test list