ECE/CS 6745/5745: Testing and Verification of Digital Circuits
Hardware Verification using
Prof. Priyank Kalla, Office: MEB 4512, Email: firstname.lastname@example.org
Office Hours: Monday after class 3-4pm, Tue 11am - 12pm, or by appointment
TA: Xiaojun Sun, Email: email@example.com. TA hours:
WEB L105: 1:25pm - 2:45pm
- Wednesday 10am - 11am; and Thursday 3pm - 4pm.
- Office hours will be held in MEB 4120 (West-side penthouse 4th floor).
The course will cover 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. A major focus of the course will be on:
Here is a list of topics that
will be covered in the course.
This is going to be a very practical, applied and yet a
- Study of conventional verification technologies, such as SAT
solvers, BDDs and AIG-based verifiers
- Study of advanced symbolic computation techniques - e.g.
computational commutative algebraic geometry to verify datapath
- Hands-on learning, project-based course, CAD tool development;
- No exams!!
There is no textbook requirement for the course. 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:
I had told you in class that 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:
Homeworks & Programming Assignments: 50%
Class Project: 50%
Class attendance is very important. 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.
Lecture Notes and Slides
8/25: 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/25: Another set of
slides that I had prepared a few years ago to give a 1-hour
crash course of testing.
8/27: 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/27 + 9/3: These operations on Boolean functions lead into
Binary Decision Diagrams: i) notes on
BDDs ; notes on BDD
9/8 + 9/10 + 9/15: After studying BDDs, we will study Boolean function
solvers, such as SAT and SMT solvers.
9/15: The SAT slides have been updated to include CDCL,
9/15: After SAT solvers, we will study AIG-based verification.
9/17: From AIGs to SMT (brief overview) to Word-level
Verification and algebraic geometry. Here are
some overview slides.
9/22 + 9/24: Intro to Rings, Fields and Polynomials for hardware modeling. [Slides updated 9/24]
9/24: Ideals, Varieties and Symbolic Computation:
Ideals and Varieties
9/29: Symbolic Computation:
Division Algorithm and Term
Orderings Slides updated 10/1
10/1: Multivariate Division and motivating Groebner bases.
10/6: Groebner Bases and Buchberger's algorithm:
here are the slides.
Slides updated 10/8
10/8: Study more Groebner bases, with examples, and then move on
Nullstellensatz and application to SAT [Slides
10/13 - 10/15: Fall Break!
10/20: Nullstellensatz and Groebner Bases
- Here are some SAT slides for use in class
The SAT problem and SAT solvers
SAT slides updated 9/15
- Solving The Boolean Satisfiability Problem. Here is
the technical report on
GRASP that describes SAT solvers, conflict-analysis and
10/22: Then we need to study Galois extension fields and apply
Nullstellensatz and Groebner bases to circuits using the Galois
extension field theory! For this, we will study what are Galois
fields. Here are the slides for Galois fields and hardware design. [Slides
10/27: Weak Nullstellensatz based verification of Galois field circuits
- Continue with Weak Nullstellensatz over Boolean rings for
SAT and equivalence check .
- For word-level hardware verification, we need another set of
concepts: Radical Ideals and their varieties and the Strong
10/29: Completed Weak Nullstellensatz based verification of
combinational circuits over Galois fields. Also studied polynomial
functions and polynomial interpolation over Galois fields. Please
see updated slides gf.pdf and my book
- After that, we will study the very interesting, but somewhat more
involved concepts of Radical ideals and Strong Nullstellensatz:
slides for Radical Ideals
11/3 - 11/5: No classes. Work on HW and Projects. Will see you
Nov 10 and start working on Radical Ideals.
11/10: Ideals and their Radicals, the I(V(J)) and how they are all related with Hilbert's Strong Nullstellensatz. Here are the
slides for radical ideals and Nullstellensatz [Slides
11/12: Finished with I(V(J)) and
- Here is the Singular file for the miter corresponding to 2-bit
multiplier that we verified in
11/17: Apply Strong Nullstellensatz over Galois fields to circuit verification in a scalable manner. Here is a set of
[Slides updated 11/19]
11/19: Efficient implementations of polynomial division over
circuits using the F4-style reduction over matrices representing the
Groebner basis problems for circuit verification.
[Slides updated 11/19]
11/19: Projections of varieties, elimination ideals and their
application to Hierarchy Abstraction and Combinational Circuit
11/24: Here are the slides
on projections and elimination over Galois fields
11/26: Starting studying sequential circuit verification, FSM
minimization, FSM encoding and re-encoding issues, Retiming and
re-synthesis and its impact on FSM equivalence checking
on FSM equivalence problem .
12/1: Proving Equivalence of Finite State Machines using
Implicit FSM traversal. Here are the :
lecture slides for today .
12/3: We will complete FSM Verification. Slides updated on 12/3.
12/8: In the last two lectures, I will give an overview of VLSI
testing problems and their formulations. You will notice that most
of these techniques can be formulated and solved using the core
engines we have learnt: SAT, Circuit-SAT, BDDs, even Groebner
engines. Introduced the stuck-at-fault model, ATPG using Boolean
differences, Roth's D calculus and Checkpoint theorem.
12/10: I want to show you the operation of the PODEM algorithm
for Combinational ATPG, then move on to Sequential ATPG, and then
discuss delay faults and IDDQ testing. Here are some slides:
12/10 is the last lecture! [Concludes the
- Here is a Singular file ivj.sing
with examples on Radical ideals and their computation using the
radical(J) procedure given in primdec.lib
Homeworks and Programming Assignments
Here is the first HW to get you started. Due Wed, Sept 10.
HW 1 .
Solutions to HW 1 are
here. Prepared by Xiaojun. Also uploaded is the latex source and
HW 2 has been assigned, and it is due on Monday 9/29. Download it
You will also need the following design benchmarks to play with.
HW 3: Programming with Singular. Due Wed Oct 22.
HW 4 has been assigned. Download it from
Here are some solutions to HW 4
that Xiaojun has prepared. Please take a look. Also, here are some
Singular files that you can use to solve some of these problems (Q2,
interpolate and miter,
- Here are two BLIF files for the 16-bit GF multipliers:
MontgomeryF_q16.blif. You'll need these files for Q5 in the HW.
- Here is a Singular file (
miter16.singular) which is a GF miter between the Mastrovito
and Montgomery multipliers. The miter is a word-level one, as
described in the lecture slides. Take a look at the file, with the
Singular commands at the bottom of this file. Run it, and feel free
to change the term ordering to Dp from lp, and experiment.
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 describing the various
options for a class project.
- [Project description document updated
10/28] Added the last section on Project proposal
preparation and submission guidelines.
Final Project Submission Guideline
Download from here
Testing and Verification Software, Tools, Benchmarks
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
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:
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
Make sure to read 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 CUDD package, please go to Prof. Fabio Somenzi's
website at at
http://vlsi.colorado.edu/~fabio/ , and download the CUDD
this link takes you to the main documentation for CUDD.
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
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
and script.delay, for area
and delay optimization, respectively.
To map the circuits to a gate-library, try the
lib2.genlib and the
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
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
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.