Presentation
Advanced State Space Tunneling: Debug Your Formal Complexity Using Waveforms!
DescriptionOne of the most challenging elements of Formal Property Verification (FPV) is the when the user encounters complexity: some subset of properties time out while neither proven nor disproven. While many advanced techniques are available to address complexity, this can be especially tricky because the FPV tool does not provide a debuggable waveform. However, the technique of State Space Tunneling (SST) allows a user to generate a waveform that gives insight into why the tool is encountering complexity issues, and the user can leverage it to create helper assertions that will enable FPV to overcome the complexity issues. While SST has been around in some form for over a decade, recent advances in the technology have made it much more usable for the typical validation engineer. Thus, for users who may have tried it unsuccessfully in the past, now is the perfect time to dive back into this powerful methodology. Benefits of recent improvements include better integration into core engines, integration of "soft constraints" to create better waveforms, and completion of proofs using "upper bounds". We will discuss the usage model and recent improvements to SST, and how they enabled excellent FPV results in a recent project at Tenstorrent.
Event Type
Engineering Poster
TimeTuesday, June 245:00pm - 6:00pm PDT
LocationEngineering Posters, Level 2 Exhibit Hall