Title:	ECE 6960 - Hardware Model Checking, Spring 2009
Instructor:	Ken Stevens, kstevens@ece.utah.edu, MEB 4506, 585-9176
Classes:	Thu 2:00pm - 3:20pm, Web 1450
Office Hours:	by appointment
Web Page:	www.eng.utah.edu/~kstevens/6960/6960.html
Prerequisites:	Instructor Approval

The purpose of this course is to prepare you to model and verify hardware systems. This course will primarily apply model checking. It will make clear the importance of formal verification to the design process, teach you about process logics and generating formal models, understanding of the lattice of formal equivalence relationships, how to weaken relationships to apply to compositional circuit verification, and you will learn how to apply temporal logic. We will also briefly discuss the difference between model checking and higher order logics.

Required Textbook:
None.
Handout materials will be provided in class.

Disability:	If you have one that needs addressing contact the instructor immediately in the beginning of class.
Add/Drop Policy:	The University is very strict on this, and we abide by their policy in this course.
Incomplete Policy:	Due to the project nature of the class, you cannot get an incomplete unless you have a documented medical or legal emergency or military call.

Grades will be determined as follows:

Homework:	65%
Exam:	35%

Following are the lecture notes and outside material that was covered during lectures.

Concurrency and Formal Languages

Concurrency Laws and Axiomatizations

Formal Equivalence Definitions