Publikation
Scalability Matters: Future-Proof Formal Verification of a RISC-V Arithmetic Logic Unit
Luca Müller; Mohamed Nadeem; Rolf Drechsler
In: 29th Euromicro Conference Series on Digital System Design (DSD) 2026. Euromicro Conference on Digital System Design (DSD-2026), September 2-4, Krakau, Poland, 2026.
Zusammenfassung
The open and royalty-free RISC-V Instruction Set
Architecture (ISA) defines base instruction sets with different
integer register widths, accounting for instructions with up to
128-bit operands. This poses challenges for verification as a
central part of Electronic Design Automation (EDA), since formal
methods that provide complete design coverage inherently lack
in scalability. To avoid pitfalls when it comes to building futureproof systems, Polynomial Formal Verification (PFV) aims to
combine these two factors, ensuring scalability for a growing
class of circuits, while preserving full coverage.
This work builds on these foundations, introducing a novel
approach to verify RISC-V Arithmetic Logic Units (ALUs).
Scalability is achieved by decomposition techniques, ensuring
provable complexity bounds. Different ALU implementations can
be integrated with minimal effort and individual instructions
are extracted independently of architecture, based solely on
the RISC-V specification. Theoretical examination shows that
polynomial complexity bounds can be established for all base
instructions of a RISC-V ALU. Experimental evaluation shows
that these theoretical polynomial complexity bounds lead to
practically scalable formal verification for an open-source RISCV ALU, enabling efficient verification for instructions with 32,
64 and 128-bit operands.