Sequential Verification Across Different Levels [Devadas 1987]
Sequential Verification Across Different Levels [Devadas 1987]
m Construct a composite STG that is the exculsive-or of STG1 and STG2
m Composite STG has N1*N2 states
m "In the composite STG, if a path exists from the initial state to any final state, the machines are not equivalent." - [Hopcroft & Ullman, 1979]