From 1fc55a34a6ae304fbcc0ce368880a85229ba5bdd Mon Sep 17 00:00:00 2001
From: Kia <kia@special-circumstanc.es>
Date: Wed, 24 Mar 2021 12:40:56 -0600
Subject: [PATCH] rename and start BMC
---
rtl_lib/gearbox.py | 32 ++++++++++++++++++--------------
1 file changed, 18 insertions(+), 14 deletions(-)
diff --git a/rtl_lib/gearbox.py b/rtl_lib/gearbox.py
index 81df8a4..a450852 100644
--- a/rtl_lib/gearbox.py
+++ b/rtl_lib/gearbox.py
@@ -103,13 +103,13 @@ class IdempotentGearbox(Elaboratable):
m.submodules.pipe = pipe = PipeStage(width=self.width, registered_ready=True)
- m.d.comb += pipe.upstream_valid_in.eq(self.bus.valid_in)
- m.d.comb += pipe.downstream_ready_in.eq(self.bus.ready_in)
+ m.d.comb += pipe.upstream_valid_in.eq(self.bus.upstream_valid_in)
+ m.d.comb += pipe.downstream_ready_in.eq(self.bus.downstream_ready_in)
m.d.comb += pipe.upstream_data_in.eq(self.bus.data_in)
- m.d.comb += self.bus.valid_out.eq(pipe.downstream_valid_out)
+ m.d.comb += self.bus.downstream_valid_out.eq(pipe.downstream_valid_out)
m.d.comb += self.bus.data_out.eq(pipe.downstream_data_out)
- m.d.comb += self.bus.ready_out.eq(pipe.upstream_ready_out)
+ m.d.comb += self.bus.upstream_ready_out.eq(pipe.upstream_ready_out)
return m
@@ -163,21 +163,25 @@ class DummyPlug(Elaboratable):
def elaborate(self, platform):
m = Module()
- #m.d.comb += gearbox.bus.data_in.eq(AnySeq(3))
- #m.d.comb += gearbox.bus.ready_in.eq(AnySeq(1))
- #m.d.comb += gearbox.bus.valid_in.eq(AnySeq(1))
+ width = 7
- m.submodules.gearbox = gearbox = ArbitraryGearbox(upstream_width=4, downstream_width=2) #, sim_memory_size=16)
- counter = Signal(8)
- m.d.sync += counter.eq(counter+1)
+ m.submodules.gearbox = gearbox = ArbitraryGearbox(upstream_width=width, downstream_width=width)
+ m.submodules.idempotent = idempotent = IdempotentGearbox(width=width)
- #with m.If(counter%4 = ):
- m.d.comb += gearbox.bus.downstream_ready_in.eq(1)
+ m.d.comb += gearbox.bus.data_in.eq(AnySeq(width))
+ m.d.comb += gearbox.bus.downstream_ready_in.eq(AnySeq(1))
+ m.d.comb += gearbox.bus.upstream_valid_in.eq(AnySeq(1))
+ m.d.comb += idempotent.bus.data_in.eq(gearbox.bus.data_in)
+ m.d.comb += idempotent.bus.downstream_ready_in.eq(gearbox.bus.downstream_ready_in)
+ m.d.comb += idempotent.bus.upstream_valid_in.eq(gearbox.bus.upstream_valid_in)
- m.d.comb += gearbox.bus.upstream_valid_in.eq(1)
+ m.d.comb += Assert(gearbox.bus.upstream_ready_out == idempotent.bus.upstream_ready_out)
+ m.d.comb += Assert(gearbox.bus.downstream_valid_out == idempotent.bus.downstream_valid_out)
+
+ with m.If(gearbox.bus.downstream_valid_out == 1):
+ m.d.comb += Assert(gearbox.bus.data_out == idempotent.bus.data_out)
- m.d.comb += gearbox.bus.data_in.eq(0xe)
return m
--
GitLab