This course is designed for professionals with a solid foundation in SystemVerilog and digital design. Familiarity with basic verification concepts and prior experience with Assertion-Based Verification (ABV) is highly recommended. The course will cover advanced topics, so it's essential to have a strong understanding of design and verification methodologies. To get the most out of this course, it’s recommended that you meet the following prerequisites:

The application of assertion techniques and the related languages have been continuously updated and developed. As assertion languages are designed to express complex behaviors, the ongoing development of assertion techniques allows us to better utilize assertions as an important verification method. SVA provides many structures and operators that are not commonly used. These powerful structures can describe complex sequences. However, not all property structures or operators are useful. It is important to compare the advantages and disadvantages of these new structures or operators with traditional sequence descriptions to decide whether to use them.

Assertion Based Verification provides an effective way to improve quality of verification by providing better controllability and observability of design errors. ABV is enabled with specification of assertions in the design. Assertions are executable specification of the design and are mostly written as 'assert' properties used to check the design functionality and 'cover' properties primarily used for functional coverage. Assertion can be verified using different ABV technologies: Formal, Simulation and Emulation/Acceleration.

Our course focuses on advanced uses of SystemVerilog Assertions (SVA). Here are the main topics covered: First, basic concepts of Assertion-Based Verification (ABV) and systematic ABV methodologies. Second, how to use powerful SVA syntax structures to describe complex assertion sequences with real-world examples. Third, evaluating the pros and cons of new syntax structures or operators and identifying the useful ones through specific cases. Fourth, an overview of the basic principles of ABV and how to construct ABV components using standardized methods. Fifth, analyzing issues of functional verification completeness and setting realistic expectations for the role of EDA tools throughout the verification process.

Assertion-based verification (ABV) is a verification approach where the user specifies design properties in SVA/PSL language and considers assertions as a primary means of verification at each verification stage, while also combining various verification techniques and gradually adopting ABV in the verification flow. This course explores the different verification stages and the verification breakthroughs driven by assertion verification techniques.

The ABV methodology can be applied to formal, simulation, and acceleration verification. Each verification technique corresponds to different verification tools. Based on the advantages and disadvantages of each verification technique, use assertions reasonably and effectively. Many verification environment indicators can be collected in the verification flow. The assertion results reported in formal, simulation, and acceleration verification can be collected together to maximize the achievement of verification metrics.

We can use some powerful constructs for describing complex assertion sequences. Endpoints, Convert the completion of a sequence into a boolean. Allow multiple concurrent sequences to be described. Action blocks, Allow procedural code to be executed on the pass or failure of an assertion. Assertion local variables, Easier definition of complex assertions by accessing local dynamic variables on the completion of a sequence or property. Defining conditional and multi-clocked properties.

Not all property forming constructs or operators are useful. With some exceptions, the operators can often be described in a more straightforward and standard way using sequences. The (especially useful) exceptions being always and followed-by. Just because something is in the LRM does not mean it is good or the only way of doing something.

Properties described using SVA can be designed for reuse, similar to functional design. Here, we explore language features and methods that promote property reuse. By constructing parameterized sequences and properties and using generate statements, we achieve functional-level reuse. Additionally, by using verification components, we can encapsulate properties and auxiliary code into a module, achieving module-level reuse.

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

Functional Verification is about risk management not verifying everything. We need to minimize the chances of a critical bug escaping the verification process. There are many tools and methodologies to help us do this. We cannot abdicate the responsibility for thorough verification to automation. Automation only helps with managing data, predictable repetitive task and computing. Functional Verification is still a human process vulnerable to human error. There is no single verification methodology which worst best for every circumstance all of the time.