This course assumes a foundational understanding of digital design principles and hardware description languages (HDLs), with familiarity with PSL 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 PSL 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 PSL 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 Property Specification Language (PSL). Students will learn to identify design modules suitable for formal verification, abstract their functional features, and translate them into PSL 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 PSL properties. Additionally, students will learn to use auxiliary HDL code in complex designs and evaluate Verification Units 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.

PSL is a language which is IEEE standard 1850, and it has a strong history of development. It is a powerful property specification language that can describe complex behaviors in very few characters. PSL has the power to define complex properties which, although useful for formal verification, cannot be easily evaluated in simulation. The PSL Language Reference Manual defines a simple subset for the language which is easily simulated.

PSL 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 PSL language, as well as recommended coding styles, common PSL issues and how to avoid them, and the pros and cons of different methods of placing PSL.

For those low-efficiency PSL, it takes a lot of time to create and debug them. Therefore, it is crucial to write effective PSL properties. Do not duplicate RTL code. Fully specifying enabling sequences and using edge-triggered conditions can help avoid properties which are over-constrained, under-constrained and over-lapping. Be careful of "open-ended" PSL constructs which can cause assertions to never fail/complete. Understanding the design specification is vital in refining assertions to be effective. An incremental approach to assertion writing works well as you learn the language.

In a property-based verification environment, a lot of auxiliary HDL code is often required while the proportion of PSL 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. PSL language has some limitations. When facing complex designs, the PSL language cannot describe them at all. It is necessary to use auxiliary code to help model and construct these design behaviors.

Understand capabilities of Verification Units. Check your tool documentation for support of VUnit’s. Gives some degree of PSL HDL flavor independence. Allow more structured, reusable and flexible approach to verification.