Essential Formal Verification Online

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.

• How to run formal verification
• A solid understanding of the principles and practicalities of using formal
• Recommendations on where, when and how to use formal
• How to write assertions (SVA) for formal and avoid the pitfalls
• The strengths and weaknesses of formal compared to simulation
• How to write formal testbenches to complement or replace simulation at block level
• Central concepts in formal such as vacuity, counter-examples, witness traces, assumptions, under-constraints, over-constraints, false positives, false negatives, free variables, safety versus liveness properties, cone of influence, formal core, and proof depth
• How to deal with inconclusive proofs and achieve formal sign-off using divide-and-conquer, cut points, abstractions, bounded proofs, and bounded unreachability analysis
• How to run formal apps such as automatically extracted properties, formal coverage, and unreachability analysis

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:

• Fully indexed class notes creating a complete reference manual
• Workbook full of practical examples and solutions to help you apply your knowledge

Introduction to Formal Verification

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

SVA Basics

Kinds of Concurrent "Assertion" • The Canonical Concurrent Assertion • Single-Cycle Properties • Implication and Vacuity • Assertions Embedded in RTL code • Bind • Satellite Code

SVA Temporal Logic

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

SVA Convenience Syntax

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

Understanding Formal Verification

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

Assumptions

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

Heapsort Example

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

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

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

Inconclusive Proofs

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 

RTL Mutation

Formal Testbench Analyzer App • RTL Mutations • RTL Mutation + Formal • Formal Testbench Analyzer App

Cut Points and Abstraction

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 Abstraction

Two Transaction FIFO Abstraction • Constraining the FIFO Inputs • Witness Trace • Satellite Code • Proving Safety and Liveness • Converting Liveness to Safety • Counting Transactions