Learning outcomes

Formal Verification learning outcomes are as follows:

• 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

Who is the course for?

Schedule

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

Trainer Profile

Martin Jones has worked for over 25 years as a design and verification consultant for several European semiconductor companies including Ericsson, Arm, Infineon and Verilab during which time he has seen the development of verification languages and methodologies culminating in SystemVerilog and UVM, in addition to formal techniques.

Martin has worked with Doulos for a number of years and specialises in the delivery of SystemVerilog and UVM related courses.