Course

SystemVerilog Assertions and Formal Verification

Technologies like machine learning, autonomous driving, IoT, and cloud computing are ushering a new era of chip design with innovative architectures and advanced process nodes. With billions of dollars at stake, the race to be first-to-market is putting new challenges on the chip design and verification community.

In this course, you will be introduced to SystemVerilog (1800-2017 IEEE standard), a unified hardware design, specification and verification language that is being rapidly adopted by chip designers and verification teams to boost productivity and ensure first-pass silicon success. While it’s based on Verilog and some extensions, the SystemVerilog language improvements include enhanced scheduling semantics, rich data types, interfaces with emphasis on assertions, and formal verification—all covered in this course.

You will also be introduced to SystemVerilog Assertion (SVA) concepts and syntax, using small examples and realistic design protocols. You will learn about immediate and concurrent assertions, their differences and use cases, and how to write assertions for formal verification. In the second part of the course covering formal verification theory, students will run the formal tool, debug a counter-example, and learn the refinement process.

In addition, we will work with:

Formal Verification applications (FV Apps) to be deployed in several design stages and in different functional areas such as SoC connectivity (CC)
Coverage closure (FCA)
X-propagation (XPROP) checks.

This is a lab-based course giving you the opportunity to dive into key topics in detail—from language constructs to assertion coding guidelines that include practical examples of how to use assertions in verification. Students will also learn methodology choices and assertions in a formal context. The course provides hands-on exercises using assertions in simulation (VCS) and formal verification (VC-Formal).

Topics Include: