Instructor Fabio Somenzi Office: ECOT348 Phone: (303) 492-3466 E-mail: Fabio@Colorado.EDU Office Hours: M 1:00-2:00 W 10:30-11:30 F 10:30-11:30 or by appointment
Today's complex VLSI systems like the above Intel P6 CPU are difficult to verify. On the other hand, the cost of shipping defective products is often prohibitive. In the case of safety-critical applications, the cost may even be in terms of human lives. These factors have spurred interest in formal methods for the verification of hardware and software. The last few years have seen the successful deployment of formal methods in many projects, and the launch of several tools based on them.
Among the formal techniques applied to the verification of hardware, model checking has proved the most popular. In model checking one is given a model of a system and a set of properties that should be satisfied. The model is reduced, if necessary, to a small, finite-state model, and state exploration techniques are applied to check the properties.
Even a comparatively small model can have a huge number of states. Therefore, efficient techniques for state exploration are mandatory for successful application of model checking. Of particular interest are the so-called symbolic techniques, in which sets of states and transitions are represented by their characteristic functions.
This course provides a comprehensive introduction to model checking. The emphasis is on hardware verification, but software verification will be discussed as well. We shall discuss the specification of systems and properties. For the former, we shall use Verilog, while for properties we shall introduce temporal logics.
The model checking algorithms for the most popular temporal logics rely on the computation of fixpoints and on the translation of properties into special automata called omega-regular automata. We shall review both processes, and thus formulate a model checking algorithm for a large class of properties.
As mentioned above, the number of states of a model can be very large. The exponential dependence of the number of states on the size of the model is known as the state explosion problem. The second part of the course will therefore concentrate on techniques to combat this problem. Our main tool will be a data structure named Binary Decision Diagrams (BDDs). BDDs represent boolean functions. Boolean functions, in turn, can be used to represent sets of states and transitions. The advantage is that even very large sets (e.g., 10**100 elements) may have compact representations.
We shall examine BDDs in depth, by studying the basic algorithms, and the BDD-based operations that are at the core of symbolic model checking. Even the shrewdest BDD techniques, however, cannot solve by themselves the state explosion problem. Therefore, we shall consider the important topic of Abstraction. Abstraction consists of deriving a simpler model from the one given, in such a way that the properties of interest can be proved (or disproved) for the original system while working on the reduced system. Various techniques have been devised for abstraction. We shall review some of the most widely used. Finally---time permitting---we shall talk about modeling of software with State Charts and of the related verification problem.
Students will use accounts on departmental Unix workstations for some of the assignments and for the projects. The assignments include the use of existing CAD tools. In particular, VIS, a CTL and LTL model checker.
Grading will be based on the homework, a programming project, one mid-term exam and the final exam. Both exams will be take-home exams. Homework will be assigned often and in general you will have one week to do the assignment. The programming project will be assigned by mid September and due two months later.
The final grade is determined as follows:
Homework assignments and solutions are posted on Moodle. Students in ECEN 5139 should visit that site and create an account. They should also register for the course on that site. Registration is enabled by a key that will be given to students in class during the first lecture. If, for any reason, you need to register, but do not have the enrollment key, contact the instructor.
Class notes will be available on Moodle.
Verilog Model of Peterson's Mutual Exclusion Algorithm.
Verilog Model of the instruction buffer model.
Reference books:
Useful links: