ECE/CS 5740/6740 - CAD of Digital Circuits and Systems
CAD of Digital Circuits - Logic Synthesis and
M, W, F, 10:45 - 11:35, WEB 1250
Final Exam: Wednesday, May 4, WEB 1250, 10:30am - 12:30pm
Final Exam Syllabus: final-exam.syllabus
A Practise Test with solutions is coming up here....
Instructor, TA and Office Hours
Instructor: Priyank Kalla
Office: MEB 4512 (east side penthouse, in front of the elevator)
Office Hours: Wednesday, noon - 1pm
TA: Xiaojun Sun, Email: firstname.lastname@example.org
TA's office hours: Monday 1:30 - 2:30, and Wednesday 3-4. Office
hours will be held in MEB 4120 (west side penthouse in MEB).
Class organization, grading, etc.
Course Objective and Description
Canvas access and Class Mailing/discussion List
I have setup Canvas for all the four sections (ECE/CS 5740/6740)
of this course. The Canvas page can be accessed:
Important: All the course content can be accessed through this
website. Canvas can be used for discussions on any course-related topic,
tool usage, and also for uploading programming assignments. I may
upload some lecture videos also on the Canvas page.
Title: Logic Synthesis and Verification Algorithms, by
Profs. Gary Hachtel and Fabio Somenzi. Publisher:
Springer. Available through the bookstore.
This is what the book looks like.
Lecture Notes and Slides
Introduction to CAD and
Synthesis . A basic introduction to the course - particularly for
those of you who don't really have a good idea about what Logic
Synthesis is about.
01/13 - 01/15: Getting started: Slides on Boolean algebra and
Boolean operations slides 2 and slides 3 .
01/20: Shannon's expansion, Boolean Difference, Consensus and
Smoothing operations, Unate and binate functions. Introduced the idea
of Binary Decision Diagrams as a graph-based data-structure for
efficient Boolean function representation and manipulation.
01/22: Formal study of Binary Decision Diagrams (BDDs):
Here are a set of slides for BDDs:
From BDDs to FDDs and BMDs, etc. These topics
can be potential class projects as CAD implementations. Here is the
Binary Moment Diagrams from Prof. Bryant.
01/25: After we finish BDDs, we will study the Boolean
Satisfiability (SAT) problem. The SAT problem is a decision problem
that finds wide applications in verification as well as in Logic
02/01: Wrapped up basic concepts of SAT. Moved on to Two-level
Here are a (somewhat elaborate) set of slides describing
the SAT problem: The SAT problem and
SAT solvers. The slides describe resolution, chronological and
non-chronological backtrack based search.
- Solving The Boolean Satisfiability Problem. Here is
the technical report on
GRASP -- Generic Search for Satisfiability that describes SAT
solvers, conflict-analysis and non-chronological backtracking.
2/19, 2/22: Heuristic minimization of two-level covers: Espresso
2/24: An overview of multi-level logic synthesis: Algebraic
factorization model versus the Boolean function decomposition theory
- 02/03: Preliminary concepts of primality, minimality,
irredundancy and minimum cardinality of two level
covers: Here are the
slides. slides updated 2/18.
- And here are
some scanned notes on
primality and irredundancy and circuit testability.
- 02/05: CUDD + SAT Demo by Xiaojun
- 02/08: The recursive approach to prime implicant generation.
slides updated 2/18.
- 02/10: Formulating the Table Covering Problem: First, let us
review the theoretical concepts, then we will build the branch and
bound algorithm. Here are the slides that we used to show examples
of row and column covering: Row and
Column covering examples.
- 2/12, 2/17: Finished Chapter 4 in the textbook.
3/4: Start with the Boolean Decomposition Model
- 2/26: Algebraic expression, factored forms and Weak
Division. Here are the slides on the
algebraic model and the factored form representations.
- 2/29: Kernels, co-Kernels and their computation. And here are the
slides on algebraic division and
kernel set theory.
- 3/2: Introduced the Rectangle Covering Problem
- 3/4: Complete the algebraic model: Common Subexpression
Extraction, identifying common cubes from multiple expressions, and
identifying common subkernels. Also covered resubstitution.
3/28: The model of AIGs, the ABC tool and Boolean decomposition
using SAT solvers.
- 3/7: Simple disjunctive decomposition, to Ashenhurst/Curtis, to
Bi-decomposition. Here are the slides
on Ashenhurst/Curtis type decomp.
- 3/9: We will finish Ashenhurst/Curtis type decomposition, and
move on to Bi-decomposition. Here are some
slides on Bi-decomposition and how
to do it on BDDs . Also, attached is the paper that describes all
these results: BDS: BDD-based Bi-decomp
- 3/21: The theories of Boolean function decomposition, AND decomp
on K-maps, and how to solve it on BDDs.
- 3/23: Studied AND and OR bi- decompositions on BDDs.
- 3/25: Finished the BDS paper, studied MUX and XNOR decomp.
4/8: We studied timing issues (arrival times, required times and
slack) false paths, static sensitization. Here are some slides on
timing issues and timing optimization. These slides are made
available courtesy Andreas Kuelhmann:
4/18: Minimization of incompletely specified machines.
- Here is a set of
powerpoint slides from a former UMass student that
describes contruction and functional reduction of AIGs (called
- 3/30: Will study Mishchenko and Steinbach's model of
bi-decomposition, and then study how to model it using a SAT
- 4/1: Here are
some slides, borrowed from Prof. Roland Jiang, on
Bi-decomposition using AIGs and SAT solvers.
For the week 01/11-01/18: Chapters 1 and 2 are introductory
chapters that give a brief overview of logic synthesis. I suggest the
class should read these chapters this week. There is no need to get
into the nitty-gritty details, just an overview is what is
Sometime ago I had prepared some brief notes about these
concepts. I am attaching them for your bedtime-reading:
Lects 2 and Lects 2-3-4 . Have fun.
For the week 01/25 - 01/29: Read Chapter 6 in the textbook on BDDs.
For the week of 2/1 - 2/7: Please read the technical report on
GRASP, and along with my
slides, understand the non-chronological backtrack search in CDCL
For the weeks of 2/8-2/21, read chapters 4 and 5 in the
For the week of 3/28 - 4/1, read the Yang and Ciesielski paper on
BDD-based Boolean decomposition.
4/13: Reach Chapter 11 in the textbook on don't cares. Also
please study the solved problems at the end of the chapter.
HW 1 has been assigned. Download it
from here. Due on Friday 1/29 in the
HW 1 solutions are here.
A simple programming assignment with BDDs. You will also need this
Homework 3, based on two-level logic
optimization is assigned. Due date: Monday March 7. HW problem Q5 updated 2/29.
Solutions to HW 3 are available from here.
A very short HW 4 is assigned, to give you some practise with
kernel extraction based multi-level synthesis. Download
HW 4 from here. Please try to complete
it and submit by noon on Thursday, as the exam will be mailed to all
of you at that time.
Here's a solution for HW4,
Q3. Qs 1 and 2 are trivial. You can compare your results by
using the print_kernel command in SIS.
HW 5 uploads:
HW 6 is uploaded here. Due by
Friday April 29, 5pm sharp. I'll upload solutions by 5pm on April
HW 6 solutions are uploaded here.
Options for Class Projects
Here is a description of class
projects that you could
pursue. Take a look. I will keep on updating this document as and
when I find more time and more information. Class
project document latest update: 3/22, 8am.
Many of these projects can easily turn into MS thesis or
Project submission instructions are
Submission Instructions. Projects are due no
later than Monday May 9.
Software, tools, benchmarks
Binary Decision Diagrams: The ROBDD Package
To download the CUDD package, please go to Prof. Fabio Somenzi's
http://vlsi.colorado.edu/~fabio/ , and download the CUDD
package. Also this link
takes you to the main documentation for CUDD.
Boolean SAT tools
Many SAT tools are available in public domain. For our purposes,
Lingeling, PicoSAT and/or zCHAFF will suffice.
Download LPSolve - an
integer-linear program solver (executable compiled on LINUX machines)
and some sample .lp files:
Espresso - Two-level logic minimizer
Espresso, compiled for Linux
Espresso manual can be downloaded from
at this Berkeley website . BEWARE - there is a whole lot of
information here, most of which you don't need right now. Just run
'espresso -h' (h = help) and you'll figure out most of the stuff.
Here is the 3-input majority
function written in kiss format.
FSM Minimization and State Assignment
State Minimization Download stamina
and an example state machine in fsm.kiss file from here
Two-Level State Encoding Download Nova
Multi-level Logic Optimization System: SIS
SIS compiled for linux: Download SIS executable
SIS Manual/paper: SIS paper
STD. Cell Library: lib2.genlib
Here are some .blif and .pla files:
des.blif , alu4.pla and 9sym.pla .
Here is file script.rugged
and script.delay .
Utility packages - arrays, lists, symbol tables - for your projects
Packages: tar'ed and
gzipped here .
The ABC tool from Alan Mishchencko, UCB
Go to Alan's website for the ABC synthesis tool and get the ABC
tool. This is the most advanced logic synthesis tool (techniques)
freely available. Link to
Alan's Website is here.
This is an older version of my own personal copy
of compiled linux binary of ABC.
Some benchmarks for experimenting with projects
Here is a gzipped tarball
of a few benchmark designs that you can use for
synthesis experiments and for your class projects.