Course

SystemVerilog Assertions and Formal Verification

---

As more functionality is packed onto denser chips, including system-on-chip (SoC) designs, verification can become a daunting task. Leading design and verification teams are using the power of assertions to manage their verification challenges through both simulation-based and formal property checking verification methodologies. While simulation-based verification accounts for the majority of verification activities, Formal Verification (FV) has matured to complement the simulation in order to verify complex and control-oriented design blocks.

This course introduces SystemVerilog Assertion (SVA) concepts and syntax, using small examples and a realistic design. It covers a range of topics, from the basics of the SVA constructs to the OVL checker library. It also covers writing and debugging assertions in the design using advanced SVA constructs. You will learn to write assertions for formal verification. The second part of the course introduces formal verification theory. You will run the formal tool, debug a counter-example, and learn the refinement process. The course covers FV application in several design stages and in different functional areas such as SoC connectivity, coverage closure, and x-propagation checks.

The lab-based course covers key topics in detail, from language constructs to assertion coding guidelines that include practical examples of how to use assertions in verification. You will also learn methodology choices and assertions in a formal context. The course provides hands-on exercises using assertions, dynamic simulations (VCS) and formal or semi-formal verification (Verification Compiler - Formal).

Topics include:

• Introduction to SVA
• SVA checker library
• SVA basic and advanced constructs
• Introduction to formal verification and tools
• Use of SystemVerilog Assertions in Formal Verification
• Case studies and labs
• Applications of Formal Verification

Skills Needed: Knowledge of basic logic design, simulation and familiarity with a hardware description language.