Improved Approximate Reachability Using Auxiliary State Variables

Approximate reachability techniques trade o accuracy for the capacity to deal with bigger designs. Cho et al 4 proposed partitioning the set of state bits into mutually disjoint subsets and doing symbolic forward reachability on the individual subsets to obtain an overapproximation of the reachable state set. Recently 7 this was improvedupon by dividing the set of state bits into various subsets that could possibly overlap, and doing symbolic reachability over the overlapping subsets. In this paper, we further improve on this scheme by augmenting the set of state variables with auxiliary state variables. These auxiliary state variables are added to capture some important internal conditions in the combinational logic. Approximate symbolic forward reachability on overlapping subsets of this augmented set of state variables yields much tighter approximations than earlier methods.

• Type: Conference
• Year: 1999
• Where: DAC
• Authors: Shankar G. Govindaraju, David L. Dill, Jules P. Bergmann
• Keywords: Auxiliary State Variables, Computer Architecture, DAC 1999, State Variables, Symbolic Forward Reachability