reordering

rtl_lib/pipe_stage.py

@@ -22,38 +22,41 @@ class PipeStage(Elaboratable):
     def elaborate(self, platform):
         m = Module()
 
-        # INTERFACE FORMAL PROPERTIES
+        # FORMAL PROPERTIES
 
+        # UPSTREAM INTERFACE
         # Stable Ready for the upstream interface cannot be guarantted if we have a register in
         # the way (otherwise we'd need a combinatorial circuit which would defeat the point).
         if(self.registered_ready == False):
             with m.If((Past(self.upstream_ready_out) & (~Past(self.upstream_valid_in))) == 1):
                 m.d.comb += Assert(self.upstream_ready_out == 1)
 
-        # Assumption of Stable Ready on downstream interface is not needed for this proof
-#        with m.If((Past(self.downstream_ready_in) & (~Past(self.downstream_valid_out))) == 1):
-#            m.d.comb += Assume(self.downstream_ready_in == 1)
+        # # Assumption of Stable data/valid on upstream interface is not needed for this proof:
+        # with m.If((~Past(self.upstream_ready_out) & (Past(self.upstream_valid_in))) == 1):
+        #     m.d.comb += Assume(Stable(self.upstream_data_in) & self.upstream_valid_in)
 
+        # Cover interface transactions and stalls:
+        m.d.comb += Cover(self.upstream_ready_out     & self.upstream_valid_in)
+        m.d.comb += Cover((~self.upstream_ready_out)  & self.upstream_valid_in)
+
+
+        # DOWNSTREAM INTERFACE
 
-        # Assumption of Stable data/valid on upstream interface is not needed for this proof:
-#        with m.If((~Past(self.upstream_ready_out) & (Past(self.upstream_valid_in))) == 1):
-#            m.d.comb += Assert(Stable(self.upstream_data_in) & self.upstream_valid_in)
+        # # Assumption of Stable Ready on downstream interface is not needed for this proof
+        # 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(ResetSignal()) == 0):
             with m.If((~Past(self.downstream_ready_in) & (Past(self.downstream_valid_out))) == 1):
                 m.d.comb += Assert(Stable(self.downstream_data_out) & self.downstream_valid_out)
 
 
-        # Cover interface transactions
-        m.d.comb += Cover(self.upstream_ready_out     & self.upstream_valid_in)
+        # Cover interface transactions and stalls:
         m.d.comb += Cover(self.downstream_ready_in    & self.downstream_valid_out)
-
-        # Cover interface stalls
-
-        m.d.comb += Cover((~self.upstream_ready_out)  & self.upstream_valid_in)
         m.d.comb += Cover((~self.downstream_ready_in) & self.downstream_valid_out)
 
 
+        # IMPLEMENTATION
 
         if (self.registered_ready == False):
             m.d.comb += self.upstream_ready_out.eq(self.downstream_ready_in | (~self.downstream_valid_out))