Hardware Verification Seminar Syllabus

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.