- Wednesday 10am - 11am; and Thursday 3pm - 4pm.
- Office hours will be held in MEB 4120 (West-side penthouse 4th floor).

- 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 circuits;
- Hands-on learning, project-based course, CAD tool development;
- No exams!!

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

- Hardware Datapath Verification using Algebraic Geometry
- I will keep on updating the release. Current update released: Oct 29, 2014.

- 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)

- Slides on BDDs: BDD Intro
- BDD Canonization and manipulation
- Conclude BDDs .
- Here is the original BDD paper written by Prof. Randy Bryant on ROBDDs.

- 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 non-chronological backtracking.

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

- After that, we will study the very interesting, but somewhat more involved concepts of Radical ideals and Strong Nullstellensatz: slides for Radical Ideals

- Here is the Singular file for the miter corresponding to 2-bit multiplier that we verified in class: eq_verify.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

- Some slides giving an overview of VLSI testing
- Some detailed issues about Sequential Circuit Testing

- Example BLIF files: ECE6745/bcd_7seg.blif, bcd_7seg_opt.blif, bcd_7seg_bug.blif. You should 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 filed.
- This is C6288.blif, a 16X16 array multiplier.
- Both VIS and ABC read BLIF files as inputs, and both perform combinational equivalence checking.

- Here is the assignment hw3
- Here is a sample Singular script to get you started.

- Here are two BLIF files for the 16-bit GF multipliers: MastrovitoF_q16.blif, and 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.

- [Project description document updated 10/28] Added the last section on Project proposal preparation and submission guidelines.

- 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.
- Here is a blif2cnf perl script. Feel free to use it.