Efficient Coverage Optimization with Formal-Guided Testcase Generation in UVM Verification

Inhalt:
Processor verification faces significant challenges in statespace explosion and test coverage limitations, particularly in complex micro-architectures. Formal verification provides precise correctness guarantees but is constrained by computational overhead and scalability issues. Conversely, simulation-based approaches, including constrainedrandom verification and fuzz testing, provide scalability but often lack systematic guidance to effectively cover critical design regions and rarely exercised state transitions. To overcome these challenges, we propose Formal-Guided Test Sequence Optimization (FGTSO), a framework that integrates formal verification with simulation to systematically target coverage holes and enhance verification efficiency. FGTSO mitigates false alarms by refining formal assumptions and resolving black-box (BBOX) limitations through abstraction modeling. By continuously aligning formal and simulation environments, FGTSO reduces test redundancy while enabling precise corner-case exploration. This approach enhances verification completeness, efficiently covering hard-to-reach design behaviors that traditional methodologies often overlook. Experimental results on the CVA6 RISC-V core show that FGTSO achieved 99.91% branch coverage within 8 days, which is 4.41% higher than HyPFuzz’s 95.5%, effectively covering 98% of the previously uncovered regions. Furthermore, within 10 days, FGTSO achieved 100% coverage across all key metrics, including line, toggle, condition, and branch coverage. These results validate FGTSO’s ability to identify complex corner-case behaviors that traditional methods fail to reach, significantly enhancing verification completeness and efficiency.