Lesson 12.5 · Your Formal-Aware Workflow

Where to go next

Keep practising

Re-run every lab in this course with a different tool, or with parameters changed.
Pick a small open-source IP (a UART, an SPI controller, a FIFO) and write a property set for it.
Take part in design-verification communities and code reviews; reading other people's properties is a great teacher.

Resource	Why read it
IEEE Std 1800 (SystemVerilog), assertions clauses	The definitive reference for SVA semantics.
E. Seligman, T. Schubert, M V A. K. Kumar — Formal Verification: An Essential Toolkit for Modern VLSI Design (2nd ed., Morgan Kaufmann, 2023)	An excellent practitioner's book on FPV, apps, FEV and signoff methodology. Highly recommended as a companion to this course.
E. Cerny, S. Dudani, J. Havlicek, D. Korchemny — SVA: The Power of Assertions in SystemVerilog	Deep coverage of assertion language semantics.
E. M. Clarke et al. — Model Checking (MIT Press)	The theory behind the engines.
R. E. Bryant (1986) — "Graph-Based Algorithms for Boolean Function Manipulation"	The paper that introduced reduced ordered BDDs.
A. Biere et al. (1999) — "Symbolic Model Checking without BDDs"	The origin of bounded model checking.
A. R. Bradley (2011) — "SAT-Based Model Checking without Unrolling"	IC3/PDR.
YosysHQ SymbiYosys documentation	Practical guide to the open-source formal flow used in our labs.