ECE 510 Formal Techniques in Design and Verification of Digital Systems

Time & Place

TTh200-320          TCH LG76

Instructor

Prof. Hai Zhou
haizhou@ece.nwu.edu
L461 Tech Institute
(847) 491-4155
Office Hours: MW 3-4P or by appointment

Overview

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.

Texts--a set of selected papers will be handed out:

  1. Chapter on "Propositional calculus" in D. Gries and F. B. Schneider, "A Logical Approach to Discrete Math", Springer-Verlag-New York, 1993.
  2. (optional) E. W. Dijkstra, The calculus of boolean structures (Part 0), EWD1001.
  3. Chapter on "Predicate calculus" in D. Gries and F. B. Schneider, "A Logical Approach to Discrete Math", Springer-Verlag-New York, 1993.
  4. (optional) E. W. Dijkstra, The calculus of boolean structures (Part 1), EWD1002.
  5. 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.
  6. C. A. R. Hoare, An Axiomatic Basis for Computer Programming. Communications of the ACM, vol. 12, no. 10, Oct. 1969.
  7. M. W. Moskewicz, C. F. Madigan, Y. Zhao, L. Zhang, S. Malik, Chaff: Engineering an Efficient SAT Solver. DAC 2001.
  8. L. Zhang, C. Madigan, M. Moskewicz, S. Malik, Efficient Conflict Driven Learning in a Boolean Satisfiability Solver. ICCAD 2001.
  9. Randal E. Bryant, Graph-Based Algorithms for Boolean Function Manipulation. IEEE Transactions on Computers, Vol. C-35, No. 8, August, 1986, pp. 677-691.
  10. 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.
  11. K. McMillan's tutorial on verification: introduction, model checking 1, model checking 2, symbolic model checking

    12.  

     

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

Policies

Grading: 10% class participation  90% homeworks and projects

Homeworks

Lecture schedule

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.