Released on November 11th, 2021.
Overview:
In our prior webinar “Formal 101 – Basic Abstraction Techniques”, we showed how to apply time-tested techniques to safely “abstract away” DUT constructs that commonly cause trouble for the formal analysis. Complementing these methods are two additional formal analysis principals that can also deliver equally dramatic reductions in wall-clock run time: Data Independence and Non-Determinism.
Quick Definitions:
- Data Independence (DI): your property/assertion does NOT depend on the specific values of the data.
- Non-Determinism (ND): this is a technique that uses “free variables” implemented as un-driven wires or extra inputs in a checker to tell the formal engines they are free to consider any cases involving all possible values of the variables at once.
In this session, we will show how with a little design knowledge and forethought on your part, you can leverage these two principles to cut down your formal analysis to a matter of minutes vs. hours.
Note that this session will be relatively technical: the examples will include RTL code -- familiarity with Verilog or VHDL is assumed.
What You Will Learn:
- The conceptual background of Data Independence (DI) and Non-Determinism (ND)
- How to quickly identify DUT elements where these verification techniques can be applied
- Examples of applying DI and ND techniques
Who Should Attend:
- Design & Verification engineers who are just getting started with formal property checking
