Traditional verification techniques use simulators with handcrafted or random test vectors to validate the design. Unfortunately, generating test vectors is labor-intensive. The overall complexity of the designed systems implies that simulation cannot remain the sole means of design verification. Formal verification is an alternative method to complement simulation. By now, the industry has realized the impact and importance of such tools in their own design and implementation processes.
The objective of the course is to introduce the students to the practical formal verification techniques for hardware/software systems that are beginning to penetrate industrial applications. Topics to be covered include: system modeling specification, formal logics for system verification (Boolean & first-order logic, higher-order logic, temporal logic), model checking, BDDs, application of theorem proving systems.
The class is not a training class. The topics covered in the class are related to computered-aided verification. Some basic knowledge on data structures, algorithms, and programming skills will be required. The students in this advanced graduate class should demonstrate their capability of understanding the fundamentals of the theory and performing the project independently.