Course Schedule:

Assigned Readings:

Randal Bryant, "Symbolic Boolean Manipulation with Ordered Binary Decision Diagrams", CMU CS Tech Report CMU-CS-92-160. Sections 1 to 3 are the relevant ones for now, although the whole paper is excellent.

Randal Bryant, "On the Complexity of VLSI Implementations and Graph Representations of Boolean Functions with Applications to Integer Multiplication", IEEE Transactions on Computers, Vol. 40, No. 2, February 1991. A general technique for proving BDDs big for certain functions (and getting better intuition about what makes BDDs big).

Karl S. Brace, Richard L. Rudell, and Randal E. Bryant, "Efficient Implementation of a BDD Package", 27th Design Automation Conference, pp. 40-45, 1990. How BDD packages are really implemented.

Randal Bryant, "Binary Decision Diagrams and Beyond: Enabling Technologies for Formal Verification", International Conference on Computer-Aided Design, pp. 236-243, 1995. This is a fairly recent survey of BDDs and BDD variants, which pretty much covers my lecture of January 22.

E.M. Clarke, M. Fujita, X. Zhao, "Hybrid Decision Diagrams: Overcoming the Limitations of MTBDDs and BMDs", International Conference on Computer-Aided Design, pp. 159-163, 1995. HDDs (or k*BMDs) are currently the pinnacle of fancy decision diagrams. This is a more in-depth look at them. (Optional Reading)

Jawahar Jain, Amit Narayan, Masahiro Fujita, and Alberto Sangiovanni-Vincentelli, "Formal Verification of Combinational Circuits", VLSI Design, 1997. This is a survey of verifying combinational circuits. The treatment of each topic is very brief, so you may not get much more out of this paper than from lectures. However, the reference list is superb, so it's a great starting point to track down other ideas. (Optional Reading)

Olivier Coudert and Jean Christophe Madre, "A Unified Framework for the Formal Verification of Sequential Circuits", International Conference on Computer-Aided Design, pp. 126-129, 1990. This paper is fairly tough reading, but it concisely covers the basics of verifying sequential circuits with BDDs. Let me know if you're not able to slog through it, and I'll try to find something easier.

Herve Touati, Hamid Savoj, Bill Lin, Robert K. Brayton, and Alberto Sangiovanni-Vincentelli, "Implicit State Enumeration of Finite State Machines Using BDD's [sic]", International Conference on Computer-Aided Design, pp. 130-133, 1990. By popular demand, this is a somewhat easier-to-read treatment of the basics of sequential verification with BDDs. I will be grief-stricken, however, if you all start saying "smoothing" and "consensus". (Optional Reading)

E. M. Clarke, E. A. Emerson, and A. P. Sistla, "Automatic Verification of Finite State Concurrent Systems Using Temporal Logic Specifications: A Practical Approach", Symposium on Principles of Programming Languages, pp. 117-126, 1983. This is the original paper on model-checking. Aarti Gupta's survey paper (handed out on day 1) also gives a quick overview. Otherwise, this is for your reference to clear up any details missing from lecture. (Optional Reading)

J. R. Burch, E. M. Clarke, K. L. McMillan, D. L. Dill, and L. J. Hwang, "Symbolic Model Checking: 10^{20} States and Beyond", Information and Computation, Vol. 98, No. 2, June 1992. This is the journal version of the original paper on symbolic model checking (which appeared in the Conference on Logic in Computer Science in 1990). The paper goes into more depth than what I expect of you and is rather theoretical, but I want you all to understand symbolic model checking for CTL at least.

David L. Dill, Andreas J. Drexler, Alan J. Hu, and C. Han Yang, "Protocol Verification as a Hardware Design Aid", International Conference on Computer Design, 1992. This is a light weight paper on the value of using very high-level formal verification to debug hardware. It also gives some tricks for verifying cache coherence and link-level protocols, which may be useful for Project 4.

C. Norris Ip and David L. Dill, "Better Verification Through Symmetry", International Conference on Computer Hardware Description Languages, 1993. This paper describes automatic symmetry reductions for explicit state enumeration -- one of the cool tricks that can greatly reduce the number of states you need to explore.

Carl-Johan H. Seger and Randal E. Bryant, "Formal Verification by Symbolic Evaluation of Partially-Ordered Trajectories", UBC Department of Computer Science Technical Report 93-8, April 1993. This is rather long and detailed, but gives enough details to figure out the basics of symbolic trajectory evaluation.

Randal E. Bryant, Derek L. Beatty, and Carl-Johan H. Seger, "Formal Hardware Verification by Symbolic Ternary Trajectory Evaluation", 28th Design Automation Conference, 1991, pp. 397-402. This is shorter and lighter reading than the tech report, but doesn't give enough detail to figure out what's really going on.

Projects:

Project 1 will be assigned on January 20, and due on February 7. Be sure to start early, as I'll be out-of-town from January 25 until February 1. Here is my sample solution to this project.

Project 2 is finally ready! Sorry for the delay. This project is due on Monday, March 3 (extension from Friday, February 28).

Project 3 is ready. This project is due on Wednesday, March 26.

Project 4 is ready. This is due on Friday, April 11.