ECE 510 Formal Techniques in Design and Verification of Digital Systems
Time & Place
Prof. Hai Zhou
L461 Tech Institute
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.
Texts--a set of selected papers will be handed out:
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),
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),
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
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,
K. McMillan's tutorial on verification: introduction,
model checking 1, model
checking 2, symbolic model checking
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
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.