Courtesy: Cadence
Are you still relying solely on simulation to validate your RTL design? Is there any more validation required?
Simulation has been a cornerstone of hardware verification for decades. Its ability to generate random stimuli and validate RTL across diverse scenarios has helped engineers uncover countless issues and ensure robust designs. However, simulation is inherently scenario-driven, which means certain rare corner cases can remain undetected despite extensive testing.
This is where formal verification adds significant value. Formal doesn’t just simply mathematically analyse the entire state space of your design; it checks every possible value and transition your design could ever encounter, providing exhaustive coverage that complements simulation. No corner case is left unchecked. No bug is left hiding. Together, they form a powerful verification strategy.
Why Formal Matters in Modern Validation
Any modern validation effort needs to take advantage of formal verification, where the apps in the Jasper Formal Verification Platform analyse a mathematical model of RTL design and find corner-case design bugs without needing test vectors. This can add value across the design and validation cycle. Let’s look at some standout Jasper applications: Jasper’s Superlint and Visualise can help designers to quickly find potential issues or examine RTL behaviours without formal expertise. Jasper’s FPV (Formal Property Verification) allows formal experts to create a formal environment and sign off on the IP, delivering the highest design quality and better productivity than doing block-level simulation. Jasper’s C2RTL is used to exhaustively verify critical math functions in CPUs, GPUs, TPUs, and other AI accelerator chips.
Jasper enables thorough validation in various targeted domains, including low power, security, safety, SoC integration, and high-level synthesis verification.
“The core benefit of formal exhaustive analysis is its ability to explore all scenarios, especially ones that are hard for humans to anticipate and create tests for in simulation.”
Why Formal? Why Now?
Here’s why formal verification matters now:
- No more test vectors or random stimuli. Formally, mathematically, and automatically explores all reachable states; verification can start as soon as RTL is available without the need to create a simulation testbench.
- Powerful for exploring corner-case bugs. Exhaustive formal analysis can catch corner case bugs that escape even the most creative simulation testbenches.
- Early design bring-up made easy. Validate critical properties and interfaces before your full system is ready.
- Debugging is a breeze. When something fails, formal provides a precise counterexample, often with the shortest trace, eliminating the need for endless log hunting.
- Perfect partnership with simulation. Simulation and formal aren’t rivals; they are partners. Use simulation for broad system-level checks, and Formal for exhaustive property checking and signoff of critical blocks. Merge formal and simulation coverage for complete verification signoff.
Conclusion
As RTL designs grow in complexity and stakes rise across power, safety, and performance, relying on simulation alone is no longer enough. While simulation remains indispensable for system-level validation, formal verification fills the critical gaps by exhaustively exploring every reachable state and uncovering corner-case bugs that would otherwise slip through. By integrating formal early and throughout the design cycle, teams can accelerate bring-up, improve debug efficiency, and achieve higher confidence at signoff. In today’s silicon landscape, the most robust verification strategy isn’t about choosing between simulation and formal—it’s about combining both to ensure no bug goes unnoticed and no risk is left unchecked.
