Approximate reachability with BDDs using overlapping projections

Approximate reachability techniques trade off accuracy with the capacity to deal with bigger designs. Cho et al. (1996) proposed approximate FSM traversal algorithms over a partition of the set of state bits. In this paper we generalize it by allowing projections onto a collection of nondisjoint subsets of the state variables. We establish the advantage of having overlapping projections and present a new multiple constrain function for BDDs, to compute efficiently the approximate image during symbolic forward propagation using overlapping projections. We demonstrate the effectiveness of this new algorithm by applying it to several control modules from the I/O unit in the Stanford FLASH Multiprocessor. We also present our results on the larger ISCAS 89 benchmarks.