Requisites: Restricted to graduate students in Electrical Engineering (EEEN) or Electrical/Computer Engineering (ECEN) or Electrical Engineering Concurrent or Electrical/Computer Engineering Concurrent Degree students only.
Covers theoretical and practical aspects of verification of finite-state systems (hardware) and infinite-state systems (programs). Model checking: temporal logics, explicit-state and symbolic search, BDDs. Constraint solvers: SAT solvers, decision procedures. Program verification: invariants, partial vs total correctness, abstraction. Recommended prereq., ECEN 2073 or CSCI 2824. Department enforced requisite., general proficiency in discrete mathematics and programming. Same as CSCI 5135. Requisites: Restricted to any graduate students or Electrical/Computer Engineering or Electrical Engineering Concurrent Degree majors only.
Studies synthesis and optimization of sequential circuits, including retiming transformations and don't care sequences. Gives attention to hardware description languages and their application to finite state systems. Also includes synthesis for testability and performance, algorithms for test generation, formal verification of sequential systems, and synthesis of asynchronous circuits. Recommended prereqs., ECEN 5139 and CSCI 5454.
