Formal Verification of CVA6’s MMU with Model-Driven Property Generation
Accelerating Structured Formal Adoption at PlanV
Introduction
As part of the PISTIs-V project, part of the ÖvIT programme sponsored by the German Cyberagentur, PlanV undertook the formal verification of the Memory Management Unit (MMU) of the CVA6 RISC-V core. Because the verified seL4 microkernel relies directly on correct MMU behavior to enforce confidentiality and integrity guarantees, the MMU represents a critical hardware subsystem.
To address this challenge efficiently and systematically, PlanV adopted a model-driven property generation approach using LUBIS EDA’s Property Generation framework. The Property Generator is one of LUBIS EDA’s proprietary tools used within its formal verification services to support a more predictable formal sign-off. By starting from an abstract SystemC representation of the Page Table Walker (PTW), PlanV generated a substantial portion of the initial SystemVerilog Assertions (SVA) automatically and refined them into production-grade properties.
The result was a structured, scalable, and repeatable methodology for entering formal verification on a complex microarchitectural subsystem—combining automation with expert refinement.
Key outcomes
- 80% of baseline properties generated automatically within the first two weeks using model-driven property generation
- Early start of formal convergence, allowing engineers to focus on refinement and corner-case analysis instead of manual property construction
- Structured and repeatable methodology established for verifying security-critical processor subsystems
- Practical path to formal adoption combining automated scaffolding with expert refinement
The Challenge
The CVA6 MMU is not a trivial block.
It includes:
- a Page Table Walker (PTW) responsible for virtual-to-physical translation
- a fully associative Translation Lookaside Buffer (TLB)
- a second-level shared TLB
- hypervisor support (ASID/VMID handling, multi-stage translation)
- replacement policies (PLRU, LFSR)
- complex flush semantics (SFENCE.VMA, HFENCE.VVMA, HFENCE.GVMA)
- exception propagation and access error handling
Because seL4’s security guarantees depend on correct address translation and protection enforcement, the MMU had to be verified rigorously, not just tested.
However, writing high-quality SVA properties for such a subsystem can become a bottleneck. Manual property authoring for large state machines and protocol logic is time-consuming and error-prone. PlanV therefore looked for a way to bootstrap formal verification without sacrificing rigor.
Model-Driven Property Generation
The SystemC code focused on intended behavior rather than implementation detail, creating a clean semantic layer above RTL.
These cases were manually refined or extended in SVA to accurately reflect RTL semantics.
This hybrid workflow proved effective, allowing automation of structural and repetitive properties, and requiring only manual expertise to address microarchitectural nuances.
TLB and Shared TLB
Unlike the PTW, the TLB and shared TLB are not naturally expressible as simple FSMs, being essentially memory arrays surrounded by a comparator.
The contrast between PTW (FSM-friendly) and TLB (table-centric logic) provided valuable insight into where model-driven generation accelerates formal adoption most effectively
Verification Environment
The generated and refined SVA properties were verified using Siemens Questa OneSpin Static Formal.
The property suite covered safety properties (state integrity, one-hot encoding), transition correctness, error and exception propagation, replacement policy correctness, address translation consistency and liveness guarantees.
The environment was structured so that PTW, TLB, and shared TLB could be verified independently, supporting modular reasoning and incremental convergence.
Impact
This shifted effort from “property creation” to “property refinement.”
Within the first two weeks, the team generated 80% of the properties automatically from the SystemC model, allowing the team to begin formal convergence early, focusing engineering effort on refinement and corner-case analysis rather than constructing structural properties from scratch.
The engagement followed a clear pipeline: abstract behavior modeled once in SystemC, automated generation of structured SVA, targeted RTL refinement, and systematic formal convergence.
This repeatable path lowers the barrier for future subsystems that exhibit FSM-like control behavior.
This scoping strategy improved verification tractability without sacrificing correctness goals.
This balanced methodology reinforced internal confidence in the results.
Strategic Outcome
Through this engagement, PlanV demonstrated the feasibility of applying a model-driven formal methodology to a complex RISC-V subsystem central to system security.
With this project, PlanV expanded its formal verification capability by integrating LUBIS EDA’s model-driven property generation framework into its engineering practice. The team built hands-on expertise in translating architectural intent into structured formal properties and guiding formal convergence effectively. This accumulated experience lowers the entry barrier for future formal verification efforts and shortens the ramp-up phase for subsequent security-critical subsystems. The The Property Generator is a simple VSCode plugin that’s ready to use right away. No complicated installations or changes to your infrastructure are required.
For PlanV, the important outcomes are a reinforced formal verification capability on critical hardware blocks, the possibility to establish a structured, reusable methodology and the strengthening engineering credibility in security-oriented projects.
In a nutshell, the CVA6 MMU verification effort illustrates a pragmatic path toward broader formal adoption, starting with modeling the intent once, and refining the generated structures manually, to allow the verification environment to scale methodically.
This approach enables engineering teams to move beyond ad-hoc property writing and toward a disciplined, model-driven formal practice—bringing rigorous verification closer to mainstream hardware development.
PlanV’s understanding of secure processor design combined with LUBIS EDA’s property generation framework enabled a systematic and scalable entry into formal verification.