Column: Silicon systems design
The growing role of formal verifi cation in RISC-V design
By Mike Bartley, CEO, Alpinum S
imulation has served the semiconductor industry well for decades, but the expanding state space of modern processors, compounded by the
compositional freedom of the RISC-V ISA, is exposing fundamental limits in what stimulus-driven verifi cation can prove. Formal methods are no longer a research curiosity. T ey are becoming a practical, oſt en mandatory layer in the verifi cation fl ow for designs where correctness is non- negotiable.
The simulation ceiling is now visible Every experienced verifi cation engineer understands the state-space problem. Even a modest processor design has a reachable state space far beyond what any regression campaign can exhaustively explore. Coverage metrics help quantify progress, but they do not remove uncertainty. T ey measure what has been exercised, and help guide validation eff orts; they do not prove that the unexplored remainder is safe. Figure 1 shows a conceptual view of the
central asymmetry. T e leſt side represents sampled execution paths explored through simulation, whilst the right side represents the full reachable state space considered under formal analysis. Simulation can cover many important
scenarios, but it still leaves unvisited regions of the state space. Formal verifi cation instead evaluates whether a
12 May 2026
www.electronicsworld.co.uk
Formal methods are becoming a practical, often mandatory layer in the verifi cation fl ow for
designs where correctness is non-negotiable
stated property holds across all reachable states within a constrained model. T is represents a stronger claim, particularly in corner cases that conventional regressions are least likely to expose. T e bugs that escape simulation are
rarely simple functional errors. T ey typically arise in interactions: privilege transitions under rare timing conditions, pipeline hazards triggered by specifi c instruction sequences, or protection- boundary violations that appear only under unusual combinations of state. T ese are precisely the failures that are hardest to detect and most expensive to resolve late in the programme lifecycle. Industry analysis consistently shows that defects identifi ed later in the fl ow incur signifi cantly higher resolution costs. RISC-V multiplies the verifi cation
problem: It is not only larger, it is structurally more open. A fi xed ISA constrains the verifi cation problem. RISC-V expands it. T e base ISA is only the starting point.
Designers combine extensions, confi gure privilege modes, implement CSR behaviour and, increasingly, introduce custom instructions. T e unprivileged architecture defi nes
the base ISA and a growing set of standard extensions, whilst the privileged
Page 1 |
Page 2 |
Page 3 |
Page 4 |
Page 5 |
Page 6 |
Page 7 |
Page 8 |
Page 9 |
Page 10 |
Page 11 |
Page 12 |
Page 13 |
Page 14 |
Page 15 |
Page 16 |
Page 17 |
Page 18 |
Page 19 |
Page 20 |
Page 21 |
Page 22 |
Page 23 |
Page 24 |
Page 25 |
Page 26 |
Page 27 |
Page 28 |
Page 29 |
Page 30 |
Page 31 |
Page 32 |
Page 33 |
Page 34 |
Page 35 |
Page 36 |
Page 37 |
Page 38 |
Page 39 |
Page 40 |
Page 41 |
Page 42 |
Page 43 |
Page 44
