Global training solutions for engineers creating the world's electronics
Menu
Essential Formal Verification
This course is available Live Online worldwide: View the Live Online full course description »
Essential Formal Verification is a hands-on, practical introduction to formal verification which will teach you the theoretical knowledge and the practical skills you need to get up-and-running with formal in the context of your design or verification project. All practical labs are run hands-on using a specific formal verification tool, although the main focus is on generic concepts that are applicable to all of the current commercial formal verification tools. After taking this course, you will have the practical skills to run formal for yourself, confident in the knowledge of what you are doing and why you are doing it.
Essential Formal Verification is delivered as a 3-day public face-to-face training or 4 sessions of live online training.
Workshops comprise approximately 50% of class time and are based around carefully designed hands-on exercises to reinforce learning.
Doulos is an independent company, enabling delegates 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:
This course is aimed at anyone who has some familiarity with RTL coding and wants to learn the principles and practicalities of running formal verification. Hence it is suitable for all RTL design engineers and design verification engineers, most obviously for engineers who are already using Verilog, SystemVerilog, or VHDL.
This course assumes you are familiar with RTL coding in general and can at least read and understand Verilog or SystemVerilog RTL code. You should have some familiarity with SystemVerilog Assertions (SVA), although you don't need to be an expert because this course will teach you how to write SVA for formal verification. Aside from RTL and SVA, you do not need to know SystemVerilog or any other language.
If you know VHDL but not Verilog or SystemVerilog, please contact sales to discuss the options.
You do not need to know anything about formal verification.
Doulos training materials are renowned for being the most comprehensive and user friendly available. Their style, content and coverage is unique, and has made them sought after resources in their own right. The materials include:
Bug hunting • Levels of Expertise • Functional Verification • Equivalence Checking • Property / Model Checking • Formal Test Bench • Formal Complements Simulation • Learning to Use Formal • Formal Script • Formal GUI • Counter-Example - Waveforms • Counter-Example - Analyzer • Counter-Example - Source Code • Style of Assertion • Specification versus Implementation • Where and When to Use Formal
Kinds of Concurrent "Assertion" • The Canonical Concurrent Assertion • Single-Cycle Properties • Implication and Vacuity • Assertions Embedded in RTL code • Bind • Satellite Code
Temporal Operators • Consuming Clock Cycles • Traces and Sequences • Linear Sequences • Sequence or, and • Sequence Concatenation and Fusion • Structure of an Assertion • Temporal Operators • Naked Sequences • Sequence Operators • Ranges • Fusion in a Range • Unbounded Ranges • Repetition Operator • Multiple Matches • Reducing the Number of Matches • Zero Repetitions • Sequence intersect • Sequence intersect • Gotchas
Matching Changes • Looking Backward • Names Sequences • within • Sequence and versus intersect • Goto • Non-Consecutive Repetition • throughout • Sequence Arguments • Named Properties • Assertion Variables • until, • iff • Weak versus Strong until • always and s_eventually • Liveness versus Safety Properties • Eventually versus Unbounded
State Space • Features of Simulation • Formal Model Checking • Target State • Unrolling the State Space • Reset State • Simulation versus Formal • The Result of Running Formal • Inconclusive Results
Implication and Vacuity • Counter-Example • Input Assumption • Simulating Assumptions • Overconstrained • Overconstrained • Verifying Assumptions with Cover • Witness Trace • What Formal Does (Very Roughly) • Benefits and Use Model • When Things Go Wrong
The Heapsort Algorithm • Assumptions • Implication Doesn't Mean Causality • Restricting the Use Cases • Heap Smoke Test • Heap Simple Assertions • Heap Interesting Properties • Free Variables and Invariants • Hard Properties • Property Progress Report • CPU and Memory • Limits of Formal • What Typically Happens • Dealing with Inconclusive Proofs
Formal Apps in General • Automatically Extracted Properties • Array Bounds Check • Arithmetic Overflow Check • Unique Case Check • Formal GUI • What Typically Happens • Other Formal Apps
Formal Coverage Analysis • Coverage Waivers • Coverage in Simulation versus Formal • Use Models for Coverage • Running the Coverage App • Formal Coverage Report • Other Aspects of Formal Coverage • Reachability versus Correctness • Assertion Density Cone of Influence • Enough Assertions Really? • Formal Core
Dealing with Inconclusive Proofs • Reducing Widths and Depths • Verify One Mode at a Time • Bounded Proofs and Formal Sign-Off • Track Bugs Found at each Proof Depth • Example Inconclusive Proof • Verification Task Progress • Formal Engine Orchestration Bounded Unreachability - Script
Formal Testbench Analyzer App • RTL Mutations • RTL Mutation + Formal • Formal Testbench Analyzer App
Restricting State Space Explosion • Wide versus Narrow Proof Searches • Divide and Conquer • Property Complexity Analysis • Cut Points Added • Constrain the Inputs • Deep State Space Search • Max Proof Depth • Cut Points Free Variables • Not Resetting the DUT • Counter Abstraction • The Nature of Formal Abstractions
Two Transaction FIFO Abstraction • Constraining the FIFO Inputs • Witness Trace • Satellite Code • Proving Safety and Liveness • Converting Liveness to Safety • Counting Transactions
Complete an enquiry form and a Doulos representative will get back to you.
Enquiry FormPrice on request
