|Instructor: Professor Karem Sakallah, 2213 EECS, email@example.com, 936-1350.|
Time and Place: TT 10:30-12:00, 3437 EECS
Credit Hours: 3
Prerequisites: EECS 478 and graduate standing
Overview: In this course we explore how large complex digital systems are verified to ascertain their functional and temporal correctness. Students who enroll can expect to gain proficiency in state-of-the-art informal as well as formal approaches to verification of large-scale systems. Many of these techniques, and the insights that inspired them, can also be adapted to the verification of other large-scale systems, e.g. complex software. Hands-on experience with a variety of verification tools (equivalence checkers, model checkers, SAT solvers, symbolic simulators, etc.) is an integral part of the course.
Catalog Description: Design specification vs. implementation. Design errors. Functional and temporal modeling of digital systems. Simulation vs. symbolic verification techniques. Functional verification of combinational and sequential circuits. Topological and functional path delays; path sensitization. Timing verification of combinational and sequential circuits. Clock schedule optimization.
Design verification overview; design errors; specification vs. implementation; interfaces.
Functional and temporal modeling of digital systems at various abstraction levels.
Simulation at the gate, register transfer and behavioral levels; Verilog HDL
Symbolic manipulation of Boolean functions; ordered binary decision diagrams.
Circuit satisfiability; conjunctive normal form. Davis-Putnam algorithm and extensions.
Functional verification of combinational circuits; simulation-based; symbolic; formal.
Functional verification of sequential circuits; simulation-based; symbolic; formal.
Timing verification of combinational circuits; topological and functional path delays.
Timing verification of sequential circuits; clock schedule optimization.
Course Assignments and Grading:
Written homework assignments (3 to 4): 30%
Classroom participation: 30%
Term paper/project: 40%