ECE/CS 5740/6740 - CAD of Digital Circuits and Systems

CAD of Digital Circuits - Logic Synthesis and Optimization

M, W, F, 11:50am - 12:40pm, LCB 215

Mid-Term Exam: Thursday March 7, 5pm - 7pm in WEB L104

Here is the mid-term exam syllabus

Final Exam: Friday, April 26, WEB 1250, 10:30am - 12:30pm

Final Exam Syllabus: final-exam.syllabus

Final exam schedule can be found here.

Practise test can be downloaded from here: 2019 final exam practise questions.

Instructor, TA and Office Hours

Instructor: Priyank Kalla

Office: MEB 2260

Office Hours: Tuesday, Wednesday 1pm-2pm

TA: No TA. I'll help you :-)

Course Downloadables

Class organization, grading, etc.

Course Syllabus

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: from this URL.

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.

Textbook

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

01/07: An 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/09 - 01/11: Getting started: Slides on Boolean algebra and Boolean operations slides 2 and slides 3 .

01/09-01/11: Shannon's expansion, Boolean Difference, Consensus and Smoothing operations, Unate and binate functions. Introduce the idea of Binary Decision Diagrams as a graph-based data-structure for efficient Boolean function representation and manipulation.

Here are some notes on Generalized cofactors, and how they can be used for Boolean function decomposition.

01/14-onwards: Formal study of Binary Decision Diagrams (BDDs). Here is a set of slides for BDDs:

BDD basics ,
BDD composition from circuits: ITE and the symbol table implementation ,
Concluding BDDs .
As an example application of how to synthesize circuits using BDDs, here is a paper on Synthesis with Pass Transistor Logic. To get a basic idea, just browse through Sections 1, 2 and 3.

01/23: 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 Synthesis.

Here are a (somewhat elaborate) set of slides describing the SAT problem: The SAT problem and SAT solvers. slides updated Feb 1. The slides describe resolution, chronological and non-chronological backtrack based search, UNSAT cores, and Craig Interpolants.
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.

01/30: Wrapped up basic concepts of SAT. Moved on to Two-level logic minimization.

01/30: Preliminary concepts of primality, minimality, irredundancy and minimum cardinality of two level covers: Here are the slides. slides updated Feb 1.
01/30: And here are some scanned notes on primality and irredundancy and circuit testability.
02/03: The recursive approach to prime implicant generation. Slides slides updated Feb 1.
02/05 - 02/13: 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.
Also, here are the slides (courtesy Prof. Chris Myers) on the UCP and BCP formulations and solving the covering table using branch-and-bound.
02/13: Finished Chapter 4 in the textbook.
2/15, 2/18, 2/20: Heuristic minimization of two-level covers: Espresso (Chapter 5)
- Here are the slides that we covered in class. The study of Espresso's approach.

2/20 onwards: An overview of multi-level logic synthesis: Algebraic factorization model versus the Boolean function decomposition theory and challenges

02/20: Start with the Boolean Decomposition Model

Simple disjunctive decomposition, to Ashenhurst/Curtis, to Bi-decomposition. Here are the slides on Ashenhurst/Curtis type decomp.
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 .
The theories of Boolean function decomposition, AND decomp on K-maps, and how to solve it on BDDs.
Studied AND and OR bi- decompositions on BDDs.
03/04: Finished the BDS paper, studied MUX and XNOR decomp.

03/04: Now we will study the Algebraic Model, as employed by the SIS tool.

03/04: Algebraic expression, factored forms and Weak Division. Here are the slides on the algebraic model and the factored form representations.
03/04: 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/25: The model of AIGs, the ABC tool and Boolean decomposition using SAT solvers.

Here is a set of powerpoint slides from a former UMass student that describes contruction and functional reduction of AIGs (called FRAIGing).

03/27-03/29: Study of the Partial Logic Synthesis Problem: With application to synthesis of Rectification and Engineering Change Order Patches:

Here are the slides: Partial Synthesis

4/01 - 4/10: Minimization of incompletely specified machines. Chapter 8, Sections 8.1 and 8.2.

4/12-4/15: The Input Encoding Problem. Here are the slides: encoding.pdf. Particularly, we study the dichotomy-based input encoding problem (DIET).

Here is the PDF file for the DIET paper, by Yang and Ciesielski.

4/15: Multi-level encoding, JEDI. Section 8.3.1.

4/22: 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:

Timing analysis
And here are some slides that consolidate these concept on PPT: timing.ppt.

Reading Assignments

For the week 01/07-01/11: 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 required.

Homeworks

HW 1 has been assigned. Download it from here. Due on Friday 1/25.

HW 1 solutions are here. For Q6, the ROBDD pseudocode, take a look at the solutions here, along with the examples that depict the operation: Solution, HW 1, Q6.

Homework 2, A simple programming assignment with BDDs, for you to get used to the BDD package. Due by Monday 18th.

Download the BDD package from github: https://github.com/ivmai/cudd , or better yet, download the GZIPPED tarball from here.
You will also need this main.c file.

HW 2 solutions are here.

Homework 3, based on two-level logic optimization, simple disjunctive decomp and Ashenhurst-Curtis Decomp is assigned. Due date: Tuesday March 5.

Solutions to HW 3:

Question 1 solutions on prime computation .
Question 2 solutions on on the UCP table covering.
Question 3 solutions on Tautology Checking .
Question 4 solutions on Two level heuristics (containment, expand, essential) .
For questions 6 & 7: Solutions for Simple Disjunctive decomp and Ashenhurst-Curtis Decomp related questions are available from here.

HW 4 is assigned, to give you some practise with kernel extraction based multi-level synthesis using Weak Division and also Boolean Bi-Decomposition. Download HW 4 from here.

In Q5, you will need to experiment with this file: hw5.eqn.
HW 4 solutions are here.
HW 4 Q3, Common sub expression extraction hw4Q3.txt.

HW 5 uploads:

Here is the HW 5 assignment, due next Wednesday, April 24.
These are some BLIF files designs: C7552.blif The HW question asks you to experiment with these files.
HW 5 solutions are 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: Feb 20.

Many of these projects can easily turn into MS thesis or projects.

Software, tools, benchmarks

Binary Decision Diagrams: The ROBDD Package

To download the CUDD package, please go to Prof. Fabio Somenzi's website at 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.

Here is the picoSAT website from where you can download and compile the source code. MAC OS users can find one through MacPorts.
Here is the Lingeling website
Here is the zchaff website from where you can download and compile the source code.
Here is a linux binary that I use zchaff on the CADE machines.
Here is a sample CNF file in the DIMACS CNF format that these SAT solvers can take as input.
Here is a blif2cnf perl script. Feel free to use it.

Linear Program

Download LPSolve - an integer-linear program solver (executable compiled on LINUX machines) and some sample .lp files:

exam_table_cover.lp .
Another lp example which is infeasible.

SIS-related materials

Espresso - Two-level logic minimizer

Espresso, compiled for Linux download Espresso

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 , lib2_latch.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.