## 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.