diff --git a/rtl_lib/pipe_stage.py b/rtl_lib/pipe_stage.py
index 7a439f5696505d4a5d00eabf7d49fbef0aad9d55..6fb6821eb83f47b1d2a7ec2332b87ebe5a23187e 100644
--- a/rtl_lib/pipe_stage.py
+++ b/rtl_lib/pipe_stage.py
@@ -23,37 +23,37 @@ class PipeStage(Elaboratable):
m = Module()
# FORMAL PROPERTIES
+ if (platform == "formal"):
+ # 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)
- # 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 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)
- # # 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)
- # 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
- # DOWNSTREAM INTERFACE
+ # # 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 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)
- 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 and stalls:
- m.d.comb += Cover(self.downstream_ready_in & self.downstream_valid_out)
- m.d.comb += Cover((~self.downstream_ready_in) & self.downstream_valid_out)
+ # Cover interface transactions and stalls:
+ m.d.comb += Cover(self.downstream_ready_in & self.downstream_valid_out)
+ m.d.comb += Cover((~self.downstream_ready_in) & self.downstream_valid_out)
# IMPLEMENTATION
@@ -91,65 +91,66 @@ class PipeStage(Elaboratable):
with m.If(self.downstream_ready_in == 1):
m.d.sync += skid_reg_valid.eq(0)
+ if (platform == "formal"):
- # FORMAL SECTION
- number_captured = Signal(3)
+ # FORMAL SECTION
+ number_captured = Signal(3)
- upstream_transaction = Signal(1)
- downstream_transaction = Signal(1)
+ upstream_transaction = Signal(1)
+ downstream_transaction = Signal(1)
- 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.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)
+ 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.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():
- m.d.comb += Assert(number_captured == 2)
+ 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))
+ m.d.comb += Assert((number_captured == 0) | (number_captured == 1) | (number_captured == 2))
- regular_sample = Signal(self.width)
- skid_sample = Signal(self.width)
+ regular_sample = Signal(self.width)
+ skid_sample = Signal(self.width)
- with m.If(upstream_transaction == 1):
- with m.If(downstream_transaction == 1):
- # Upstream transaction, downstream transaction
- 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(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.If(upstream_transaction == 1):
+ with m.If(downstream_transaction == 1):
+ # Upstream transaction, downstream transaction
+ 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():
- with m.If(downstream_transaction == 1):
- # no upstream transaction, downstream transaction
- 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():
+ # Upstream transaction, no downstream transaction
+ 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():
- # no upstream transaction, no downstream transaction
- m.d.comb += Assert(1==1)
+ with m.If(downstream_transaction == 1):
+ # no upstream transaction, downstream transaction
+ 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)
@@ -159,23 +160,23 @@ class PipeStage(Elaboratable):
-class DummyPlug(Elaboratable):
- def elaborate(self, platform):
- m = Module()
- #oldpipe = OldPipeStage(8)
- newpipe = PipeStage(width = 8, registered_ready = True)
- #newpipe = oldpipe
- #fifopipe = SyncFIFO(width = 8 , depth = 3,fwft=1)
- #egg = Trame(width = 8, alpha=fifopipe, beta=newpipe)
- m.submodules += newpipe
+# class DummyPlug(Elaboratable):
+# def elaborate(self, platform):
+# m = Module()
+# #oldpipe = OldPipeStage(8)
+# newpipe = PipeStage(width = 8, registered_ready = True)
+# #newpipe = oldpipe
+# #fifopipe = SyncFIFO(width = 8 , depth = 3,fwft=1)
+# #egg = Trame(width = 8, alpha=fifopipe, beta=newpipe)
+# m.submodules += newpipe
- m.d.comb += newpipe.upstream_valid_in.eq(AnySeq(1))
- m.d.comb += newpipe.downstream_ready_in.eq(AnySeq(1))
- m.d.comb += newpipe.upstream_data_in.eq(AnySeq(8))
+# m.d.comb += newpipe.upstream_valid_in.eq(AnySeq(1))
+# m.d.comb += newpipe.downstream_ready_in.eq(AnySeq(1))
+# m.d.comb += newpipe.upstream_data_in.eq(AnySeq(8))
- return m
+# return m
-if __name__ == '__main__':
- baka =DummyPlug()
- main(baka)
\ No newline at end of file
+#if __name__ == '__main__':
+# baka =DummyPlug()
+# main(baka)
\ No newline at end of file