TTh200-320 TCH LG76

Prof. Hai Zhou

haizhou@ece.nwu.edu

L461 Tech Institute

(847) 491-4155

Office Hours: MW 3-4P or by appointment

The biggest challenge in digital system design--verification is obviously included since no one wants incorrect designs--is to maintain the complexity at a manageable level. Different from all previous artifacts made in human history, digital systems must work under a vast number of different environments (and inputs). Considering the behavior of a system case by case is no longer working, either in design or verification. Formal techniques treat a design as a mathematical object and establish its behavior from its structure through mathematical reasoning--that is, proofs. In this course, we will study a selected set of formal techniques and their applications in digital system design and verification.

- Chapter on "Propositional calculus" in D. Gries and F. B. Schneider, "A Logical Approach to Discrete Math", Springer-Verlag-New York, 1993.
- (optional) E. W. Dijkstra, The calculus of boolean structures (Part 0), EWD1001.
- Chapter on "Predicate calculus" in D. Gries and F. B. Schneider, "A Logical Approach to Discrete Math", Springer-Verlag-New York, 1993.
- (optional) E. W. Dijkstra, The calculus of boolean structures (Part 1), EWD1002.
- R. W. Floyd, Assigning Meanings to Programs. In J. T. Schwartz (ed.), "Mathematical Aspects of Computer Science", vol. XIX of Proceeding of Symposia in Applied Mathematics. Providence: American Mathematical Society, 1967.
- C. A. R. Hoare, An Axiomatic Basis for Computer Programming. Communications of the ACM, vol. 12, no. 10, Oct. 1969.
- M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: Engineering an Efficient SAT Solver. DAC 2001.
- L. Zhang, C. Madigan, M. Moskewicz, S. Malik, Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. ICCAD 2001.
- Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, Vol. C-35, No. 8, August, 1986, pp. 677-691.
- Chapters on "Temporal Logic" and "Model Checking" in E. M. Clarke Jr., O. Grumberg, and D. A. Peled, "Model Checking", The MIT Press, Cambridge, London. 1999.
- K. McMillan's tutorial on verification: introduction, model checking 1, model checking 2, symbolic model checking

Recommented books:

D. Gries and F. B. Schneider, "A Logical Approach to Discrete Math",
Sringer-Verlag New York, 1993.

Grading: 10% class participation 90% homeworks and projects

Week 1-2 (3/31-4/11)Introduction to logic: propositional calculus, predicate calculus and proofs

Week 3 (4/14-18)Correctness for programs: Floyd's method and Hoare's logic

Week 4 (4/21-25)Satisfiability and combinational equivalence checking

Make-up class on Wed. 4/30 10-1130 at Annenberg G29

Week 5-6 (4/28-5/9)BDD and symbolic encoding of states

Week 7-8 (5/12-23)Temporal logic and model checking

Week 9-10 (5/26-6/6)Protocol verification

Please check back often to this page (www.ece.nwu.edu/~haizhou/ece510) for updates and course material down-loading.