University of Massachusetts, Amherst
Department of Electrical & Computer Engineering

ECE 667 - Synthesis and Verification of Digital Systems
Spring 2011

Instructor: Maciej Ciesielski

Office: KEB 309B
Phone: (413) 545-0401

Office hours: Mo, We 1:00 - 2:15, KEB 309B, or by appointment.

Email: ciesiel@ecs.umass.edu
Lectures: Tu, Th, 1:00 - 2:15, Marston 132

  • Course Objective
  • Course Information
  • Grading
  • Textbook
  • Prerequisites

    Course Objective

    To learn about state-of-the-art techniques and algorithms for synthesis and verification of digital systems. Topics in synthesis cover high-level and architectural synthesis, decision and word-level diagrams, combinational logic optimization, and sequential optimization. Topics in verification include: formal and simultion based verification techniques; combinational and sequential equivalence checking; model and property checking; satisfiability (SAT); and functional test generation.

    Course Information

    This course presents modern approaches to logic design and verification of digital circuits, including the necessary background material in Boolean Logic, Finite State Machines, Decision Diagrams,and satisfiability (SAT).

    The first part of the course covers basic techniques of high-level and architectural synthesis, including operation scheduling, resource allocation and binding. Next, the fundamentals of Boolean algebra, logic function representations, and basic logic optimization algorithms are introduced. We shall concentrate on those parts of the theory that will help you understand how logic synthesis and verification CAD tools work. This is useful to those who want to develop such tools and to those who simply want to use them proficiently.
    The next part will be devoted to logic synthesis, concentrating mostly on multi-level synthesis and technology mapping. Application to both ASICs and FPGAs will be discussed. The last part will cover Verification, including functional test generation, satisfiabiliyt, and formal methods (equivalence checking and model checking).

    Grading

    There will be about 6 homework assignments, one midterm exam (testing your knowledge of theory), presentation of research paper, and the final exam. For those of you doing resarch in this area, there may be an option to do a project instead of the final exam (subject to early approval by instructor).
    Homework assignments may include the use of synthesis tools, such as GAUT, ABC, BDS, TDS, and commercial tools, available on CSE Unix machines. A best project would involve designing and implementing an algorithm or a simple VLSI CAD tool.

    The final grade will be determined as follows:

    • Homework assignments - 30%
    • Midterm exam - 25%
    • Paper presentation - 15%
    • Final exam - 30%
    NO INCOMPLETE grades will be allowed, so please plan accordingly if you choose to take the project option.

    Textbook

    In addition, students will be given a set of handouts and research papers.

    Additional references.

    • Logic Synthesis and Verification Algorithms, G. Hachtel and F. Somenzi, Kluwer Academic Publishers, 1996 (2nd printing). ISBN 7923-9746-0.
      Errata

    • Logic Synthesis and Verification, S. Hassoun, T. Sasao (editors), Kluwer Academic Publishers, 2001. ISBN 0-7923-7606-4.

    • Switching Theory for Logic Synthesis, T. Sasao, Kluwer Academic Publishers, 1999. ISBN 0-7923-8456-3

    Prerequisites:

    Basic logic design; hardware design and organization (undergrad level). Basic course in algorithms is desired but not required (it can also be taken concurrently).