Exhaustive formal verification of hardware designs that implement cryptography extensions is crucial for security. However, scaling verification for designs with such large bit-widths often results in state-space explosions. In our DAC ’26 paper, we present the first formal verification of Marian, an open-source implementation of the RISC-V vector cryptography extensions. By leveraging proof modularization we were able to obtain an unbounded proof with and our systematic invariant identification methodology we achieve a 2.7x proof speedup. During the verification process, we also discovered a flaw in the ratified RISC-V specification.
Motivation
Critical components like cryptographic algorithms are frequently implemented in hardware to guarantee higher security assurance and better performance. Because hardware designs possess a deterministic state space, they can theoretically be exhaustively verified. Yet, scaling the formal verification of complex datapaths with large bit-widths remains an open challenge.
To achieve proof convergence, verification engineers typically add helper invariants. These are properties that are fast to prove and can be converted into assumptions to reduce the reachable state space for the remaining assertions. However, these invariants are highly design-specific, seldom published, and the field lacks a generic methodology to systematically identify and evaluate their effectiveness.
Invariant Identification Methodology
To evaluate the impact of invariants, we devise a methodology to categorize and test their impact. Based on common hardware functionalities, we defined 7 generic invariant categories: Regular Data, Datapath Control, Pipeline, Finite State Machine (FSM), Counter, Internal Control, and Handshake.
We provide tooling to automatically generate verification scripts that test all combinations of invariant groups. We further define metrics that enable the assessment of the effectiveness of the invariants. They measure, for example, the impact of invariant groups on proof speed and verification bounds.
Our invariant categories and metrics are discussed in detail in the paper.
Verification
We use an industrial sequential equivalence checker (Jasper C2RTL) to prove the RTL designs against the official C++ Spike simulator’s code, which we find to be modularizable per instruction. We prove the following main property:
“When providing the same inputs to the Spike model (C++) and Marian (HDL), and Marian signals calculation completion, the output of Marian’s crypto unit is equivalent to Spike’s output.”
Scaling Verification for Marian and VCRYPTU
When we first attempted to verify the entire Marian crypto unit, the proof stalled (8 clock cycles after 1 hour) due to design complexity. To resolve this, we employed two primary strategies:
- Modularization: We split the proofs to verify each Marian pipeline stage separately. Modularization alone allowed us to reach unbounded proofs. We further modularized the execution stage by verifying the execution units per individual instruction, speeding up verification by 1.28×.
- Identifying effective invariants: We manually identified 38 candidate invariants for Marian. Our evaluation method revealed that invariants on counters and handshake signals had the largest influence on improving proof bounds.
- Applying effective invariants: Invariants brought a further speedup of 3× for the modularized verification of the execution unit, with the largest speedup per instruction being 6.25x for the Shang-Mi 4 instructions*. Combining effective invariants with our modularization strategy resulted in a total proof speedup of 2.7× for Marian.
*The proofs were obtained by correcting for the wrong endianness (see our discovered vulnerability) in the equivalence property for SM4 by swapping the assignments that Jasper makes from the C++ variables to the RTL, so that it corrects for the mismatch in endianness. This was done to verify that computations are performed correctly, and only endianness is the problem, and to measure proof speedup.
Generalizing our results
To test the generalizability of our invariant identification methodology, we evaluated it on VCRYPTU, our own custom implementation of the SHA-256 RISC-V vector cryptography sub-extension. VCRYPTU uses a vastly different microarchitecture than Marian; for instance, it is not pipelined and embeds a crypto unit directly inside every vector lane. Proofs got stuck after 1 hour without invariants, and with most invariants added as well. However, with Counter invariants, we were able to obtain unbounded proofs within 43 seconds.
The most effective invariant categories
For both Marian and VCRYPTU, invariants on counters and handshakes were consistently the most impactful.
Counter invariants asserted, for example, that counters do not exceed a maximum or prove relationships between counters. Handshake invariants prove, for example, that the design correctly signals completion of a computation.
Invariants on datapath control signals, that, for example, choose which data path value is forwarded to a destination, were also effective.
Discovered Vulnerabilities
During our formal verification of the ShangMi 4 (SM4) instructions, we found a violation of our main equivalence property. Marian followed the endianness used in the RISC-V specification, but Spike did not. Thus, initially, it seemed that the Spike simulator code was wrong. However, the maintainers concluded that this was a flaw in the ratified RISC-V vector cryptography specification itself. The endianness for the SM4 vector instructions was not clearly defined in the standard. Due to our findings, the RISC-V specification is now being updated.
Paper and Code
“Leveraging Invariants for Scalable Verification of RISC-V Cryptography Extensions” will be presented at the 63rd ACM/IEEE Design Automation Conference (DAC ’26). We have open-sourced our verification scripts and evaluation artifacts.
Acknowledgements
This work was supported by a Qualcomm Innovation Fellowship and by the Swiss State Secretariat for Education, Research and Innovation under contract number MB22.00057 (ERC-StG PROMISE).
Frequently Asked Questions
Are the invariant assessment scripts reusable?
Yes, the verification generation scripts are open-sourced and are written in Python. You will need to adapt them to contain your verification tool’s commands.
Do the results generalize?
Yes, we tested our invariant assessment methodology on 2 very different designs, Marian and VCRYPTU.
Isn’t modularization sufficient to obtain proofs?
This is true for Marian, which is easily modularizable. Invariants speed up proofs additionally. For VCRYPTO we did not perform modularization and instead obtained unbounded proofs by using invariants.
What is the benefit of using invariants for regression speedup when we need to re-verify the invariants after design changes?
All invariants that still hold after the design change can be re-used. This can be quickly assessed, as their proof time is much faster than the main property’s proof time. However, you might find new invariants that can speed up proofs even further.
Can invariants slow down verification?
Yes, in some cases adding invariants can slow down the proof of the main property. Our invariant assessment methodology finds these cases.