# Ibex RV32IMCB Exhaustive Verification Report

Structural enumeration with ExaVerif (ev) and synTagma

Author

Affiliation

SSCCS Foundation [](mailto:contact@ssccs.org)

[SSCCS Foundation](https://ssccs.org)

Published

August 3, 2026

Abstract

ExaVerif performed exhaustive verification of the lowRISC Ibex core’s register-register (OPCODE_OP) and register-immediate (OPCODE_IMM) ALU encoding spaces, covering the full RV32IMCB instruction set including Zbt (R4-type ternary instructions). The standard pipeline evaluates 524,288 combinations in 3.66 seconds. The Tagma-based structural enumeration evaluates the same space in 46.3 milliseconds — a 79x improvement — by generating only structurally valid combinations and eliminating all runtime constraint checks. Total valid encodings: 92,160 (R-type) plus 55,616 (I-type).

Code

[Github](https://github.com/ssccsorg/ev)

Benchmarks

[bench.rs](https://github.com/ssccsorg/ev/blob/main/benches/bench.rs)

Fixture

[Ibex RV32IMCB spec](https://github.com/ssccsorg/ev/blob/main/tests/fixtures/ibex/rv32imcb.xif.yaml)

References

[neXus](https://docs.ssccs.org/projects/nexus/)

[OpenHW](https://docs.ssccs.org/partnerships/openhw_integration.html)

Other Formats

[LLMs](https://docs.ssccs.org/projects/ev/ibex.llms.md)

## Verification Target

The Ibex core (lowRISC, OpenHW Group) implements the RISC-V RV32IMCB instruction set with an optional Bit-Manipulation extension. This verification covers the OPCODE_OP (0x33, register-register) and OPCODE_IMM (0x13, register-immediate) decode logic in `ibex_decoder.sv` under the RV32BFull configuration.

### R-type: funct7/funct3 decode (OPCODE_OP)

The decoder selects ALU operations through a 10-entry main case statement plus a Zbt ternary override for funct7 values with bit 1 set:

| funct7 | funct3 | Instruction class | Sub-extensions |
|----|----|----|----|
| 0 | all 8 | RV32I base | ADD, SLL, SLT, SLTU, XOR, SRL, OR, AND |
| 1 | all 8 | RV32M | MUL, MULH, MULHSU, MULHU, DIV, DIVU, REM, REMU |
| 4 | 1, 4, 5, 6, 7 | zbb + zbp + zbe | PACK, PACKH, SHFL, UNSHFL, BCOMPRESS |
| 5 | 1–7 | zbc + zbb | CLMUL, CLMULR, CLMULH, MIN, MINU, MAX, MAXU |
| 16 | 1, 2, 4, 5, 6 | zba + zbp | SH1ADD, SH2ADD, SH3ADD, SLO, SRO |
| 20 | 1, 2, 4, 5, 6 | zbs + zbp | BSET, XPERM_N, XPERM_B, GORC, XPERM_H |
| 32 | 0, 4, 5, 6, 7 | RV32I + zbb | SUB, SRA, XNOR, ORN, ANDN |
| 36 | 1, 4, 5, 6, 7 | zbs + zbb + zbe + zbf | BCLR, BEXT, PACKU, BDECOMPRESS, BFP |
| 48 | 1, 5 | zbb | ROL, ROR |
| 52 | 1, 5 | zbs + zbp | BINV, GREV |

### Zbt ternary (R4-type override)

When funct7 bit 1 is set, the decoder selects R4-type ternary instructions (CMIX, CMOV, FSL, FSR) for funct3 values 1 and 5. This adds 64 funct7 values with 2 funct3 values each.

### I-type: register-immediate (OPCODE_IMM)

The OPCODE_IMM decoder covers ADDI, SLTI, SLTIU, XORI, ORI, ANDI (any funct7) plus shift and bitmanip variants (SLLI, SRAI, RORI, BSETI, etc.) for funct3 values 1 and 5, including FSRI (funct7 bit 1 set with funct3=101).

## Exhaustive Verification Results

![](ibex_files/figure-html/fig-verification-scale-output-1.svg)

Figure 1: Ibex RV32IMCB encoding space: 524,288 raw combinations reduce to 92,160 structurally valid encodings. The remaining 54 unmapped funct7 values pass trivially per the cross-constraint semantics.

## Performance: Structural Enumeration vs Standard Pipeline

![](ibex_files/figure-html/fig-speed-comparison-output-1.svg)

Figure 2: Verification time comparison: struct_enum (Tagma-based) vs standard evaluate pipeline across four fixture sizes. At CVA6 R4 2M scale, struct_enum achieves 764x speedup by eliminating all runtime constraint evaluation.

## Scaling Analysis

![](ibex_files/figure-html/fig-scaling-output-1.svg)

Figure 3: Scaling behavior: evaluate runs in O(N) where N is the full space; struct_enum runs in O(V) where V is the structurally valid subset. The gap widens with space density: the sparser the valid space, the greater the speedup.

## Benchmark Results (ARMv8.4-A Firestorm)

![](ibex_files/figure-html/fig-bench-table-output-1.svg)

Figure 4: Complete benchmark data. struct_enum achieves 79x–764x speedup over the standard pipeline across real-world RISC-V verification targets.

## How It Works

A YAML specification describes the encoding space. The standard pipeline enumerates all combinations and evaluates each against constraints:

``` bash
ev verify --target tests/fixtures/ibex/rv32imcb.xif.yaml
```

The Tagma-based structural pipeline achieves the same result by encoding constraints into the enumeration space itself:

``` bash
# structural verification via Rust library API
# cargo bench -- struct_enum/ibex
```

### Structural vs Standard: the mechanism

| Aspect | Standard (`evaluate`) | Structural (`struct_enum`) |
|----|----|----|
| Combinations generated | **All** 524,288 | **Valid only** 92,160 |
| Constraint evaluation | 10 checks × 524,288 | **0** (structurally encoded) |
| Invalid detection | `check.allows()` → false | Vacant slot → 1.65 ns |
| Memory | 8 GB peak (Vec) | 0 (lazy iterator) |
| Time | 3.66 s | 46.3 ms |

## Comparison with synTagma Benchmarks

The struct_enum speedup mirrors synTagma’s core thesis: structural addressing eliminates hash-based lookup overhead.

| synTagma primitive | ev application | Measured | Advantage |
|----|----|:--:|:--:|
| Nonexistent prefix lookup | Invalid encoding detection | **1.65 ns** | 14.0Mx vs HashMap |
| CoordPath indexing | Combination addressing | **5.2 ns** | O(depth) = O(5) |
| CoordSpace sparse get | Valid encoding iteration | **1.69 ms** (2M space) | 846x vs evaluate |
| Axis projection | funct7/funct3 filtering | **46.3 ms** (524K space) | 79x vs evaluate |

## Limitations

### What this verification does not yet cover

- **Multi-cycle instruction modelling**: rol/ror and zbe/bdecompress/ bcompress complete in 2 cycles. The encoding space is verified, but pipeline timing is not.
- **RV32BBalanced vs RV32BFull**: The fixture assumes RV32BFull. Balanced mode disables zbc, zbe, zbp, zbr. A parameterised fixture would be needed for per-configuration verification.
- **RV32E register constraint**: Ibex optionally supports RV32E (16 registers). The fixture assumes 32-register RV32I.
- **Pipeline hazards**: Write-after-read hazards (rs1==rd) are not modelled at the encoding level.