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


Symbolic Reachability with BDDs:

Please email me your completed program and a brief description of your results (how many reachable states and how many iterations) on the ISCAS 89 benchmarks.

I have written for you a program that computes the set of reachable states of a sequential circuit. However, the program is missing the core code that computes the reachability iteration we discussed in class. Your job is to fill in the missing code to create a working program. 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.

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 try running your program on the smaller benchmarks. I've also supplied a working binary of a solution on the departmental Linux machines, so you can compare your results against mine. (Or, feel free to compare results with others in the class on Piazza!)

As with the Assignment 1, you are unlikely to get your program to work on all of the benchmarks. Do what you can. Please be considerate of other users on the machine, as BDDs can get VERY big, VERY quickly.

You will need to use the same BDD package from the BDD version of Assignment 1. In addition, you will need the program I wrote, which consists of several files. Feel free to use or modify as much of this code as you wish.

It may be faster to copy the files directly from /faculty/ajh/public_html/courses/cpsc513/assign-reach.

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. I've fixed things so at least things should compile cleanly this year.