Formal
Verification

Run a property with free inputs, read a counterexample and distinguish a bounded result from a proof.

1. F1.1Simulation Covers Paths, Formal Covers States
2. F1.2Your First Proof: The Same SVA, No Testbench
3. F1.3Assert, Assume, Cover: The Three Verbs
4. F1.4Reading a Counterexample
5. F1.5Safety and Liveness, Bounded and Unbounded
6. F1.6Reset, the Initial State and $initstate

See what a formal tool builds from RTL, what SAT and SMT solvers answer, and how BMC, k-induction, IC3/PDR and the other engines reach a verdict.

1. F2.1From RTL to a Transition System
2. F2.2SAT and SMT in One Lesson
3. F2.3Bounded Model Checking
4. F2.4k-Induction
5. F2.5IC3/PDR: Invariants Found by the Tool
6. F2.6BDDs, Interpolation and the Engine Zoo

Build a formal bench, keep assumptions honest with covers, triage false failures, and choose end-to-end, glue, helper and liveness properties.

1. F3.1The Formal Testbench and the Master Rule
2. F3.2Over-Constraint and Vacuity
3. F3.3Under-Constraint and Counterexample Triage
4. F3.4End-to-End Versus Glue Properties
5. F3.5Cover: Reachability, Witnesses and Dead Code
6. F3.6Modelling Code and Helper Assertions
7. F3.7Liveness, Fairness, Deadlock

Find out why a proof stalls, then make it finish with cut points, blackboxes, case splits, assume-guarantee, symbolic constants, abstraction, helper invariants and the right engine, and check every step stays sound.

1. F4.1Why Proofs Do Not Converge
2. F4.2Cutpoints and Blackboxes
3. F4.3Case Splitting and Assume-Guarantee
4. F4.4Symbolic Constants and Data Independence: The Formal Scoreboard
5. F4.5Counter, Memory and Parameter Abstraction
6. F4.6Induction Strengthening in Practice
7. F4.7Engine Choice and Run Management

Build each packaged formal app by hand on the open engine: automatic checks, connectivity, registers, X, clock crossings, unreachability, information flow and post-silicon debug.

1. F5.1The App Map
2. F5.2Automatic Checks
3. F5.3Connectivity
4. F5.4Registers (CSRs)
5. F5.5X-Propagation
6. F5.6CDC and RDC with Formal
7. F5.7Unreachability and Coverage Closure
8. F5.8Security: Information Flow
9. F5.9Formal for Post-Silicon Debug

Prove two designs the same: the miter, combinational LEC with matched flops, sequential equivalence with a latency, why multipliers defeat the solvers, conditional equivalence for a bug fix, and mutation coverage of a property set.

1. F6.1LEC: Combinational Equivalence
2. F6.2SEC: Sequential Equivalence
3. F6.3Datapaths: Why Multipliers Hurt
4. F6.4Proving a Bug Fix Changed Only the Bug
5. F6.5Mutation Coverage with MCY

Say what a proof covers and what it does not, measure a property set by mutation, argue a bounded sign-off with a required depth, hand formal results to simulation, and write the plan a lead can review.

1. F7.1What a Proof Covers
2. F7.2Property Completeness
3. F7.3The Sign-Off Argument
4. F7.4Formal with Simulation
5. F7.5The Formal Verification Plan

Complete formal benches for the blocks every job has: a FIFO, an arbiter, a timer, handshaking FSMs, APB and AXI4-Lite, a memory controller with a write buffer, and a pipeline. Properties, assumptions, covers, proofs and the bugs they catch, all measured.

1. F8.1A FIFO, End to End
2. F8.2An Arbiter: Exclusion, Rotation and Fairness
3. F8.3Counters, Timers and Shift Registers
4. F8.4FSMs and Handshake Controllers
5. F8.5A Bus Interface: APB and AXI4-Lite
6. F8.6A Memory Controller: One Symbolic Address
7. F8.7A Pipeline: Instruction-Level Checking

Sign off a register block end to end, prove a packet router with one symbolic packet and a bounded wait, see what design for formal buys in measured seconds, and walk into a formal interview prepared.

1. F9.1Capstone: Formal Sign-Off of the AXI4-Lite Register Block
2. F9.2Capstone: End-to-End Proof of a Packet Router
3. F9.3Design for Formal, and the Formal Engineer's Week
4. F9.4Formal Interviews and Formal Careers