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

CAD of Digital Circuits - Logic Synthesis and Optimization

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: xiaojun.sun@utah.edu
  • 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).

    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/13: 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/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 paper on 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 Synthesis.
  • 02/01: Wrapped up basic concepts of SAT. Moved on to Two-level logic minimization.
  • 2/19, 2/22: Heuristic minimization of two-level covers: Espresso (Chapter 5)
  • 2/24: An overview of multi-level logic synthesis: Algebraic factorization model versus the Boolean function decomposition theory and challenges
  • 3/4: Start with the Boolean Decomposition Model
  • 3/28: The model of AIGs, the ABC tool and Boolean decomposition using SAT solvers.
  • 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.

    Reading Assignments

  • 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 required.
  • 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 solvers.
  • For the weeks of 2/8-2/21, read chapters 4 and 5 in the textbook.
  • 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.

    Homeworks

  • HW 1 has been assigned. Download it from here. Due on Friday 1/29 in the HW locker.
  • HW 1 solutions are here.
  • Homework 2, A simple programming assignment with BDDs. You will also need this main.c file.
  • 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 29.
  • 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 projects.
  • Project submission instructions are here: Project 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 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.

    Linear Program

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

    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.