University of Massachusetts, Amherst
Department of Electrical & Computer Engineering

ECE 667 / 597 SV - Synthesis and Verification of Digital Systems
Fall 2021

Instructor: Maciej Ciesielski

Knowles Engineering Building (KEB) 209D
Phone: (413) 545-0401
Lectures: Tu, Th, 10:00 - 11:15 AM

Office hours: Mon., Wed. 2:00 - 3:00 or by appointment
ciesiel@ecs.umass.edu


  • 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 simulation based verification techniques; combinational and sequential equivalence checking; model and property checking; satisfiability (SAT); and functional test generation.

    Course Information

    This course presents a modern approach 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, with emphasis on formal methods (equivalence checking and model checking) and satisfiability.

    Grading

    There will be five homework assignments, one midterm exam (testing your knowledge of theory) and the final exam. Homework assignments will include the use of synthesis tools, such as GAUT, ABC, BDS, TDS, and commercial tools, available on CSE Unix servers.

    The final grade will be determined as follows:

    • Homework/project assignments - 40%
    • Midterm exam - 30%
    • Final exam - 30%
    NO INCOMPLETE grades will be allowed, so please plan accordingly.

    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).