Scalable compositional minimization via static analysis

State-equivalence based reduction techniques, e.g. bisimulation minimization, can be used to reduce a state transition system to facilitate subsequent verification tasks. However, the complexity of computing the set of equivalent state pairs often exceeds that of performing symbolic property checking on the original system. We introduce a fully-automated efficient compositional minimization approach which requires only static analysis. Key to our approach is a heuristic algorithm that identifies components with high reduction potential in a bit-level netlist. We next inject combinational logic which restricts the component´s inputs to selected representatives of symbolically-computed equivalence classes thereof. Finally, we use existing transformations to synergistically exploit the dramatic netlist reductions enabled by these input filters. Experiments confirm that our technique is able to efficiently yield substantial reductions on large industrial netlists.