Osmosis 2020: Customer Story - Ensuring Completeness of Formal Verification with GapFree: To End or Not to End (Property Writing) | Sandia National Laboratories

Ratish Punnoose, Distinguished Member of Technical Staff

A challenge with formal verification of RTL designs is knowing how much verification is enough. This is especially true when it comes to knowing when to stop writing additional properties. How can we achieve confidence that enough properties have been checked to verify the correctness of the design? OneSpin's GapFreeVerification methodology provides an answer to this problem. The methodology results in an automated check of the written properties to ensure that all design behaviors have been captured.