Learning outcomes

Core Understanding and Foundations
• Grasp the core principles, purpose, and value of formal verification in modern digital design flows.
• Distinguish between formal and simulation-based verification, understanding when and how to apply each effectively.
• Understand the syntax, semantics, and structure of SystemVerilog Assertions (SVA) for both combinatorial and sequential logic.

Who is the course for?

Schedule

Session 1 – Core Principles & Property Development
• Review of formal verification fundamentals
• Property classification and types
• Advanced formal constructs and temporal operators
• Techniques for writing and debugging assertions

Session 2 – Formal Methodologies in Practice
• Constrained random vs formal: when and how to combine
• Integrating formal into the verification flow
• Proof strategies and bounded proofs
• Debugging counterexamples and proof convergence

Session 3 – Productivity and Reuse
• Leveraging reusable property libraries
• Abstraction and modular design for scalability
• Best practices for verification planning and sign-off
• Case study: deploying formal in a complex SoC project

Session 4 – Advanced Applications
• Equivalence checking and formal regression flows
• Formal for interface and memory coherency verification
• Safety and security property verification
• Coverage analysis and closure

Session 5 – Industrial Deployment & Tool Integration
• Overview of key formal tools (Synopsys, Cadence, Siemens, OneSpin)
• Setting up formal environments and automating runs
• Common pitfalls and troubleshooting techniques
• Workflow integration and collaboration

Session 6 – Real-World Scenarios & Future Trends
• Case studies from leading semiconductor companies
• Formal verification in AI, automotive, and safety-critical domains
• Emerging research and methodologies
• Interactive Q&A and wrap-up discussion

New content being added:
• Property classification: fairness, safety, liveness, concurrent, and sequential properties
• Formal constructs: sequences, let, and other key structures that simplify complex designs
• Operators in depth: mastering release, until, and other important operators
• Formal closure: understanding its role and how to ensure completeness in proofs
• Bridging formal and functional verification: how both approaches complement each other for robust verification
• Complementary coverage and signoff techniques: achieving comprehensive verification confidence
• Creating formal scenarios from functional unreachable coverage: turning coverage gaps into valuable test opportunities
• Switching between asserts and assumes: understanding when and why to use each effectively
• Plus much more: practical examples, debugging tips, and methodology insights drawn from industry experience

Trainer Profile

Dr. Mike Bartley earned his PhD in Mathematical Logic from the University of Bristol before entering industry in 1988, applying formal languages (Z and VDM) to software development and training. He moved into semiconductors in 1994 with ST Micro, pioneering the use of constrained random techniques and formal verification for CPU and SoC design. Over the years, Mike has led verification innovation at Infineon, two start-ups, and his own company—Test and Verification Solutions—later acquired by Tessolve. He now leads Alpinum Consultancy, providing advanced verification training and consultancy services.
A qualified teacher since 1984, Mike combines deep technical expertise with strong pedagogical skills, honed through teaching in schools, universities, and industry. His courses blend practical labs, quizzes, and online assessments to support active learning and measurable progress.
Mike has supported formal verification deployment at leading organisations including ST Micro, Infineon, ARM, Intel, NXP, AMD, Panasonic, and Samsung, and has organised major industry conferences such as Verification Futures. In the past three years, he has delivered this course eight times across universities (Mexico, Vietnam, Egypt) and companies such as Intel, SiLabs, and QUALCOMM.