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, especially formal signoff, covers a wide range of technologies and has relatively high requirements for users. There is a big difference between the verification work done by formal verification engineers and traditional simulation engineers. The main job of the traditional simulation engineer is to write test cases to verify the design function, while most of the work of the formal verification engineer is to model the design behavior, which requires the formal verification engineer to understand the design functions deeply.

This course is a fundamental introduction to all important technical points in the current field of formal verification. For each technical point, the course mainly focuses on a brief introduction and concepts but no in-depth discussion. By learning the basics of these technical points, students will have a preliminary understanding of formal verification technology. This course can be used as the first and necessary ladder for everyone who wants to step into the field of formal verification. Moreover, it will lay an indispensable foundation for students to apply formal verification technology to practices in the future.

This course answers many basic questions about the field of formal verification, explains the basic principles of the underlying technology of formal verification, proposes the latest formal signoff methodology, and expounds on the technical development direction in the field of formal verification. By taking this course, you will have a certain understanding of formal verification techniques as well as some basic knowledge of formal methodology.

In order to use formal verification reasonably and effectively, it is often necessary to consider the entire verification flow as a whole to play the role of formal verification. It is very necessary to apply formal methods to the verification flow in a systematic process.

The basic principle of formal verification is to verify the functional correctness of the design based on logical derivation and mathematical proof. Formal tools model the design's behavior. On the compiled design model, through the exhaustive algorithms, formal tools analyze whether the properties are consistent with the design's behavior in all reachable state space cycle by cycle.

In the formal verification, the object of verification is property checking. Identify the design modules suitable for formal verification and abstract their functional features one by one from the specifications of these modules. Translate these features into corresponding properties using a property-based language. Build a property-based formal testbench, and compare the RTL design code with the property checking to verify whether the RTL design code's functionality meets the requirements of the design specifications.

As formal techniques research matures and approaches a level of sophistication required by industry, we must take steps to ensure a successful transfer to this more demanding level. One step is to fundamentally change design methodologies such that we move from ambiguous natural language forms of specification to forms that are mathematically precise and verifiable. Formal property verification is the key ingredient in this methodological change. The end result is improved design quality through improved understanding of the design space, improved communication of design intentions, and improved verification quality.

The complexity is a significant problem in formal verification. In the formal signoff flow, users have to spend a lot of time and effort analyzing and solving the problem of complexity in the design. This course explains the leading causes of complexity in a design, the relationship between the complexity and the properties, and how to reduce the impact of the complexity in formal verification.

Coverage is another significant problem in formal verification. The results of assertions represent the functional correctness of formal verification. However, verification is a matter of confidence, and a complete verification flow must consider completeness. Similar to simulation, formal verification also checks verification completeness through coverage. The main difference is that simulation only has stimuli coverage, while formal verification includes both stimuli coverage and checker coverage.

Formal verification, due to its fully proven nature, enables full functional verification of design modules and can be delivered as a final functional signoff. The formal signoff flow mainly includes two methods: signoff with full prove and signoff with coverage. A comprehensive formal signoff methodology is provided in this course.

In addition to signoff, there are many simple and easy-to-use formal applications for formal verification. These out-of-the-box applications provide corresponding formal solutions for different verification problems, which enable beginners or engineers without formal verification technical backgrounds to quickly and efficiently solve some problems encountered in verification.