Generalized reversible rules

Abstract

In FMCAD'98, I have presented a generalized notion of reversible rules for performing state reduction in automatic formal verification. In this talk, I will summarize the techniques, and discuss possible improvement that I am currently working on.

The key idea in reversible rules is that some of the transition rules in a design may be invertible, and therefore, they can be used to collapse subgraphs into abstract state. The generalized algorithm has achieved the following goals: 1) the definition of reversible rules is simplified so that it is easy to apply the reduction method in practice; 2) the definition is generalized to allow more reduction in the size of the state graph.

The reduction algorithm can be combined with symmetry reduction techniques, for verification of invariants, deadlock-freedom, and stuttering-invariant temporal properties.