17/3/2014
69
A+                   B+
A-                    B-
Theorem:
      the de-synchronization protocol
      preserves flow-equivalence
Proof: by induction on the length of the traces
    Induction hypothesis: same latch values at reset
    Induction step:
        same values at cycle i è same values at cycle i+1
CE-653 - De-Synchronisation Methodology