This course assumes a foundational understanding of digital design principles and hardware description languages (HDLs), with familiarity with SVA being beneficial but not mandatory. Prior experience in formal verification is advantageous but not required. A background in IC design or verification is preferred. Proficiency in basic programming and digital logic is necessary, along with access to formal verification tools for executing SVA assertions.

With the continuous development of formal verification technology, both the performance of the formal tools and the formal verification methodology has been greatly improved in recent years. Formal verification has also become popular in the industry. At DVCon, one of the most influential technical conferences in the entire IC verification field, there have been more and more topics about formal verification. The topics of these speeches introduce the application of formal verification technology in actual projects. Major chip design companies in the industry have specific cases about the application of formal verification technology. Formal verification technology has a unique prove-to-be-true method when verifying the design functions, which has been recognized by many chip-design and verification engineers. These engineers have now begun to use it as an important verification technology that needs to be mastered, and learn how to apply formal verification technology to their projects. Property coding is the first step in starting project practice with formal verification technology.

Formal verification is a property-based verification method that describes all functional features that need to be verified in the design one by one through property encoding. Then, by combining the specified properties with formal techniques, all the properties are run on formal verification tools to observe the results and determine if the RTL design code and the design functionality described by the properties are consistent.

This course will mainly focus on how to write property code, discuss the basic syntax and principles of the latest SVA property language, how to write efficient assertions, and the important role they play in the property-based verification flow. Based on a large number of project practical experiences, through specific cases, it analyzes and explains the method of writing streamlined and efficient property codes. This course can guide us on how to apply formal verification technology in actual projects as the beginning of project practice.

This course provides a comprehensive overview of formal verification principles and practices, focusing on SystemVerilog Assertion (SVA). Students will learn to identify design modules suitable for formal verification, abstract their functional features, and translate them into SVA properties. By building a property-based formal testbench, students will compare RTL design code with property checking to ensure functionality meets design specifications. The course emphasizes the importance of formal property verification in improving design quality and provides practical methods for writing effective SVA properties. Additionally, students will learn to use auxiliary HDL code in complex designs and evaluate Verification Components for a structured approach to verification.

In the formal verification, the object of verification is property checking. Identify the design modules suitable for formal verification and abstract their functional features one by one from the specifications of these modules. Translate these features into corresponding properties using a property-based language. Build a property-based formal testbench, and compare the RTL design code with the property checking to verify whether the RTL design code's functionality meets the requirements of the design specifications.

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.

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

SVA describes the behavior of a design from a verification perspective, using properties to describe what the design should and should not do. The course provides many practical methods for using SVA language, as well as recommended coding styles, common SVA issues and how to avoid them, and the pros and cons of different methods of placing SVA.

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 modelled 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.

An assertion-based verification testbench often requires a lot of time and effort to develop, which makes it necessary to consider the reusability of verification environments, such as models, assertions, assumptions, covers, etc. For those common design modules, we can develop an assertion-based verification component and encapsulate it, making it more standardized and versatile, so it can become an assertion-based verification IP. In the formal verification process, using more such verification IPs can significantly reduce the time to build the verification environment and help to improve the efficiency and quality of the verification work.