Ibex RV32IMCB Exhaustive Verification Report

Structural enumeration with ExaVerif (ev) and synTagma

Author

Affiliation

SSCCS Foundation

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

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 764x 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 (ARMv8.4-A Firestorm)

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:

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	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.