2IMF20 Hardware Verification - Assignment 1 CEC with SAT

Please email me your completed program (cmbcmp-sat.c only, with any additional files you added, but not the SAT solver, the object files, the benchmarks, etc.) and a brief plain text description (so as a plain text file (that is with extension .txt)) of your results on the ISCAS 85 benchmarks. Be sure to start early!

Your task is to write a combinational circuit comparison program. The program will take the names of two input files containing circuits and will print whether or not the circuits are functionally equivalent. If they are not, the program should print an input vector that distinguishes the two circuits.

To give you interesting data to work with, I'm providing a copy of the ISCAS 85 benchmarks. This is an industry-standard set of combinational benchmarks. (I realize this benchmark set is older than many of you are, but it's still used in some papers even now.) The benchmarks have names like "c1908". You are to use your program to compare the version of the circuit in the DATA subdirectory (e.g. "c1908.isc") with a logic-optimized version of the same circuit in the NONREDUN subdirectory (e.g. "c1908nr.isc"). These circuits are supposed to be the same. Note, however, that in the past there were bugs in the benchmark set -- circuits that were supposed to be the same were actually different. You can see if your program can catch these mistakes by comparing against the old versions in the NONREDUN subdirectory (e.g. "c1908nr_old.isc").

Your task is to write a combinational circuit comparison program using a SAT solver. Your program will take the names of two input files containing circuits and will print a SAT instance that is satisfiable iff the circuits are different. The SAT solution tells you what input assignment will make the circuits give different results, but it's entirely optional if you want to write a helper program to translate the SAT output back into the names of the inputs to the circuits. You'll test your program on the ISCAS 85 benchmarks.

You need a SAT solver to complete this assignment. Here are three links to popular solvers. They all should read CNF or DIMACS files:

Below, you will find a skeleton code that reads ISCAS 85 files, builds up a circuit data structure in memory, and generates most of the needed clauses in the DIMACS CNF format that the SAT solver wants. Feel free to use or modify as much of this code as you wish. (The easiest thing to do is just search for "FIX THIS!!!" in the skeleton code and make your changes there.) The assignment took me very little time; I expect it will take you longer, as you'll need to familiarize yourself with the code and the SAT solver.

Note that this assignment is a slight adaptation of the assignments proposed by Alan Hu. Here is his course webpage. Thanks Alan!