The course will discuss the application of automated reasoning techniques in the verification of software and hardware components in electronic systems. It will cover basic knowledge of logic, satisfiability solvers, model checking and their applications. This course also includes topics on circuit testing (pre-silicon & post-silicon).

Logic design and physical design are two major steps in the digital design process. This course is an introduction to the automation techniques in the logic design step. It covers the workflow from hardware description languages to gate-level netlists. In this course, we will discuss the theoretic foundations, including the basics of automata theory, lexing, parsing, synthesis and minimization of two-level and multi-level circuits, finite-state machine synthesis and verification, technology mapping, automatic test generation and timing analysis. This course, for the first time, connects frontend techniques of compilers with the introduction of logic synthesis. Compiling techniques and digital logic were typically taught in two separate courses. The combination in this course is intended to provide a more comprehensive view of the underlying techniques of modern logic design automation tools.

N/A