Improved Approximate Reachability using Auxiliary State Variables

Approximate reachability techniques trade off 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 over approximation of the reachable state set. Recently [7] this was improved upon 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 onoverlapping subsets of this augmented set of state variables yields much tighter approximations than earlier methods