Start date: 09 January 2024
Duration: 4 Days, 9am - 3pm each day
Location: Online course
Cost: Members € 600; Non-members € 900
Course code: N/A
Note: The next rerun of this course is being postponed from 24-27 Oct to 9-12 January 2024.
This 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. Leading tools supported by this course include:
• Cadence JasperGold®
• Siemens Questa® Formal
• Synopsys VC Formal™
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. In order to satisfy demand, 2023 reruns are being held on 24 - 27 Oct, 25 - 28 July and 28 - 31 Mar 2023 after 3 reruns in 2022 on 29 Nov - 2 Dec, 20 - 23 Sept and 28 - 31 Mar. 2022.
Participants on this course will learn:
• 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?
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.
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
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
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
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
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.