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.

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.

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

Sequences are the second level of the SVA structure. Cycle-based properties are usually described using sequences. A sequence contains multiple Boolean expressions separated by ##N, where N is the number of cycles between expressions. This course explains sequences and shows assertions based on them.

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

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.

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 modeled into state space by synthesis tools. They are part of the complexity, so the efficiency of SVA is especially important.

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.

Provide sufficient knowledge on specific designs and protocols to enable lab exercises to be completed. SVA provides an efficient and powerful way to verify designs. The approach to writing properties needs some thought and should be included in the test plan. A "divide and conquer" methodology works well. Plan the structure of your assertions and identify key branch conditions. Declare alternative behaviors and key conditions as sequences. Build compound sequences using conjunction, disjunction, repetition etc. Define enabling conditions and triggers. Use coverage to check assertions are triggered. Remember SVA does not remove the obligation to write a thorough testbench.

Understand the purpose and applications of formal verification, particularly through property checking. Gain insights into how formal verification differs from dynamic simulation in testing design reliability. Recognize how model checking uses mathematical methods to verify that constraints and properties hold under all specified conditions, without relying on test vectors. Explore the specific advantages of using static verification for proving that properties cannot fail, contrasting with dynamic verification that relies on test stimuli. Familiarize yourself with how to structure constraints and assertions effectively to enhance verification completeness, ensuring that the verification outcomes are as accurate as the property definitions.