Department of Computer Science
CPSC 538D: Verification of Mixed Hardware-Software Systems (96W)


Project 1:

Due February 5. Please email me your completed program and a brief description of your results on the ISCAS 85 benchmarks.

OK, here it is. 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. 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"). Given that there were bugs in the benchmark suite before, there may still be bugs, and maybe your program can find them!

Please note that a direct BDD approach is unlikely to work on the larger circuits (e.g. c6288). I am only requiring you to do the direct BDD approach, but you can try more interesting approaches if you wish. In any case, please be considerate of other users on the machine, as BDDs can get VERY big, VERY quickly.

To make your task easier, I am providing a BDD package with associated memory management package, as well as skeleton code that reads ISCAS 85 files and builds up a circuit data structure in memory. Feel free to use or modify as much of this code as you wish. It took me almost exactly one hour to write a minimal solution to this project starting from the skeleton code I'm providing you. I expect it will take you longer than an hour, as you'll need to familiarize yourself with my code and the BDD package.

It may be faster to copy the files directly from /faculty1/ajh/World/courses/cpsc538d. If you want to install the memory and BDD packages yourself on a different machine, look for the file "dist.tar" in my directories /faculty1/ajh/memlib and /faculty1/ajh/bddlib.