diff --git a/PipeStage.py b/PipeStage.py
index 96f212ef6aa4c41b71c0ccd6d5aca94eca6e5f4f..fa443ef808b87810ba63f6ab9d3d94cc4f4a775c 100644
--- a/PipeStage.py
+++ b/PipeStage.py
@@ -1,4 +1,7 @@
+from enum import Enum
 from nmigen import *
+from nmigen.hdl.rec import *
+from nmigen.asserts import *
 from nmigen.cli import main
 
 
@@ -7,7 +10,7 @@ from nmigen.cli import main
 
 
 class PipeStage(Elaboratable):
-    def __init__(self, width, *, registered_ready):
+    def __init__(self, *, width, registered_ready):
         self.width = width
         self.registered_ready = registered_ready
 
@@ -23,7 +26,7 @@ class PipeStage(Elaboratable):
         m = Module()
 
         if (self.registered_ready == False):
-            m.d.comb += self.upstream_ready_out.eq(self.downstream_ready | (~self.downstream_valid))
+            m.d.comb += self.upstream_ready_out.eq(self.downstream_ready_in | (~self.downstream_valid_out))
 
             with m.If(self.upstream_ready_out == 1):
                 m.d.sync +=  self.downstream_data_out.eq(self.upstream_data_in)
@@ -60,7 +63,7 @@ class PipeStage(Elaboratable):
 
 
 
-class RegisteredPipeStage(Elaboratable): # registered
+class OldPipeStage(Elaboratable): # registered
     def __init__(self, width):
         self.width = width
 
@@ -124,36 +127,56 @@ class RegisteredPipeStage(Elaboratable): # registered
 
 
 
+class Trame(Elaboratable):
+    def __init__(self, *, width, alpha, beta):
+        self.width = width
+        self.alpha = alpha
+        self.beta  = beta
+
+        self.upstream_valid_in =    Signal(1)
+        self.upstream_ready_out =   Signal(1)
+        self.upstream_data_in =     Signal(self.width)
+
+        self.downstream_valid_out = Signal(1)
+        self.downstream_ready_in =  Signal(1)
+        self.downstream_data_out =  Signal(self.width)
+
+    def elaborate(self, platform):
+        m = Module()
+
+        m.submodules += self.alpha
+        m.submodules += self.beta
+
+        m.d.comb += self.alpha.upstream_valid_in.eq(self.upstream_valid_in)
+        m.d.comb += self.alpha.upstream_data_in.eq(self.upstream_data_in)
+        m.d.comb += self.alpha.downstream_ready_in.eq(self.downstream_ready_in)
+
+        m.d.comb += self.beta.upstream_valid_in.eq(self.upstream_valid_in)
+        m.d.comb += self.beta.upstream_data_in.eq(self.upstream_data_in)
+        m.d.comb += self.beta.downstream_ready_in.eq(self.downstream_ready_in)
+
+        m.d.sync += Assert(self.beta.upstream_ready_out == self.alpha.upstream_ready_out)
+        m.d.sync += Assert(self.beta.downstream_valid_out == self.alpha.downstream_valid_out)
+        m.d.sync += Assert(self.beta.downstream_data_out == self.alpha.downstream_data_out)
+
+        return m
+
+
+
+
 
 class DummyPlug(Elaboratable):
     def elaborate(self, platform):
         m = Module()
-        egg = RegisteredSkidBuffer(8)
-        m.submodules += egg
+        oldpipe = OldPipeStage(8)
+        newpipe = PipeStage(width = 8, registered_ready = True)
 
-        cntr = Signal(8)
-        intctr = Signal(8)
-        data_in = Signal(8)
-        m.d.sync += intctr.eq(intctr +1)
-        m.d.comb += egg.upstream_data_in.eq(data_in)
-
-        upstream_valid = Signal(1)
-        m.d.comb += egg.upstream_valid_in.eq(upstream_valid)
-        m.d.comb += upstream_valid.eq(1)
-
-        downstream_ready = Signal(1)
-        m.d.comb += egg.downstream_ready_in.eq(downstream_ready)
-        m.d.comb += downstream_ready.eq(1)
-        m.d.comb += data_in.eq(cntr)
-        with m.If((intctr == 4) | (intctr == 5) | (intctr == 6)):
-            m.d.comb += downstream_ready.eq(0)
-#        with m.If((intctr == 4) | (intctr == 5)):
-#            m.d.comb += upstream_valid.eq(0)
-#            m.d.comb += data_in.eq(0)
-
-        with m.If(egg.upstream_ready_out == 1):
-            m.d.sync += cntr.eq(cntr+1)
+        egg = Trame(width = 8, alpha=oldpipe, beta=newpipe)
+        m.submodules += egg
 
+        m.d.comb += egg.upstream_valid_in.eq(AnySeq(1))
+        m.d.comb += egg.downstream_ready_in.eq(AnySeq(1))
+        m.d.comb += egg.upstream_data_in.eq(AnySeq(8))
 
         return m
 
diff --git a/pipestage.sby b/pipestage.sby
new file mode 100644
index 0000000000000000000000000000000000000000..cf8b8f0783408000313a06fec9bf5d15386da2a1
--- /dev/null
+++ b/pipestage.sby
@@ -0,0 +1,19 @@
+[options]
+mode prove
+multiclock off
+
+[engines]
+smtbmc
+
+[script]
+read_ilang pipestage.il
+prep -top top
+proc
+opt
+fsm
+flatten
+show -format dot -notitle
+
+
+[files]
+pipestage.il
\ No newline at end of file