Formal 101 – Basic Abstraction Techniques


Image for Formal 101 – Basic Abstraction Techniques event

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 35 minute webinar 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 webinar 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 of your golden RTL source code)

Who Should Attend:

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

Meet the speakers

Photo of Jin Hou
Siemens EDA

Jin Hou

Questa Formal Specialist

Ms. Jin Hou received her Ph.D in formal verification from Université de Montréal. She is currently a product engineer for Questa Formal at Siemens EDA. She has 13 years working experience in Formal Verification and Assertion-based Verification, 8 years as CAE supporting the formal tool Magellan at Synopsys, and 5 years as a Product Engineer at Siemens EDA supporting Questa® AutoCheck, PropCheck, Cover Check, X-Check, Connectivity Check, Register Check, Secure Check, SLEC. She has been working in product definition, customer support, tool testing, customer training, technical marketing. She has applied formal verification to a lot of customer designs and helped worldwide customers adopt advanced technologies.
Photo of Joe Hupcey
Siemens EDA

Joe Hupcey

Questa Formal Product Manager

Joe Hupcey III is a part of the Mentor’s Product Management team for Design & Verification Technologies; based in Mentor’s office in Silicon Valley, CA. He is responsible for the Questa Formal product line of automated applications and advanced property checking. Prior to joining Mentor, Joe has held product management and marketing roles in several Electronic Design Automation (EDA) companies, for products that covered multiple aspects of hardware and software functional verification. Before transitioning into marketing, Joe worked as an electrical engineer in FPGA design, EDA tools for FPGAs and ASICs, and ASIC verification. Joe’s educational background includes BSEE, MSEE, and MBA degrees from Cornell University in Ithaca, NY.


Register with your Siemens account or register as a guest.