Fall 2023

ECE/CS 6745/5745: Testing and Verification of Digital Circuits

Hardware Verification using Symbolic Computation

WEB 1230: 1:25pm - 2:45pm



Instructor:

  • Prof. Priyank Kalla, Office: MEB 4112, Email: kalla@ece.utah.edu
  • You can also send me email via Canvas course page
  • Office Hours: Tuesday 2-3pm, in my office, or if this time doesn't work for you, you can setup an appointment.
  • TA: Ritaja Das, ritaja.das@utah.edu. Ritaja's office hours: Thursday 11am-12pm.

    Course Websites

  • The course will be offered through two websites:

    Course Description

  • The course will cover VLSI Testing and Formal Hardware Verification techniques. This is a fundamental problem in digital circuit/RTL design validation, where it is important to verify whether or not a given circuit implementation is equivalent to its functional specification. This is called 'Equivalence Checking', and this fundamental problem is a foundation for most other formal verification techniques. The course will cover both conventional and advanced formal (mathematical) tools, algorithms and technologies that are employed as core computational platforms to verify such implementations.
  • We will also cover basic concepts of Automatic Test Pattern Generation Techniques to test VLSI circuits for fabrication defects. A major focus of the course will be on:
  • Course Syllabus: Here is a list of topics that will be covered in the course. We may adjust the coverage of these topics depending upon how we are proceeding in the class.
  • This is going to be a very practical, applied and yet a specialized course!

    Textbook

  • I am writing a textbook on the topics related to this course. This book is a work in progress, but I can start releasing some of the chapters associated with the topics we are covering in class. Feel free to download the book:
  • I will provide you with notes, slides, tutorial and published papers that will cover the entire course.
  • There are some texts that can be used as references, particularly to cover computational commutative algebra and algebraic geometry (Groebner bases theory and technology). There are:

    Grading

  • Homeworks & Programming Assignments: 60%
  • Class Project: 40%
  • Each student will have to independently solve the HW assignments, which will include some logic and arithmetic circuit design, algorithm implementation for verification, and performing verification and bug catching. HWs will be assigned every 2-weeks or so.
  • Students will then also form a team of 2 members to work on a term-project (something like a month-long assignment). At the end of semester, a report, software, data, will be submitted for grading.
  • No Exams!

    Attendance

  • Class attendance is essential. Since this course material is not available in any dedicated textbook, if you miss class lectures, then it is going to be very hard to understand the material.

    Cheating/Academic Misconduct

    Students are bound by the ECE academic misconduct policy and the University's Student Code. Cheating on homeworks and projects or plagiarizing constitute academic misconduct in this course and will result in academic sanction. These include copying solutions from other students, submitting someone else's code or experiments as yours, copying the work of others without crediting it to them. Learning from each other is encouraged, but in the end you have to solve the problems on your own, and run your own experiments and make your own observations from those experiments. Academic misconduct on any assignment will result in a sanction in this course up to failing the course. The sanctions are the following:
  • First offense on a homework/laboratory assignment will result in a zero on the assignment.
  • Second offense will result in failure of the course and an incident report will be submitted to the department and college.

    Lecture Notes and Slides

  • 8/21: Introduction to the course

  • 8/21: Let us begin with a review of Boolean algebras, operations on Boolean functions, and (computer) representations of Boolean functions, all in the context of Test/Verification.
  • 8/23: Here is a set of lecture slides that introduces Boolean algebra, truth tables, and logic optimization. These slides are from my undergrad Digital Logic Design Class. On the Canvas page, in the media gallery, you will find video recordings corresponding to these slides. These are very basic, and you can refer to these with those lecture videos to brush up these concepts:

  • 8/28 onwards: We start off with some basics of representation of Boolean functions and operations on Boolean functions. These operations on Boolean functions lead into Binary Decision Diagrams: i) notes on BDDs ; notes on BDD applications.
  • 9/11: A Demo of BDD package and tools, the CUDD Package.
  • 9/11 onwards: Equivalence Checking and SAT Solving. We will study Boolean function solvers, such as SAT and SMT solvers.
  • 9/13 onwards : SAT-solvers, the CNF-formats, resolution, chronological backtrack based search, called the DPLL approach.
  • 9/18 onwards: We will complete our study of non-chronological backtrack based SAT-search with conflict-driven clause learning (CDCL) solvers. I will give you a demo of CNF file formats and SAT solvers.
  • 9/18: Circuit-SAT Solving for Combinational Equivalence Checking (CEC), the ABC Tool, The Berkeley Logic Intermediate Format (BLIF) for logic circuits, and a demo on the use of the ABC tool for CEC.
  • 9/20 onwards: The problem of Craig Interpolation and post-verification debugging and rectification of buggy circuits:
  • 9/25: We continue our study of Rectification of buggy circuits using Craig Interpolation. Compute the On-set, Off-set and the don't care-set of the rectification function for logic optimization.
  • 9/27: We will complete our dicussion with rectification using Craig interpolation. Will give a demo of the use of the ABC tool for Equivalence Checking, and Rectification using Craig Interpolants.
  • 10/2: Today, we will start a new topic: Automatic Test Pattern Generation (ATPG) for stuck-at faults. This helps to detect manufacturing defects, as well as logical errors and redundancies in combinational logic.
  • 10/04: How to reduce the test generation effort? Slides for fault collapsing and checkpoint theorem: atpg fault collapsing and checkpoint theorem.
  • 10/9-10/13: Fall Break.
  • 10/16: We will continue our discussions with reducing the test generation effort: using equivalence and dominance fault collapsing, and complete the checkpoint theorem. We will also look at issues with multiple-stuck-at faults (MSF) and discuss why MSF ATPG leads to the issue of test invalidation. This completes combinational stuck-fault ATPG!
  • 10/16 onwards: Now we move on to Formal Equivalence Checking of Arithmetic Circuits. For this, we will use techniques from Commutative Algebra, Computer Algebra and Algebraic Geometry. We need to build the theoretical framework for Polynomial Modeling of Circuits.
  • 10/18: We will continue with the coverage of basic commutative algebra concepts: Rings, fields, algebraic closure of a field, polynomials representations, etc.
  • 10/18 onwards: Then we need to study finite fields, specifically Galois extension fields, and apply these concepts to model, design and verify digital circuits. Here are the slides for Galois fields and hardware design. [Slides updated 9/23/2019]
  • 10/23: We will begin our discussions of finite (Galois) fields, using the slides linked above.

  • 10/25: We study the construction of Finite Fields, and how to add and multiply elements in finite fields.

  • 10/23: Continue the study of Galois fields: Irreducible versus primitive polynomials, Conjugates, Minimal polynomials from conjugates, and the notion of field containment.
  • 10/30: We will do a quick recap of irreducible and primitive polynomials, conjugates of elements of finite fields, how to reconstruct minimal polynomials of the elements of Galois fields, the concept of field containment and algebraic closures, and then move on to polynomial representations of functions using Lagrange interpolation formulas and design of modulo multipliers. We will complete our discussions with design of an algebraic miter for formal equivalence checking.
  • 10/20: Wrapping up algebraic miters over finite fields. Here is a singular file that describes multiple concepts, such as, how to declare a miter in a finite field, how to declare an ideal (J), and how to compute a Goebner Basis of ideal (J). Also, how to interpret the output of Groebner bases. Here is the file: 2-bit-multiplier-miter.sing.
  • 11/6 onwards: We start investigating symbolic computer algebra algorithms. We begin with: Ideals, Varieties and Symbolic Computation: Ideals and Varieties
  • 11/6: We start with Symbolic Computation: Division Algorithm and Term Orderings Slides updated 9/27/2019
  • 11/8 and 11/13: We cover univariate polynomial division algorithm, Groebner bases in univariate polynomial rings = GCD. Also covered Term orderings in multivariate polynomial rings. Studied multivariate polynomial division.
  • 11/15: And now we get to Groebner Bases and Buchberger's algorithm: here are the slides.
  • 11/13: We completed our study of: i) 3 definitions of Groebner basis (in the slides); ii) Buchberger's S-polynomials, iii) Buchberger's algorithm to compute a Groebner basis; iv) Making a Groebner basis minimal and then to reduce it; v) complexity of a GB.
  • 11/20: Combinational Circuit Equivalence Checking and SAT solving using polynomial algebra: The Weak Nullstellensatz and application to SAT and Verification [Slides updated Nov 4, 2019]
  • We will continue with the Weak Nullstellensatz over finite fields, as given in my slides, and we will also look at how to count the number of solutions (cardinaility of the variety) to an ideal. We'll apply it to equivalence checking via algebraic miters.
  • Here are some Singular files corresponding to the examples in the slides. Also find the notes that I used in class:
  • 11/22: Verify arithmetic circuits using Ideal Membership Testing: slides are here.
  • 11/27: Using the same RTTO based term ordering derived from the circuit, we will now verify integer multipliers using ideal membership. The problem will be formulated over the polynomial ring Q[x1,...,xn].
  • 11/27: Completed the discussion on verification of arithmetic circuits by ideal membership, checking if the spec f in a member of the ideal J + J0. Use of the Reverse Topological Term Order (RTTO), the Buchberger's product criterion.
  • 11/27 onwards: We will now move on to the fundamental concepts behind the ideal membership formulation for verification. This is based on the Strong Nullstellensatz based verification of combinational circuits:
  • 11/29: Finish Radical ideals and the Strong Nullstellensatz, and solve the verification problem efficiently.

  • 11/29: Apply Strong Nullstellensatz over Galois fields to circuit verification in a scalable manner. Here is a set of slides [Slides updated 11/22/2021]
  • 12/4: Proving Equivalence of Finite State Machines using Implicit FSM traversal. Here are the : lecture slides for today .
  • 12/6: We will complete our discussion on Equivalence checking of Finite State Machines, and then move on to an overview of Sequential ATPG for stuck-at faults. We will look at the reasons for untestable faults in sequential circuits, and how to make a sequential circuit a combinational one for testing purposes using Scan Flip-Flops. Some notes: on FSM ATPG problem .
  • 12/6: Sequential ATPG part 2: on FSM ATPG problem, Self Initializing Tests .
  • 12/6: Sequential ATPG part 3 + Scan Design + IDDQ + Delay Faults: Scan Design, IDDQ, Delay Faults: Start from Slide #27 onwards.
  • The last lecture! [Concludes the course!]

    Homeworks and Programming Assignments Fall 2023

  • Here is the first HW to get you started. Due Wednesday, Sept 6: HW 1 . Upload the solutions on the Canvas site.
  • Here are all the files related to HW 2.
  • Here is HW 3: hw3_2023.pdf. Due Wednesday Oct 18. In this HW, you may also need some of these files given below:
  • HW 4 has been assigned, and it is due on Thu 10/26 by Midnight. Download it from here. This is a short homework, should be completed within a week.
  • HW 4 solutions can be found here: HW 4 solutions

  • HW 5 has been assigned. It's a short HW, due November 10th. No extensions this time. Download it from here.
  • HW 5 Solutions can be found here: HW 5 solutions

  • The last HW, HW 6, is assigned. A short HW, only 3 questions for 6745 students, and only 2 for 5745 students. Due by Monday Dec 11. Download HW6 from here: HW # 6.

    Class Projects

  • Students will form a 2-3 member team and work on a class project. The class project will be a study + implementation of a hardware verification/symbolic computation approach.
  • Here is document updated Dec 12, Fall 2023 describing the various options for a class project. You may go through it, as it will give you an idea of what you will accomplish.

    Final Project Submission Guidelines

  • [Project description document updated 12/12/2023 for Guidelines on Project Submission]
  • See the last Section, Section X, in the projects document. It describes what to submit and how.
  • Final project is due by Monday Dec 18, by midnight.
  • Submission archive to be uploaded on Canvas. I've created an assignment for it.

    CAD, Verification and Computer Algebra Tools and Resources

    Compile/Install issues and instructions

  • To install Zchaff, ABC and VIS, here's a document that describes the missing packages that might be needed for successful compiling.

    Boolean SAT tools

    Many SAT tools are available in public domain. For our purposes, Lingeling, PicoSAT and/or zCHAFF will suffice.

    The VIS Verification Package

  • VIS can be downloaded from U. Colorado website: vlsi.colorado.edu/~vis/ .
  • You can also download this gzipped tarball (VIS.tar.gz) that includes the source and the 'vis' binary that I have already compiled and tested on CADE lab1-xx machines.
  • Make sure to read the users manual and the programmer manual later on for your projects.
  • Remember that VIS needs the variable VIS_LIBRARY_PATH to be properly set. See HW 2 for details..

    Binary Decision Diagram Packages

  • To download the Colorado Decision Diagram (CUDD) package, this is the most comprehensive website today, which also includes tutorial content.

    The And-Invert-Graph (AIG) based ABC Package for Equivalence Checking (and Synthesis)

  • 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 a compiled linux binary of ABC.

    Download Singular from the University of Kaiserslautern

  • Download and Explore the Singular Computer Algebra Tool . We will be using this tool extensively!

    FSM Synthesis and Optimization using SIS

  • Download the linux binary of the SIS tool, it runs on CADE machines.
  • Along with the binary, you should download the optimization scripts script.rugged and script.delay, for area and delay optimization, respectively.
  • To map the circuits to a gate-library, try the lib2.genlib and the lib2_latch.genlib .
  • You will also need to download stamina for state minimization and nova for state assignment.
  • Finally, here is an example KISS file for describing FSM as state tables: fsm.kiss
  • Take a look at this README/SCRIPT of my execution of a FSM synthesis on the FSM.kiss file. My comments are denoted by "// Comments...."
  • Shortly, I will upload some demos on how to do reachability analysis on FSMs and sequential equivalence checking

    Hardware Verification Benchmarks and Data

  • Here is a gzipped tarball of a few benchmark designs given in BLIF format that you can use for synthesis experiments and for your class projects. These are combinational multi-level circuits from the ISCAS 85 benchmark sets.
  • Then there is a set of Finite field arithmetic circuit benchmarks that you can download from two websites: i) Jinpeng Lv's website; and ii) Tim Pruss' website . These benchmarks also have tools and scripts to translate them from BLIF to SAT to SINGULAR format.

    Typesetting your documents with LaTeX

  • Please download this tarball, gunzip and untar it: latex-for-class.tar.gz. These files can help you getting started with writing documents for the class projects.
  • First, go through the PDF file; then look at the *.tex files, and follow the compile instructions.
  • With the packages that I have provided, this compiles on the CADE-lab machines. Of course, if you would like to install LaTeX on your own machines, install the latest (2014) version of TeXLive [MacTex for Mac]. Instructions available on the internet.