
Generalized reversible rules
AbstractIn 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, deadlockfreedom, and stutteringinvariant temporal properties. 
Contact 
©20022018 U.C. Regents 