Approximate Reachability with BDDs Using Overlapping Projections

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.

• Type: Conference
• Year: 1998
• Where: DAC
• Authors: Shankar G. Govindaraju, David L. Dill, Alan J. Hu, Mark Horowitz
• Keywords: Approximate, Approximate Fsm Traversal, Approximate Reachability Techniques, Computer Architecture, DAC 1998