Presentation
Janus – twin-faced debugging - Anecdotes from formal, security & timing exception verification
DescriptionWe present our experience with a custom flow named Janus, which enhances the debugging process by converting formal verification traces into UVM tests, effectively bridging the gap between formal verification and dynamic simulation. This dual approach improves bug detection and reduces debug efforts. By leveraging formal verification (FV) to generate focused, concise trace data, Janus translates these traces into UVM-based simulation tests, enabling enhanced debugging and comprehensive coverage generation.
This technique is demonstrated in two key applications: security controller IP with taint verification and LPDDR PHY controllers with timing exception handling. For the security controller, Janus uses formal verification to identify potential taint propagation vulnerabilities, which are then validated through simulation to ensure secure data handling. For the LPDDR PHY controller, timing exceptions—such as false path and multi-cycle path constraints from the user's SDC file—are verified through formal methods, while the translated UVM tests simulate realistic operational conditions to validate the system.
By integrating formal verification with UVM simulation, Janus significantly improves debugging efficiency (by a factor of 4 on an IP), while also providing detailed coverage generation. For the SDC verification, Janus successfully identified and verified 250+ failing exceptions in simulation.
This technique is demonstrated in two key applications: security controller IP with taint verification and LPDDR PHY controllers with timing exception handling. For the security controller, Janus uses formal verification to identify potential taint propagation vulnerabilities, which are then validated through simulation to ensure secure data handling. For the LPDDR PHY controller, timing exceptions—such as false path and multi-cycle path constraints from the user's SDC file—are verified through formal methods, while the translated UVM tests simulate realistic operational conditions to validate the system.
By integrating formal verification with UVM simulation, Janus significantly improves debugging efficiency (by a factor of 4 on an IP), while also providing detailed coverage generation. For the SDC verification, Janus successfully identified and verified 250+ failing exceptions in simulation.
Event Type
Engineering Poster
TimeTuesday, June 245:00pm - 6:00pm PDT
LocationEngineering Posters, Level 2 Exhibit Hall
Similar Presentations