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 SystemVerilog Assertions (SVA) and how to write concise and effi...