This course is designed for engineers and verification professionals who are familiar with basic digital design concepts and are looking to deepen their understanding of SystemVerilog Assertions (SVA) and formal verification techniques. A solid foundation in digital logic and familiarity with hardware description languages (HDL) like Verilog or SystemVerilog is essential for success in this course. To get the most out of this course, it’s recommended that you meet the following prerequisites:

Formal verification is a property-based verification method. The formal testbench it constructs mainly includes cycle-based models, constraints, end-to-end checkers, functional coverage, and formal verification IP. Writing these components relies heavily on assertion languages. Assertion is a design behavior description language with a foundational syntax structure that requires systematic learning. For formal verification, systematically learning and mastering an assertion language is one of the basic skills needed to enter the field.

Assertions have been a verification method for many years. However, due to limitations in tool performance and methodology, they were mainly used as an auxiliary verification method and were not widely adopted. With the rapid development of formal verification technology, assertion-based verification (ABV) has become popular recently. Initially, assertions were used sparingly in testbench as an auxiliary verification method. Now, they can be used independently with a complete methodology to build a property-based testbench for sign-off.

This course focuses on the basic syntax rules of SystemVerilog Assertions (SVA) and how to write concise and efficient assertions. SVA has a rich syntax structure and many advanced usage methods. However, for formal verification, the requirements for assertion syntax are not high. There is no need to master complex syntax structures or advanced usage methods because they are not used in formal verification. Formal verification emphasizes using auxiliary code with assertions to construct intermediate signals for complex design behaviors, while assertions handle simple property behaviors involving these intermediate signals. This course guides how to apply assertions in actual projects and serves as a starting point for formal verification project practice.

SVA is part of the SystemVerilog language, defined in the industry standard IEEE 1800 for SystemVerilog. SVA is a property description language with basic syntax composed of four levels: Boolean expressions, sequences, properties, and verification directives.

Boolean expressions are the foundation of the SVA language. They are the first level of the SVA structure, and all design behavior descriptions start with them. This course explains and demonstrates simple assertions based on Boolean expressions.

Sequences are the second level of the SVA structure. Cycle-based properties are usually described using sequences. A sequence contains multiple Boolean expressions separated by ##N, where N is the number of cycles between expressions. This course explains sequences and shows assertions based on them.

Liveness assertions and fairness assumptions do not have meaning in simulation; they are only effective in formal verification. A liveness assertion means that something good will eventually happen, while a fairness assumption means an input must eventually be false. These concepts are related to the IEEE standards of the SVA language. Note that the same property can behave differently under different syntax standards.

For those low-efficiency SVA, it takes a lot of time to create and debug them. The symptoms of low-efficiency SVA are not limited to tools and technology, but also bring many human factors, making it difficult to understand the properties and a big problem for maintenance and reuse. In formal verification, all SVA and design codes need to be modeled into state space by synthesis tools. They are part of the complexity, so the efficiency of SVA is especially important.

In a property-based verification environment, a lot of auxiliary HDL code is often required while the proportion of SVA is often small. By creating auxiliary code, the writing of properties is easier and more readable and easier to understand. The use of auxiliary code also makes it easier for tools to evaluate verification issues and reduce tool run time. SVA language has some limitations. When facing complex designs, the SVA language cannot describe them at all. It is necessary to use auxiliary code to help model and construct these design behaviors.

As formal techniques research matures and approaches a level of sophistication required by industry, we must take steps to ensure a successful transfer to this more demanding level. One step is to fundamentally change design methodologies such that we move from ambiguous natural language forms of specification to forms that are mathematically precise and verifiable. Formal property verification is the key ingredient in this methodological change. The end result is improved design quality through improved understanding of the design space, improved communication of design intentions, and improved verification quality.