From 5382fdd6546dda2b3c0d89bb11da895e3d47dd47 Mon Sep 17 00:00:00 2001
From: Kia <kia@special-circumstanc.es>
Date: Sun, 14 Mar 2021 19:34:31 -0600
Subject: [PATCH] reordering
---
rtl_lib/pipe_stage.py | 29 ++++++++++++++++-------------
1 file changed, 16 insertions(+), 13 deletions(-)
diff --git a/rtl_lib/pipe_stage.py b/rtl_lib/pipe_stage.py
index 742a405..7a439f5 100644
--- a/rtl_lib/pipe_stage.py
+++ b/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))
--
GitLab