Workshop Description

Hands‑on introduction to formal verification using SVA, model checking, and practical tool flows to prove RTL correctness and find hidden bugs early. 

The emphasis is on: 

• Building foundational understanding of formal verification concepts and workflows 

• Teaches how to write effective SystemVerilog Assertions for formal engines 

• Introduces assume‑guarantee reasoning to constrain and guide formal analysis 

• Covers bounded model checking, k‑induction, and IC3/PDR techniques 

• Demonstrates counterexample debugging and root‑cause analysis 

• Explores RTL‑to‑gate equivalence checking for design assurance 

• Uses Questa Formal tools (PropCheck, AutoCheck) in hands‑on labs 

• Shows how to integrate formal verification into a complete verification strategy and sign‑off flow

Workshop Duration: 2 days