Textbook
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.
This course presents modern approaches to logic design
and verification of digital circuits, including necessary background
material in Boolean Logic, Finite State Machines, Decision Diagrams,
and satisfiability (SAT) algorithms.
The first part of the course will cover high-level and architectural
synthesis of designs described using hardware description languages (HDL).
Next, the fundamentals of Boolean algebra, logic function representations,
and basic algorithms will be 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 third part will be devoted to Logic Synthesis, concentrating mostly
on multi-level synthesis. Novel synthesis methods based on BDD representation
and AIG graphs will be covered in detail here.
Application to both ASICs and FPGAs will be discussed.
Finally, the last part will be devoted to Verification, including
simulation-based validation, functional test generation, and formal
methods (equivalence checking and model checking).
There will be about 6 homework assignments, one midterm exam
(testing your knowledge of theory), presentation of research paper,
and either the final exam or a project.
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 - 20%
- Paper presentation - 10%
- Final project or exam - 40%
NO INCOMPLETE grades will be allowed, so please plan accordingly if you
choose to take the project option.
Althouh there is no official textbook required for the course,
the following text is strongly recommended (it is a great reference to have):
Students will be given a set of handouts and research papers.
The following is a suggested list of references.
- 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
- Logic Synthesis and Verification Algorithms,
G. Hachtel and F. Somenzi, Kluwer Academic Publishers, 1996
(2nd printing). ISBN 7923-9746-0.
Errata