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:

This website: http://www.ece.utah.edu/~kalla/index_6745.html, here I will upload all lecture slides, CAD tools and HW assignments.
I have also activated the Canvas Website for the course ( https://utah.instructure.com/courses/890995), where you will submit the HWs assignments and you may also carry class conversations and discussions about HWs, projects, or anything related to the course.

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:

Study of conventional testing and verification technologies, such as SAT solvers, BDDs and AIG-based verifiers. These form the foundation of modern CAD tools and techniques and are in extensive use in industry.
Study of advanced symbolic computation techniques - e.g. computational commutative algebraic geometry to verify datapath circuits;
Hands-on learning, project-based course, CAD tool development;
No exams!!

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:

Hardware Datapath Verification using Algebraic Geometry
I will keep on updating the release. Current update released: May 2017.

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:

An Introduction to Groeber Bases by William W. Adams and Philippe Loustaunau, American Mathematical Society.
"Ideals, Varieties and Algorithms", by Cox, Little and O'Shea. Here is a link to the book from Prof. Cox's website. .

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: Introduction to Test, Validation and Verification A few years ago when I first introduced this course as a "special topic" - Test, Validation and Verification, I gave an introductory write-up about "What exactly is Testing and Verification, and what's the difference?" I hope this write-up will give you an overview of the topics...
8/21: Another set of slides that I had prepared a few years ago to give a 1-hour crash course of testing.

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.

Here are some notes on Boolean functions , along with a set of slides , and some more slides on operations on Boolean functions (Shannon's expansion)

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:

Intro to Boolean algebra, truth tables, to SOP forms, to two-level logic circuits, logic simplification, etc.: slide set 1 on these basics
A slide deck on the concept of universal logic
A slide deck on the concept of logic optimization (minterms, cubes, implicants, primes, and K-Maps)

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.

Some slides to review basic Boolean operations.
Slides on BDDs: BDD Intro
BDD Canonization and manipulation
Conclude BDDs .
Here is the original BDD paper written by Prof. Randy Bryant on ROBDDs.

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.

Here are some SAT slides for use in class The SAT problem and SAT solvers SAT slides updated 8/30/2021
Solving The Boolean Satisfiability Problem. Here is the technical report on GRASP that describes SAT solvers, conflict-analysis and non-chronological backtracking.

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.

Here are some overview slides on how ABC works.
The link/info on the ABC tool is given below on this webpage under the CAD Tools section. It is time to download, compile and install the ABC tool in your account.
Example BLIF files: bcd_7seg.blif, bcd_7seg_opt.blif, bcd_7seg_bug.blif. You may try to prove and disprove equivalence between these 3 designs.

9/20 onwards: The problem of Craig Interpolation and post-verification debugging and rectification of buggy circuits:

Craig Interpolation: Concept given in the slides on Boolean SAT. [SAT slides updated 9/20/2023]
Will show you how to compute two interpolants: the smallest interpolant and the largest interpolant.
The use of Shannon's exapansion, co-factors of a Boolean function, existential quantification, universal quantification and Boolean differences.
Here are some notes on these concepts: quantification-bool-diff-interpolant.pdf.
And finally, we study the topic of Partial Synthesis: With Application to Rectification of buggy circuits using Craig interpolation.

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.

You may revisit the following slides:
Here are some overview slides on how ABC works.
The link/info on the ABC tool is given below on this webpage under the CAD Tools section. It is time to download, compile and install the ABC tool in your account.
Example BLIF files: bcd_7seg.blif, bcd_7seg_opt.blif, bcd_7seg_bug.blif. You may try to prove and disprove equivalence between these 3 designs.

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.

What is the stuck-at fault model? We will cover the material from slide numbers 10-21 from vlsi_test_intro.pdf to introduce the concept.
The basic theory of fault activation and propagation. Here are some notes with solved examples: atpg-fundamentals-notes.pdf.
Testability properties of two-level logic circuits: here are some scanned notes on primality and irredundancy and circuit testability.
10/2 onwards: Slides for ATPG: atpg_redundacy_chkpts_cloud.pdf

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.

Intro to Rings, Fields and Polynomials for hardware modeling.

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]

In the class, I used these notes for exposition: Polyfunction worksheet.

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.

I used the Galois field slides referenced above, along with the following notes: GF-Notes.pdf.
I also gave the first demo of Singular, using the simplest of Singular files: finite-field-basic-demo.sing.

10/23: Continue the study of Galois fields: Irreducible versus primitive polynomials, Conjugates, Minimal polynomials from conjugates, and the notion of field containment.

I used the slides linked above, and used these notes GF-Notes-2.pdf.
Here is a sample Singular file for computations in finite fields to help you get started: finite-field-demo.sing. Feel free to experiment with it.

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.

In the class, we have analyzed the lagrangian interpolation formula, to interpolate a polynomial from a function. Here is a Singular file lagrange.sing that will show you how to implement the interpolation.

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.

I used some of these notes to design a 2-bit GF multiplier, and motivate the Groebner basis of ideals using the analogy of Gaussian elimination: GF-Notes-3.pdf.
Conclude discussions on Galois Fields on 11/1.

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

I used the following notes to explain the ideal-variety correspondences in class: Ideal-variety-notes.pdf
Univariate Division and motivating Groebner bases.

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.

Here is the division example we covered in class with the DEGLEX order multivariate division and how it proceeds. I have also solved the problem with the LEX order.
Here is another Singular Demo file that shows the term ordering usage in ring declarations. It also shows how to access leading terms of polynomials, and how to compute Groebner bases.
Here are the class notes that I used: poly-division-notes.pdf.

11/15: And now we get to Groebner Bases and Buchberger's algorithm: here are the slides.

We will complete our study of Groebner bases, the Buchberger's algorithm, and reduce the Groebner basis to a unique canonical form. Once we have studied and understood the Groebner basis algorithm, then we will start applying Groebner bases for equivalence checking.

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.

We also used these notes on Nov 1 and Nov 3: ordering-division-reduction-gb.pdf.
I gave another demo of Singular: i) spoly.sing , using the library "teachstd.lib" and the use of spoly() function; and ii) demo.sing , functions that can help you to implement division algorithms.

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:

The example on slide 6: f2.sing
The equivalence checking example of the 2-bit multiplier: eq_verify.sing, related to the concepts and example from slides 16-20.
Here are the notes that I used on Nov 20 to explain the concepts: Nullsatz-notes.pdf.
And here are the slides that I marked-up in the class: nullsatz-sat-marked-up-slides.pdf.

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].

Design of unsigned adders and multipliers is taught in undergraduate ECE/CS 3700 as well as ECE/CS 3810. I am providing you some tutorial slides on the design of unsigned adders and integer array multipliers.
Tutorial slides on addition: adder design.
Tutorial slides on fast adders and multipliers: Fast Addition and Unsigned Multiplication.

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: I used the following Singular files to give a demo of this approach: i) Verification of 2-bit GF multiplier 2-bit-SNS.sing; and ii) Verification of a 2X2 integer multiplier using the same RTTO approach by modeling the problem over Q: int-mult.sing.

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:

For this, we will study the very interesting, but somewhat more involved concepts of Radical ideals and Strong Nullstellensatz: slides for Radical Ideals
Finish with I(V(J)) and √ J
11/27 onwards: We used these notes to explain the concept of I(V(J)): Radicals-notes.pdf
11/27 onwards: We further used these notes to explain the concept of Radical(J), the Strong Nullstellensatz over finite fields, and how to use them in Verification: Radicals-Notes-2.pdf
11/27 onwards: Here is a Singular file ivj.sing with examples on Radical ideals and their computation using the radical(J) procedure given in primdec.lib

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]

We will also study an important concept for improving Buchberger's algorithm: The Product Criterion.
11/29: I also used these notes to explain how spec vanishes on a variety, and also how Buchberger's product criteria applies to polynomials with relatively prime leading terms: Verify CUT efficiently using SNS.

12/4: Proving Equivalence of Finite State Machines using Implicit FSM traversal. Here are the : lecture slides for today .

Here are some notes to follow along with the slides: Sequential Verification Notes .

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.

HW #1 solutions are here: hw1_23_soln.pdf.

Here are all the files related to HW 2.

The assignment is described here: hw2_23_prog_assign.pdf.
Here is the main.c file, which is referenced in the HW. You will need to use it. Also, I used this file to give the demo in class.
Here are some BLIF logic circuit benhmarks that you can experiment with: C17.blif, Mastrovito_Fq16.blif, and C6288.blif.

Here is HW 3: hw3_2023.pdf. Due Wednesday Oct 18. In this HW, you may also need some of these files given below:

Here is a blif2cnf perl script. Feel free to use it.
Example BLIF files: bcd_7seg.blif, bcd_7seg_opt.blif, bcd_7seg_bug.blif. You may try to prove and disprove equivalence between these 3 designs.
These are some larger designs: C7552.blif and the optimized netlist C7552_fixed_opt.blif. The HW question asks you to experiment with these files. -- --
ABC can read BLIF files as inputs, and perform combinational equivalence checking, using the cec command.
In Q3, you have to run experiments with Craig Interpolation in ABC, for rectification.
- Here are two blif files to try craig interpolation in ABC: ci_A.blif and ci_B.blif.
- In ABC, Run the command: "inter ci_A.blif ci_B.blif"; and then run "write_blif inter.blif". The interpolant will be written in inter.blif. This corresponds to the example on page 15 of the rectification slide-set.

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.

For the last question on equivalence checking and bug catching in arithmetic circuits, you'll need these two files: i) MastrovitoF_q16.blif, and ii) MontgomeryF_q16.blif.

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.

Here is a sample Singular file for computations in finite fields to help you get started: finite-field-demo.sing. Feel free to experiment with it.
To help you solve Q4, here is a Singular file 2-bit-multiplier-miter.sing that shows how the verification problem is setup for a 2-bit finite field multiplier using an algebraic miter in Singular.
In the class, we have analyzed the lagrangian interpolation formula, to interpolate a polynomial from a function. Here is a Singular file lagrange.sing that will show you how to implement the interpolation. You may refer to it when you solve Q5 on the HW.

HW 5 Solutions can be found here: HW 5 solutions

Here is Singular file for HW 5 Q1: HW 5 Q1 find_primitive.sing
Here is my Singular file for solution to HW 5 Q4: HW5 Q4 Solution , the 3-bit Mastrovito design and its miter against the spec.
Here is Singular file for HW 5 Q5: HW 3 Q5 Lagrange interpolation

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.

You may find these files useful to formulate your decision procedures in Singular:
General Programming in Singular: spoly.sing , using the library "teachstd.lib" and the use of spoly() function; and
More General Programming in Singular, compute reduced GB, use option(redSB), etc: demo.sing
Here is a Singular file ivj.sing with examples on Radical ideals and their computation using the radical(J) procedure given in primdec.lib

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.

Project should be finalized by Nov 15. A 1 page project abstract or summary proposal should be uploaded on Canvas by then.

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.

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.
Also, here is a description of how to use the DIMACS CNF-SAT problem description: CNF file problem description.
Here is a blif2cnf perl script. Feel free to use it.

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 CUDD Package, BDD and ADD Tutorials: https://davidkebo.com/cudd
Here is the documentation for the CUDD package: cudd.pdf.

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.