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.

Course Topics:

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%