This course requires basic knowledge of digital logic design and hardware description languages like Verilog or VHDL. Familiarity with computer architecture concepts is helpful. Access to a computer with internet connectivity is necessary. Students should be dedicated to completing course modules and assignments, with an interest in advancing skills in formal verification.

Formal verification technology has a wide range of applications and places high demands on engineers, especially in formal signoff delivery, where the work of formal verification engineers is quite different from that of traditional simulation verification engineers. For traditional simulation verification engineers, their main task is to write test cases to verify the functional correctness of designs. However, for formal verification engineers, their primary work is to model design behavior, which requires a thorough and comprehensive understanding of design functions.

Formal verification engineers need to have systematic logical thinking and be able to extract functional features from design specifications to build accurate formal models. This requires not only a solid design foundation but also proficiency in formal verification tools and algorithms to abstract verification problems into mathematical models and complete functional verification of designs.

This course serves as a fundamental introductory course, covering all important technical points in the current field of formal verification. For each technical point, the course mainly provides conceptual introductions, helping learners establish a systematic knowledge framework. Some topics are explained only at the conceptual level without in-depth discussion, which can be further explored in future studies based on project needs.

Through learning this course, engineers can gain a comprehensive preliminary understanding of formal verification technology, understand the differences between formal verification and traditional verification methods, and grasp the role and significance of formal verification in the verification process. This will lay the necessary theoretical foundation for further study of tool usage, algorithm principles, and application techniques in formal verification.

This course can serve as a stepping stone for engineers to enter the field of formal verification and provides an indispensable technical foundation for applying formal verification technology in practical projects to improve verification quality and design reliability.

This course answers many fundamental questions in the field of formal verification. It explains the basic principles of underlying formal verification technology, introduces the latest formal signoff methodology, and provides an overview of the development direction of formal verification technologies. Through learning this course, we will gain a comprehensive understanding of formal verification technology and acquire fundamental knowledge of formal methodologies.

1. Formal verification needs to be used reasonably and effectively. It often requires integration with the entire verification flow to maximize its value. Applying formal methods systematically in the verification process is crucial for improving verification efficiency and quality. Formal verification techniques help cover areas that traditional verification methods cannot exhaustively test by using mathematical proofs to achieve complete verification.

2. The basic principle of formal verification is to prove the functional correctness of designs through logical inference and mathematical proof. Formal tools model the design behavior, and on the compiled design model, exhaustive algorithms analyze the properties cycle by cycle in the reachable state space to determine whether they are consistent with design behavior. This verification approach avoids the risk of missing test scenarios and ensures the completeness and reliability of verification results.

3. In the process of formal verification, the core verification target is property checking. Engineers need to identify design modules suitable for formal verification and extract functional features from their specifications, abstracting them into verifiable properties using property languages. By building a formal testbench based on properties, the RTL design code is compared with the properties to verify whether the design functionality meets the specification requirements.

4. As formal technology research matures and reaches the complexity required for industrial applications, measures must be taken to ensure a successful transition to this higher level. Design methodologies need to change from ambiguous natural language specifications to mathematically precise and verifiable forms. Formal property verification is the key factor in achieving this methodological transformation. It enhances understanding of the design space, improves communication of design intent, and enhances verification quality, resulting in higher-quality design delivery.

5. Complexity issues are a significant challenge in formal verification. In the formal signoff process, users spend a lot of time and effort analyzing and resolving design complexity. The course explains the main factors contributing to design complexity, describes the relationship between complexity and assertion properties, and introduces methods to reduce the impact of complexity in formal verification. Mastering complexity analysis and optimization is an essential skill for completing formal verification tasks efficiently.

6. Coverage issues are another critical challenge in formal verification. The results of property proofs only indicate functional correctness, but verification is about building confidence in completeness. Similar to simulation verification, formal verification uses coverage to check the completeness of verification. The difference is that simulation verification only has stimulus coverage, while formal verification includes both stimulus coverage and check coverage. These two types of coverage complement each other to ensure the comprehensiveness of the verification process.

7. Due to its complete proof characteristics, formal verification can perform thorough functional verification of design modules and can be used as the final method for functional signoff. The formal signoff process mainly includes two approaches: full proof signoff and coverage-based signoff. This course systematically introduces both signoff methods to help learners master the process and criteria for formal signoff and apply them in projects.

8. In addition to signoff delivery, formal verification also offers many simple and easy-to-use applications. These out-of-the-box tools and functions provide efficient formal solutions for different verification problems, enabling beginners or engineers without formal verification backgrounds to solve practical verification issues quickly and effectively. These applications improve the usability and adoption of formal verification and expand its role in the verification process.