University of Massachusetts, Amherst
Department of Electrical & Computer Engineering

ECE 667 - Synthesis and Verification of Digital Systems
Spring 2009

Instructor: Maciej Ciesielski

Office: KEB 309B
Phone: (413) 545-0401
Office hours: Wednesday, 1:30 - 3:00 or by appointment.
Email: ciesiel@ecs.umass.edu
Lectures: Tu, Th, 9:30 - 10:45, LGRC A205

  • 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, including combinational and sequential equivalence checking, 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 allow one to 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 simulation-based validation, functional test generation, 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 (more project oriented) or a project (subject to early approval by instructor).
    Homework assignments may include the use of synthesis tools, such as SIS, VIS, BDS, TEDify, and commercial tools, available on CSE Unix machines. The optimal project will involve designing and implementing an algorithm or a simple VLSI CAD tool. Possible projects will be discussed in class during the first few weeks of the course. Students must choose between the final project and the final exam.

    The final grade will be determined as follows:

    • Homework assignments - 30%
    • Midterm exam - 25%
    • Paper presentation - 15%
    • Final exam (or project) - 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).