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
