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

Hardware Verification using Symbolic Computation

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

Instructor:

  • Prof. Priyank Kalla, Office: MEB 4512, Email: lastname@ece.utah.edu
  • Office Hours: Monday after class 3-4pm, Tue 11am - 12pm, or by appointment
  • TA: Xiaojun Sun, Email: firstname.lastname@utah.edu. TA hours:

    Course Description

  • 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 specialized course!

    Textbook

  • 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:

    Grading

  • Homeworks & Programming Assignments: 50%
  • Class Project: 50%

    Attendance

  • 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/25: Introduction

  • 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 applications.
  • 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, non-chronological backtracking.
  • 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 to applications: Nullstellensatz and application to SAT [Slides updated 10/20]
  • 10/13 - 10/15: Fall Break!
  • 10/20: Nullstellensatz and Groebner Bases
  • 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 updated 10/29]
  • 10/27: Weak Nullstellensatz based verification of Galois field circuits
  • 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 chapter.
  • 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 updated 11/13]
  • 11/12: Finished with I(V(J)) and  J 
  • 11/17: Apply Strong Nullstellensatz over Galois fields to circuit verification in a scalable manner. Here is a set of slides [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 [Slides updated 11/19]
  • 11/19: Projections of varieties, elimination ideals and their application to Hierarchy Abstraction and Combinational Circuit Verification
  • 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 Some notes: 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 course!]

    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 template for algorithm pseudo-code.

  • HW 2 has been assigned, and it is due on Monday 9/29. Download it from here. 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
  • 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, 3, 4): find_primitive.sing, interpolate and miter, interpolation

    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 describing the various options for a class project.

    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 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 CUDD package, please go to Prof. Fabio Somenzi's website at at http://vlsi.colorado.edu/~fabio/ , and download the CUDD package. Also 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 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

  • Coming up....

    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.