PlanV Testimonial
Formal verification of CVA6’s MMU with model-driven property generation
Project background
PlanV applied formal verification to the Memory Management Unit (MMU) of the CVA6 RISC-V core within the PISTIs-V project of the ÖvIT programme sponsored by the German Cyberagentur. Because the verified seL4 microkernel depends directly on correct MMU behavior to enforce confidentiality and integrity guarantees, the MMU represented a security-critical hardware subsystem with high correctness requirements.
Working with LUBIS EDA, PlanV generated 80% of the baseline properties automatically within the first two weeks, allowing formal convergence to begin early and establishing a structured, model-driven methodology for the verification effort.
The challenge
The CVA6 MMU combines several demanding elements in one subsystem, including a Page Table Walker (PTW), a fully associative TLB, a second-level shared TLB, hypervisor support, replacement policies, complex flush semantics, and exception propagation. For PlanV, this meant that verification had to go beyond conventional testing and provide rigorous evidence for correct behavior.
At the same time, manually writing high-quality System Verilog Assertions for such a block would have created a significant bottleneck. The challenge was therefore not only to verify a complex subsystem, but to do so in a way that made formal verification practical, structured, and scalable.
LUBIS EDA contribution
LUBIS EDA supported PlanV with a model-driven property generation approach based on its Property Generation Framework. Starting from an abstract SystemC representation of the PTW, the framework generated a substantial portion of the initial SystemVerilog Assertions automatically and provided a structured property baseline aligned with the intended behavior.
For PlanV, this created a workflow in which automation covered structural and repetitive parts of the verification task, while manual refinement focused on implementation-specific details and microarchitectural nuances. This allowed the team to spend less effort on creating structural properties from scratch and more effort on refinement and corner-case analysis. The engagement combined formal methodology, tooling support, and structured execution to help PlanV move into formal verification with greater speed and confidence.
How the work was done
The collaboration followed a clear and repeatable pipeline: abstract behavior was modeled once in SystemC, translated into structured SVA, refined against RTL semantics, and then verified in Siemens Questa OneSpin Static Formal.
The PTW was especially well suited to this approach because of its FSM-oriented behavior. Where the design moved beyond this abstraction, for example in TLB-related structures and state-dependent output semantics, PlanV and LUBIS EDA applied targeted manual refinement. This created a hybrid methodology that balanced automation with expert engineering judgment.
Results achieved
Within the first two weeks, the team generated 80% of the baseline properties automatically from the SystemC model. This allowed formal convergence to begin early and shifted engineering effort away from writing structural properties from scratch and toward refinement and corner-case analysis.
Beyond the immediate project benefit, the collaboration established a structured and repeatable methodology for verifying security-critical processor subsystems. PlanV expanded its formal verification capability, built hands-on expertise in translating architectural intent into formal properties, and created a practical path for shortening ramp-up in future formal verification efforts.
The project also showed where model-driven property generation provides the strongest leverage: structured control logic such as page table walkers benefits significantly from automated scaffolding, while more table-centric structures still require manual treatment. For PlanV, this provided not only results for the MMU itself, but also a clearer methodology for future engagements.
Value for PlanV
The value of the engagement went beyond one verification task. It showed a practical way to introduce formal verification into a demanding security-oriented hardware context without relying fully on manual property development. It also created a reusable foundation for future verification work on similar subsystems and lowered the entry barrier for future formal verification efforts.
More broadly, the collaboration showed that model-driven property generation can reduce the barrier to formal verification while maintaining engineering quality. The workflow made formal verification more systematic, repeatable, and scalable.
What Our Partners Say
Feedback from industry leaders who have adopted model-driven formal verification methodologies with LUBIS EDA.