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


Project 2:

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

I have written for you a program that computes the set of reachable states of a sequential circuit, but it is not very good. The program will take the name of an input file containing the circuit and will print the total number of reachable states in that circuit, assuming the circuit starts with all registers zeroed. For this project, your task is to modify the program to use a better reachability iteration (as discussed in class) and (more importantly) to use a more efficient means to compute images.

To give you interesting data to work with, I'm providing a copy of the ISCAS 89 benchmarks. This is an industry-standard set of sequential benchmarks. The benchmarks have names like "s444.bench". You should run my program and your improved version on these benchmarks in order to (1) make sure your program doesn't have bugs (or that mine does!) and (2) see if your program is more efficient than my simple version.

As with the last assignment, you are unlikely to get your program to work on all of the benchmarks. Do what you can, and you should see your modified program run better than the one I'm giving you. As with the last assignment, please be considerate of other users on the machine, as BDDs can get VERY big, VERY quickly.

You will need to use the BDD and memory management packages from Project 1. In addition, you will need the program I wrote, which I'm giving to you as a tar file. (To unpack a tar file, mv the tar file into a new directory and type "tar -xvf project2.tar".) Feel free to use or modify as much of this code as you wish.

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. By the way, I recycled some code from some very old programs, so my apologies for the ugliness of the program I'm giving you.