Ibex RV32IMCB Report

Structural enumeration with ExaVerif (ev) and synTagma

Author

Affiliation

SSCCS Foundation

Published

August 6, 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

Benchmarks

Fixture

References

Other Formats

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

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

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 32x speedup by eliminating all runtime constraint evaluation.

Scaling Analysis

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 (release build, this machine)

Figure 4: Complete benchmark data. struct_enum achieves 79x–32x 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:

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:

# 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	14x vs HashMap
CoordPath indexing	Combination addressing	5.2 ns	O(depth) = O(5)
CoordSpace sparse get	Valid encoding iteration	29.5 ms (2M space)	32x 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.