Formal 101 – Basic Abstraction Techniques

Formal verification algorithms can struggle to read-in and analyze DUTs with very large state spaces. Specifically, circuit elements like counters and memories can introduce a lot of state bits and sequential state depth that can bring a formal analysis to a grinding halt. The solution is to “abstract away” such parts of the DUT by either swapping in simplified models of these elements, or by safely removing them completely (electronically, without touching your golden RTL source code).

Fortunately, modern formal tools like Questa PropCheck automate the abstraction of many troublesome DUT elements; saving you setup time up-front, as well as wall clock run time and memory usage. But there are some circuit elements that the tools just can’t infer on their own from the raw RTL.

This is where your engineering knowledge comes in, using the contents of this webinar to guide you. In this session we will teach about the types of DUT constructs that commonly cause trouble for the formal analysis, and how to apply time-tested techniques to safely abstract them away so that the formal verification run can rapidly reach closure.

Note that this session will be relatively technical: the examples will include state diagrams and RTL code. Familiarity with Verilog or VHDL is assumed

What You Will Learn

• What kinds of circuit designs commonly need to be abstracted away
• The range of available abstraction techniques
• How to quickly and effectively apply these techniques (electronically, without editing …