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:
- 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:
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: 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.
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.
- 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:
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.
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.
- 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:
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
Subsequent set of topics
11/17: Finish Radical ideals and the Strong Nullstellensatz, and
solve the verification problem efficiently.
11/22: 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/22: 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.
11/29: Projections of varieties, elimination ideals and their
application to Hierarchy Abstraction and Combinational Circuit
Verification
- Here are the
slides on projections of varieties and elimination ideals over
Galois fields. [Slides updated 11/27/2021]
- Application of Elimination: extracting a specification polynomial
from a circuit.
- I used the following Singular file to "extract" a specification
polynomial out of a 2-bit GF multiplier using elimination orders:
polynomial-abstraction.sing.
11/29 + 12/1: Start studying sequential circuit Testing:
Some notes:
on FSM ATPG problem .
12/6: Sequential ATPG part 2:
on FSM ATPG problem, Self Initializing Tests .
12/8: 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:
- 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.
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
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 Nov 6, 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 description document updated
11/06/2023]
- Project should be finalized by Nov 15. A 1 page project abstract
or summary proposal should be uploaded on Canvas by then.
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.