Approximate reachability techniques trade o accuracy with the capacity to deal with bigger designs. Cho et al 3 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 e ciently the approximate image during symbolic forward propagation using overlapping projections. We demonstrate the e ectiveness 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.
Shankar G. Govindaraju, David L. Dill, Alan J. Hu,