This class is a seminar where we will discuss the use of mathematical logic to model, specify, and verify, digital computer hardware. This class is intended to introduce a student to a number of topics in the hardware verification field. Student participation and interest can influence the topics discussed and the assignments given. The point of this seminar is to build up awareness of the hardware verification area so the interested student is ready to purse related topics for a PhD.
The following gives a rough outline of what we will do, but note, this is a tentative agenda. I will have several invited speakers give talks, and these speakers will present when they are available.
Sep 9 Introduction to Hardware Verification Sep 16 Introduction to ACL2 Sep 23 Introduction to ACL2, continued Sep 30 Equivalence Checking Oct 7 Symbolic Simulation, Transistor Analysis Oct 14 Symbolic Trajectory Evaluation, and Model Checking Oct 21 Project Discussions Oct 28 Using ACL2 to Model, Specify, and Verify Hardware Nov 4 Using ACL2 to Model, Specify, and Verify Hardware Nov 11 Student Presentations Nov 18 Student Presentations Nov 24 Student Presentations Dec 2 Wrap-up, Final Exam
The grade for this course will be composed of four equally weighted parts: class participation, a project, several specification and verification problems, and a final exam. The project may be a presentation or it may be a program. One or two of the specification and verification problems may be graded. Relevant technical papers will be provided or referenced and students will be asked to lead discussions about these papers. The final exam will cover some of the concepts presented and discussed. Both the quality and correctness of your work and presentations will determine your grade.