This course is designed for engineers, verification professionals, and students who have a basic understanding of digital design and want to dive into formal verification using Property Specification Language (PSL). While no prior experience with PSL is required, familiarity with hardware description languages (HDL) like Verilog or VHDL will be beneficial. 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 the Property Specification Language (PSL) and how to write concise and efficient assertions. PSL 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.

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.

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

The Foundation Language (FL) refers to all PSL except the Optional Branching Extension (OBE). It can easily express simple properties like conditions that occur in the same cycle, the next cycle, some following cycles, and eventual conditions. The FL structure has powerful operators for expressing simple relationships between Boolean conditions. It can also be used with SERE to get more complex properties.

SERE stands for Sequential Extended Regular Expression. Properties with temporal usually use SERE for description. SERE allows easy expression of complex, multi-cycle, sequence-based properties. This is simpler and more readable than using other FL structures. Operators allow simple descriptions of repeating sequences and provide options like consecutive repetition, non-consecutive repetition, and goto repetition. A general sequence can be written once, named, and used in other SEREs. Complex sequences can be managed by breaking them down into individual named sequences.

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.

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.