Column: Silicon systems design


proof. By contrast, formal verification produces explicit and auditable claims: a property is proven under defined assumptions for a specific design instance. RISC-V is increasingly deployed in


domains where such expectations apply, including automotive, industrial control and secure embedded systems. In these contexts, the question is no longer whether formal methods add value, but whether verification can be considered sufficiently robust without them.


Figure 3: Hybrid verification flow combining formal property verification and simulation-based coverage


interplay all expand the verification surface. Directed testing can’t realistically cover this cross-product, and even constrained- random approaches remain inherently statistical rather than exhaustive. At this point, the limits of simulation become structural rather than merely practical.


What formal verification actually changes Formal verification does not generate more tests – it changes the nature of the verification claim. Instead of asking whether a bug appears


under-sampled scenarios, formal verification evaluates whether a defined property holds for all possible behaviours within a constrained model. When a property is proven, the result is not probabilistic; it is exhaustive for that property. Tis distinction is most valuable in


bounded, control-intensive parts of the design: instruction decode correctness, CSR legality and WARL behaviour, privilege and security isolation, interface protocol compliance, and interrupt and exception handling. Tese areas are both tractable for formal methods and critical to overall system correctness. Open verification frameworks and


publicly available methodologies demonstrate how formal techniques can be applied systematically at the ISA and microarchitectural levels.


14 May 2026 www.electronicsworld.co.uk


Not replacement, but composition Formal verification does not replace simulation. It complements it. Te practical verification strategy for a RISC-V core is increasingly hybrid. Figure 3 shows this composition as


two parallel verification streams that converge at sign-off. Formal methods are most effective early in the flow and at architectural boundaries, where they can prove correctness of decode logic, control structures and key invariants. Simulation then provides broad behavioural coverage across pipelines, memory hierarchies and system-level integration, typically using a reference model or ISS. Formal techniques reappear later in the flow through equivalence checking and targeted interface-level verification. Te result is not duplication of effort,


but a stronger verification argument based on two fundamentally different forms of evidence. And the shiſt towards formal


verification is not only technical, but driven by assurance requirements, too. Standards such as ISO 26262 require


verifiable and traceable evidence of correctness, particularly for safety- critical hardware elements. Simulation coverage alone is inherently statistical and can be difficult to interpret as


The real challenge is discipline Te primary barrier to adoption is not tooling. It is an engineering discipline. Writing correct properties requires


architectural understanding and precision. Poorly defined constraints can invalidate proofs. Computational limits require careful decomposition of verification problems. Integrating formal verification into established flows requires methodological change rather than simple tool adoption. Most importantly, formal verification


requires a shiſt in mindset. Properties must be treated as first-class verification artefacts: specified, reviewed, maintained and owned alongside the design. Tis represents a different working model from traditional testbench-centric verification.


Beyond simulation, not without it Simulation will remain central to verification. It is the only practical method for exploring full-system behaviour at scale. However, the assumption that


simulation alone is sufficient is no longer valid for complex, configurable architectures such as RISC-V. Te industry is not moving away from simulation; it is moving beyond reliance on it as the sole source of confidence. For verification teams, the implication


is clear. Te objective is no longer limited to coverage closure. It is demonstrably correct, supported by both behavioural exploration and formal proof.


Tis column continues in next month’s edition of Electronics World.


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