This is the follow-on course to Essential Formal Verification Online. It is intended to take engineers beyond an introductory use of formal technologies to a deep, practical level of knowledge of formal verification.
Advanced Formal Verification will equip you to tackle complex verification challenges, by taking full advantage of formal verification on your engineering projects.
Advanced topics such as satisfiability, abstractions (e.g., safe, reduction, and induction), formal synthesis and modeling, non-determinism, advanced constraints, under- and over-constraining, and much more are discussed in depth. While the practical labs are run hands-on using specific formal verification tools, the main focus is on the concepts that are applicable to all of the current commercial formal verification tools.
Practical labs comprise approximately 50% of class time and are based around carefully designed hands-on exercises to reinforce learning. The Advanced Formal Verification exercises are built around the open source RISC-V Picorv32 project, applying formal techniques to it and other peripheral modules.
Doulos is an independent company, enabling course attendees to receive the benefit of objective tuition, while learning in the context of their chosen tool and methodology. Leading tools supported by this course include:
Cadence Jasper™ Formal Verification Platform
Siemens Questa® Formal
Synopsys VC Formal™
Course Overview Video:
Who should attend?
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.
What will you learn?
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
Pre-requisites
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.
Training materials
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.
Structure and Content
How Formal Works
Formal algorithms • Counter-examples • Formal engines • Clocking • Initialization and reset sequences • Formal flow and synthesis • Debugging with formal
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
Writing constraints for performance • Large input stimulus generation • Constraint dependencies • Helper constraints • Packet-based protocols
Formal Equivalency
Differences between LEC and SEC • How SEC works • Assume-guarantee process • Automatic and user-defined mappings • Helper assertions and hints • Dealing with SEC inconclusives • Applications for SEC
