Advanced Formal Verification Online

This course is targeted at individuals that already have a working knowledge of formal technologies and some hands-on experience.

It is particularly targeted at engineers and teams who want to move to a subject-matter expert level on formal verification, understanding how to plan, use, and implement formal verification on their real-world projects.

• Learn how to setup formal reset initialization sequences and pre-load state
• Learn how to break down and solve formal verification problems
• Learn different reduction techniques for improving formal analysis
• Learn how to build a formal verification environment
• Learn advanced SVA syntax and techniques to apply formal to more applications
• Learn the difference between safety and liveness properties and when to use them
• Learn about nondeterminism, how it accelerates formal, and how it helps you solve problems
• Learn how to build a formal scoreboard, perform data-integrity checks, and much more
• Learn the formal abstraction process and implement formal abstractions
• Learn how to write various types of constraints and how to constrain formal for sequences and frames of input data
• Learn how to avoid over- and under- constraining
• Learn what sequential equivalency checking is, how to use it, and its various applications

This class assumes a working knowledge of SystemVerilog, SystemVerilog Assertion syntax, and formal verification concepts and tools. We strongly recommend prior attendance of the Doulos Essential Formal Verification Online course (or equivalent) prior to attending this course.

Please contact Doulos directly to discuss and assess your specific experience against the pre-requisites.

Doulos training materials are renowned for being the most comprehensive and user-friendly available. Their style, content and coverage are unique in the training world and have made them sought after resources.

The materials include fully indexed class notes creating a complete reference manual.

How Formal Works

Formal algorithms • Counter-examples • Formal engines • Clocking • Initialization and reset sequences • Formal flow and synthesis • Debugging with formal

Formal Modeling

Formal synthesis • Safety • Liveness • Embedded assertions • Fairness • Formal testbenches • Helper code

Nondeterminism

Free variables • Design symmetry • Data independence • Symbolic constants • Formal testbenches • Formal scoreboarding

Abstractions and Reductions

Complexity in formal • Reduction and safe reduction techniques • The basic abstraction process • Types of abstract models • Design symmetry and data independence • Example of design abstractions • Safe abstractions

Abstract Modeling

Abstract checker models • Abstraction by induction • Abstraction using state machines • Abstraction using events • Data integrity checking • Abstract checker model examples

Constraining Formal

Underconstraining • Overconstraining • Guidelines • Advanced property writing • Constraint dependencies • Determining the minimal constraint set

Formal Equivalency

Differences between LEC and SEC • How to setup and use SEC • Mappings • Tips for SEC convergence • Applications for SEC