diff --git a/PipeStage.py b/PipeStage.py
index 198c6f0c0529a854cd6dc5312a08f539a1e5ec2d..f8c77b60f1bacdab560cc0aba700dce91036dedf 100644
--- a/PipeStage.py
+++ b/PipeStage.py
@@ -39,7 +39,6 @@ class PipeStage(Elaboratable):
 
             pipe_reg_valid = Signal(1)
             skid_reg_valid = Signal(1)
-            egg = Signal(1)
 
             m.d.comb += self.downstream_valid_out.eq( skid_reg_valid | pipe_reg_valid)
             m.d.comb +=   self.upstream_ready_out.eq(~skid_reg_valid)
@@ -49,28 +48,25 @@ class PipeStage(Elaboratable):
             with m.Else():
                 m.d.comb += self.downstream_data_out.eq(pipe_reg)
 
-            with m.If(self.downstream_ready_in == 1):
-                m.d.sync += skid_reg_valid.eq(0)
 
             with m.If(self.upstream_ready_out == 1):
                 m.d.sync +=       pipe_reg.eq(self.upstream_data_in)
                 m.d.sync += pipe_reg_valid.eq(self.upstream_valid_in)
                 with m.If(self.downstream_ready_in == 0):
-                    m.d.comb += egg.eq(1)
                     m.d.sync +=       skid_reg.eq(pipe_reg)
                     m.d.sync += skid_reg_valid.eq(pipe_reg_valid)
 
+            with m.If(self.downstream_ready_in == 1):
+                m.d.sync += skid_reg_valid.eq(0)
 
         #with m.If((Past(self.downstream_ready_in) & (~Past(self.downstream_valid_out))) == 1):
         #    m.d.comb += Assume(self.downstream_ready_in == 1)
 
         #with m.If((Past(self.upstream_ready_out) & (~Past(self.upstream_valid_in))) == 1):
         #    m.d.comb += Assert(self.upstream_ready_out == 1)
-        capture_regular = Signal(self.width)
-        capture_skid = Signal(self.width)
 
-        capture_regular_valid = Signal(1)
-        capture_skid_valid = Signal(1)
+        number_captured = Signal(3)
+
 
         upstream_transaction = Signal(1)
         downstream_transaction = Signal(1)
@@ -78,41 +74,52 @@ class PipeStage(Elaboratable):
         m.d.comb += upstream_transaction.eq(self.upstream_ready_out & self.upstream_valid_in)
         m.d.comb += downstream_transaction.eq(self.downstream_ready_in & self.downstream_valid_out)
 
+        m.d.sync += number_captured.eq(number_captured + upstream_transaction - downstream_transaction)
+
+        with m.If(pipe_reg_valid == 0):
+            with m.If(skid_reg_valid == 0):
+                m.d.comb += Assert(number_captured == 0)
+            with m.Else():
+                m.d.comb += Assert(number_captured == 1)
+        with m.Else():
+            with m.If(skid_reg_valid == 0):
+                m.d.comb += Assert(number_captured == 1)
+            with m.Else():
+                m.d.comb += Assert(number_captured == 2)
+
+
+        m.d.comb += Assert((number_captured == 0) | (number_captured == 1) | (number_captured == 2))
+
+
+        regular_sample = Signal(self.width)
+        skid_sample    = Signal(self.width)
 
-        # Case analysis based on upstream / downstream transactions
 
         with m.If(upstream_transaction == 1):
             with m.If(downstream_transaction == 1):
                 # Upstream transaction, downstream transaction
-                with m.If(capture_skid_valid == 1):
-                    m.d.comb += Assert(self.downstream_data_out == capture_skid)
-                    m.d.sync += capture_skid_valid.eq(0)
-                with m.Else():
-                    m.d.comb += Assert(capture_regular_valid == 1)
-                    m.d.comb += Assert(self.downstream_data_out == capture_regular)
-                    m.d.sync += capture_regular.eq(self.upstream_data_in)
+                with m.If(number_captured == 2):
+                    m.d.comb += Assert(self.downstream_data_out == skid_sample)
+                with m.Elif(number_captured == 1):
+                    m.d.comb += Assert(self.downstream_data_out == regular_sample)
+                    m.d.sync += regular_sample.eq(self.upstream_data_in)
 
             with m.Else():
                 # Upstream transaction, no downstream transaction
-                with m.If(capture_regular_valid == 0):
-                    m.d.sync += capture_regular.eq(self.upstream_data_in)
-                    m.d.sync += capture_regular_valid.eq(1)
-                with m.Else():
-                    m.d.comb += Assert(capture_skid_valid == 0)
-                    m.d.sync += capture_skid.eq(capture_regular)
-                    m.d.sync += capture_regular.eq(self.upstream_data_in)
-                    m.d.sync += capture_skid_valid.eq(1)
+                with m.If(number_captured == 0):
+                    m.d.sync += regular_sample.eq(self.upstream_data_in)
+                with m.Elif(number_captured == 1):
+                    m.d.sync += skid_sample.eq(regular_sample)
+                    m.d.sync += regular_sample.eq(self.upstream_data_in)
 
         with m.Else():
             with m.If(downstream_transaction == 1):
                 # no upstream transaction, downstream transaction
-                with m.If(capture_skid_valid == 1):
-                    m.d.comb += Assert(self.downstream_data_out == capture_skid)
-                    m.d.sync += capture_skid_valid.eq(0)
-                with m.Else():
-                    m.d.comb += Assert(capture_regular_valid == 1)
-                    m.d.comb += Assert(self.downstream_data_out == capture_regular)
-                    m.d.sync += capture_regular_valid.eq(0)
+                with m.If(number_captured == 2):
+                    m.d.comb += Assert(self.downstream_data_out == skid_sample)
+                with m.Elif(number_captured == 1):
+                    m.d.comb += Assert(self.downstream_data_out == regular_sample)
+
             with m.Else():
                 # no upstream transaction, no downstream transaction
                 m.d.comb += Assert(1==1)
diff --git a/pipestage.sby b/pipestage.sby
index cf8b8f0783408000313a06fec9bf5d15386da2a1..f80990cc419287e0d95ebc5dbdae2c9bb06da559 100644
--- a/pipestage.sby
+++ b/pipestage.sby
@@ -1,9 +1,13 @@
 [options]
 mode prove
+#mode bmc
+#depth 256
+
 multiclock off
 
 [engines]
-smtbmc
+#smtbmc boolector
+abc pdr
 
 [script]
 read_ilang pipestage.il
@@ -12,7 +16,7 @@ proc
 opt
 fsm
 flatten
-show -format dot -notitle
+show -format dot -notitle -prefix /home/thz/dotty.dot
 
 
 [files]