JasperGold: Structural Property Synthesis App
Assertion-Based Verification and Property Creation
It can take a long time before a testbench is available, so rather than wait, RTL designers would like to start basic verification as soon as enough RTL is available to do so, then move on to the next project. Assertion-based verification (ABV) can support such an expedited workflow, but writing assertions in standard languages such as SVA or PSL demands specialized knowledge. Even for experts, it can be extremely time-consuming to manually create all the properties required. What’s needed is:
- Automation that can extract and deduce essential properties from RTL;
- The ability to perform structural and functional checks as early as possible in the RTL development cycle, even before any test vectors or testbench is available;
- The capability to automatically rank, classify, prove and verify the properties; and
- Customized debug features to effectively root cause the relevant failures.
The Jasper Solution
The JasperGold® Structural Property Synthesis (SPS) App automatically generates IEEE standard SVA properties based on your RTL – no testbench or stimuli are required! This offers engineers with no knowledge of SVA to generate many valuable properties very quickly, saving many weeks of tedious error-prone work.
The App can be used early in the validation process because the App automatically extracts structural properties from even fragments of RTL. These structural properties can then be configured from a wide variety of predefined functional checks such as dead code checks, finite state machine (FSM) checks, arithmetic overflow checks, etc.
The generated properties can also be ranked, pre-classified and output in standard SVA which can then be used in any ABV flow such as simulation, formal analysis or emulation to increase functional coverage and reduce debug time.
Bottom line: the SPS App helps eliminate common functional design errors and makes sure the code is clean before validation starts; improving design quality and shortening the overall schedule.
- The JasperGold® Structural Property Synthesis (SPS) App reads in the design under test’s (DUT's) RTL only -- no stimuli is needed, and the testbench can be non-existent, and/or it will be ignored even when available. There is also no need to annotate and/or add pragmas to the RTL.
- The App generates structural properties to feed a variety of lint/static checks (like non-synthesizable constructs, out-of-range indexing, etc.), common design errors (like arithmetic overflow, bus conflicts and floating bus, out of range indexing, etc.), and predefined functional checks (such as dead code checks, such-at signals, finite state machine (FSM) checks, etc.).
- The SPS App’s Analysis Browser highlights the exact lines of RTL code corresponding to the issues identified by the property synthesis.
- Users can manually assign “waivers” for clearly illegal / impossible cases for the SPS App to avoid in follow-on runs.
- Properties created by the SPS App can be fed directly into Jasper's advanced Visualize™ debug and "What-if?" analysis debug flows.
- The properties can also be ranked, pre-classified and output into IEEE standard SVA which can then be used in any assertion-based verification (ABV) flow such as simulation, the JasperGold Formal Property Verification (FPV) App/formal analysis, or emulation to increase functional coverage and reduce debug time as part of an RTL sign-off flow.
- Enables engineers with no knowledge of SVA to automatically generate, classify, and rank many valuable properties very quickly -- even before a testbench exists -- saving many weeks of tedious error-prone work
- Helps eliminate common functional design errors and makes sure the code is clean before validation starts
- Can be used with the JasperGold® Formal Property Verification App to exhaustively find design errors before simulation is available
- Leverages Jasper’s unique Visualize™ technology to enable users to focus on critical expressions and points of interest, and a GUI for easy specification of waivers for known illegal/impossible areas for follow-on runs
- Requires users to document the reason for waivers for clearly impossible/illegal code coverage paths – this really helps when you come back to the report weeks or months later. This is especially true when you need to consider if the waivers are still valid when the block is reused.