Formal 101 – Setting Up & Optimizing Constraints

Constraints development for formal analysis is quite simply the creation of appropriate limits on the universe of possible stimulus being driven into the DUT’s input signals – i.e. it is conceptually similar to a constrained-random RTL simulation stimulus setup. However, in this process, instead of writing formatted constraints in SystemVerilog or VHDL, the user describes valid behavior of the inputs using either hand-written “properties” in SystemVerilog (SVA) or Property Specification Language (PSL), or productized libraries for standard protocols (AHB, AXI, etc — Siemens EDA offers multiple formal-optimized verification IPs.) Furthermore, the unique nature of formal analysis enables engineers to learn important information by temporarily under-constraining and over-constraining the analysis.

In this 40-minute webinar we will show you how to write optimal constraints for formal analysis; and how to deliberately under- and over-constrain the analysis to learn more about the effectiveness of the constraints themselves, your test plan and formal coverage plan, and the DUT behavior.

Note that this webinar will be relatively technical: the examples will include RTL code — familiarity with Verilog or VHDL is assumed.

What You Will Learn:

• The difference between simulation and formal constraints
• How “less is more” when it comes to formal constraints
• How to benefit from deliberately under- and over- constraining the analysis
• How you can further leverage an aspect of the popular “assume-guarantee” formal principal to further refine your constraints

Who Should Attend:

• Design & Verification engineers who are new to formal property checking

Product Covered:

Questa PropCheck