This course is designed for engineers, students, and professionals who aim to master Property Specification Language (PSL) and elevate their verification capabilities. To succeed in this course, you should have a solid understanding of digital design and hardware description languages like VHDL or Verilog. Familiarity with basic verification concepts is also essential, as this course will build on those foundations to teach you assertion-based verification using Property Specification Language (PSL). To get the most out of this course, it’s recommended that you meet the following prerequisites:

Assertions are embedded pieces of code that act like observers. They can be inserted anywhere in the design code. When used in a verification environment, assertions help to identify design bugs earlier and more easily. This method is a highly efficient way to improve work productivity. Through assertions, we can capture specific design behaviors and gain detailed knowledge of how the design should operate. Assertions are crucial for increasing the observability and controllability of a design. Assertions are a language for describing design behavior. Their syntax is fundamental, requiring systematic learning to use assertion-based verification techniques effectively.

Assertion-based verification provides an effective way to improve verification quality by offering better controllability and observability of design bugs. Using assertions ensures that interface designs are executed correctly. They help discover deep design bugs, identify hard-to-find corner cases. We can also analyze and improve test cases in simulation through coverage environments with assertions.

Our course mainly focuses on the basic syntax of Property Specification Language (PSL). PSL is a language under the IEEE 1850 standard. It has a long history of development and use and is a powerful property description language. This course introduces the basic terms in PSL and its four-layer structure: modeling, verification, temporal, and Boolean layers. It covers the VHDL and Verilog PSL flavors and the keywords in PSL. We discuss important parts of PSL, such as Boolean expressions, SERE, SERE Composition, and coverage. By analyzing specific cases, we consider what to pay attention to when writing PSL properties and summarize some methods for writing effective property code. This course guides us on how to apply assertion-based verification techniques in real projects and serves as a basic skill to master when starting project practice.

Leverage assertions and translate design specifications into assertions. Assertions are written by various people at various times during the development of a product, from conception through design and implementation, and during verification. Assertions can be written at different levels of abstraction, in various hardware design language contexts. Assertions take some effort to write. At the same time, they can make design verification much more efficient, can simplify debugging, and can significantly improve overall productivity.

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 SERE. Complex sequences can be managed by breaking them down into individual named sequences.

Sequences include a wide range of powerful operators and functions that allow the construction of complex sequences. PSL has many complex operators to build sequences, and using advanced sequence combination operators and features makes defining sequences and properties easier.

Besides verifying functional correctness, it is essential to check the completeness of the verification process. Monitoring and managing verification progress, and evaluating the quality of verification through completeness results, is crucial. Coverage can be introduced to analyze the effectiveness of test cases and observe the efficiency of test vectors.