Department of Computer Science
CPSC 513: Introduction to Formal Verification and Analysis


Assignment 1:

Please email me your completed program (cmbcmp-bdd.c only, with any additional files you added, but not the BDD package, the object files, the benchmarks, etc.) and a brief description of your results as a plain text file (not .doc, not .pdf, etc.) 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 was an industry-standard set of combinational benchmarks, but embarrassingly, they made a mistake in their optimization, so some circuits that were supposed to be equivalent weren't, which ended up making this an even better benchmark set. :-) (I realize this benchmark set is older than most 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. You can see if your program can catch the mistakes by comparing against the old versions in the NONREDUN subdirectory (e.g. "c1908nr_old.isc").

Please note that a direct BDD approach is unlikely to work on the larger circuits (e.g. c6288, which is a multiplier). 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. In particular, you should use the limit or ulimit commands to avoid thrashing the machine you are running on.

To make your task easier, I am providing a BDD 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. (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 my code and the BDD package.

In the past, students have built CUDD on Windows (I think usually with Cygwin.) and MacOS. I do all my development on Linux, and I just "git clone"d fresh copies both on my Ubuntu machine at home and a CS-department-maintained Linux box at UBC. In both cases, I ran into this build issue, but running "autoreconf" and then "./configure", exactly as suggested, worked perfectly. However, be sure to get started on this assignment ASAP, so you have time to ask (e.g., classmates) if you have build problems. That's the sort of problem that's not intellectually interesting at all, but can be a total show-stopper.

If you're running on the CS dept Linux machines, you could also include and link to my copy of the BDD package (or copy over the cudd.h include file and libcudd.a library file). For example, you can compile and link like this:
gcc -I/isd/users/software/cudd-3.0.0/cudd cmbcmp-bdd.c -L/isd/users/software/cudd-3.0.0/cudd/.libs -lcudd -lm

If you're not running on the CS dept machines, your best choice is to go to the unofficial GitHub mirror, download, and build your own copy.

Also, if you want some small circuits in the proper input format to play with, you can get the little circuits I drew on the board during lecture circuit 1 and circuit 2. (Or, you should really make your own, or make changes to these!)