University of Colorado at Boulder
University of Colorado at Boulder Search A to Z Campus Map CU Search Links
ECE Home
Course List
Contact Us

ECEN 5139 - Formal Verification of VLSI Systems

Catalog Data ECEN 5139 (3). Formal Verification of VLSI Systems. Covers two-level and multilevel minimization, optimization via expert systems, algebraic and Boolean decomposition, layout methodologies, state assignment, encoding and minimization, silicon compilation.
Credits and Design 3 credit hours. Elective course.
Prerequisite(s) ECEN 2703, Discrete Mathematics,
and general proficiency in discrete mathematics and programming.
Textbook Lecture notes.


  1. Synthesis and Optimization of Digital Circuits, G. DeMicheli, McGraw-Hill, New York, 1994.
  2. Logic Synthesis, S. Devadas, A. Ghosh, and K. Keutzer,McGraw-Hill, New York, 1994.
  3. Symbolic Model Checking, K. L. McMillan, Kluwer AcademicPublishers, Boston, 1994.
Course Objectives Automatic synthesis is a key tool in the development of VLSI systems and the knowledge of its techniques and applications has become vital for circuit and systems designers. Students who take this course learn how to use and write synthesis and verification tools.
Topics Covered
  1. Binary Decision Diagrams.
  2. Reachability analysis.
  3. Formal verification techniques: Model checking and language containment.
  4. Solution of boolean equations.
  5. Symbolic synthesis of combinational circuits.
  6. Test generation for sequential circuits.
  7. Optimization of sequential circuits.
  8. Synthesis for low power.

Last revised: 08-02-11, PM, ARP.