Ensuring that a design is fully specified by assertions
Traditional formal verification ensures that a design satisfies required functionality as specified by a set of assertions. The idea of a formal proof is very powerful, but only as good as the assertions underlying it. These leads to some important verification questions:
- What if the set of assertions is incomplete?
- What if the design contains additional functionality not covered by the assertions?
- What if this additional functionality is there by mistake or malicious action?
OneSpin’s GapFreeVerification App answers these questions. It leverages the Operational Assertions App, which enables formal verification enthusiasts to develop high-level, non-overlapping assertions (Operational SVA) that capture end-to-end transactions and requirements in a concise, elegant way. The Operational Assertions are leveraged by the GapFreeVerification App for automatic detection of specification omissions and errors, holes in the verification plan, and unverified RTL functions.
GapFreeVerification goes beyond proving that the RTL design meets the set of Operational SVA. It also verifies that the set of assertions is sufficient to cover the design and ensures that there is no unverified RTL functionality. Any unintended functionality in the design is detected and reported as a violation of the assertions. Extra logic included in the design by accident, or inserted deliberately as a hardware Trojan, is flagged so that it can be removed. OneSpin’s GapFreeVerification App ensures that a design does everything it's supposed to do and does not do anything it's not supposed to do.
The GapFreeVerification App is included in the DV-Certify platform.