From f0cefd43523ba7a57ff28fc8c7a19e5708d61a73 Mon Sep 17 00:00:00 2001
From: Kia <kia@special-circumstanc.es>
Date: Wed, 24 Mar 2021 13:21:11 -0600
Subject: [PATCH] BMC showed us a bug!
---
rtl_lib/gearbox.py | 102 +++++++++++++++++++++++++++++++++-----------
rtl_lib/gearbox.sby | 24 +++++++++++
2 files changed, 101 insertions(+), 25 deletions(-)
create mode 100644 rtl_lib/gearbox.sby
diff --git a/rtl_lib/gearbox.py b/rtl_lib/gearbox.py
index a450852..5af7a95 100644
--- a/rtl_lib/gearbox.py
+++ b/rtl_lib/gearbox.py
@@ -55,8 +55,8 @@ class ArbitraryGearbox(Elaboratable):
m.d.comb += upstream_transaction.eq( self.bus.upstream_ready_out & self.bus.upstream_valid_in)
m.d.comb += downstream_transaction.eq(self.bus.downstream_ready_in & self.bus.downstream_valid_out)
- m.d.comb += self.bus.upstream_ready_out.eq( shift_reg_len - valid_bit_count >= upstream_width)
- m.d.comb += self.bus.downstream_valid_out.eq(shift_reg_len >= downstream_width)
+ m.d.comb += self.bus.upstream_ready_out.eq(shift_reg_len - valid_bit_count >= upstream_width)
+ m.d.comb += self.bus.downstream_valid_out.eq( valid_bit_count >= downstream_width)
m.d.comb += self.bus.data_out.eq(shift_reg[0:downstream_width])
@@ -101,7 +101,7 @@ class IdempotentGearbox(Elaboratable):
def elaborate(self, platform):
m = Module()
- m.submodules.pipe = pipe = PipeStage(width=self.width, registered_ready=True)
+ m.submodules.pipe = pipe = PipeStage(width=self.width, registered_ready=False)
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)
@@ -135,20 +135,59 @@ class GoldenGearboxModel(Elaboratable):
write_ptr = Signal(range(self.sim_memory_size))
read_ptr = Signal(range(self.sim_memory_size))
- with m.If(self.bus.valid_in == 1):
- m.d.sync += write_ptr.eq(write_ptr + self.upstream_width)
- with m.Switch(write_ptr):
- for cand_wptr in range(0, self.sim_memory_size):
- with m.Case(cand_wptr):
+ upstream_width = self.upstream_width
+ downstream_width = self.downstream_width
+
+ # these are to make fake flow control signals
+ fake_memory = self.upstream_width + self.downstream_width
+ fake_occupied = Signal(range(self.upstream_width + self.downstream_width))
+
+ upstream_transaction = Signal(1)
+ downstream_transaction = Signal(1)
+
+ m.d.comb += upstream_transaction.eq( self.bus.upstream_ready_out & self.bus.upstream_valid_in)
+ m.d.comb += downstream_transaction.eq(self.bus.downstream_ready_in & self.bus.downstream_valid_out)
+
+ m.d.comb += self.bus.upstream_ready_out.eq(fake_memory - fake_occupied >= upstream_width)
+ m.d.comb += self.bus.downstream_valid_out.eq( fake_occupied >= downstream_width)
+
+ with m.If(upstream_transaction == 1):
+ with m.If(downstream_transaction == 1): # upstream and downstream
+ # the simultaneous transaction is hard, but updating the valid count isn't
+ m.d.sync += fake_occupied.eq(fake_occupied + upstream_width - downstream_width)
+ m.d.sync += read_ptr.eq(read_ptr + self.downstream_width)
+ m.d.sync += write_ptr.eq(write_ptr + self.upstream_width)
- m.d.sync += self.memory.eq(
+ with m.Switch(write_ptr):
+ for cand_wptr in range(0, self.sim_memory_size):
+ with m.Case(cand_wptr):
- Cat(self.memory.bit_select(0, cand_wptr),
- self.bus.data_in))
+ m.d.sync += self.memory.eq(
+
+ Cat(self.memory.bit_select(0, cand_wptr),
+ self.bus.data_in))
+
+
+ with m.Else(): # upstream, no downstream
+ m.d.sync += fake_occupied.eq(fake_occupied + upstream_width)
+ m.d.sync += write_ptr.eq(write_ptr + self.upstream_width)
+
+ with m.Switch(write_ptr):
+ for cand_wptr in range(0, self.sim_memory_size):
+ with m.Case(cand_wptr):
+
+ m.d.sync += self.memory.eq(
+
+ Cat(self.memory.bit_select(0, cand_wptr),
+ self.bus.data_in))
+
+ with m.Else():
+ with m.If(downstream_transaction == 1): # no upstream, downstream
+ m.d.sync += fake_occupied.eq(fake_occupied - downstream_width)
+ m.d.sync += read_ptr.eq(read_ptr + self.downstream_width)
+
+ m.d.comb += self.bus.data_out.eq(self.memory.bit_select(read_ptr, self.downstream_width))
- with m.If(self.bus.ready_in == 1):
- m.d.comb += self.bus.data_out.eq(self.memory.bit_select(read_ptr,self.downstream_width))
- m.d.sync += read_ptr.eq(read_ptr + self.downstream_width)
return m
@@ -163,24 +202,37 @@ class DummyPlug(Elaboratable):
def elaborate(self, platform):
m = Module()
- width = 7
+ upstream_width = 5
+ downstream_width = 9
+ sim_memory_size = 32
- m.submodules.gearbox = gearbox = ArbitraryGearbox(upstream_width=width, downstream_width=width)
- m.submodules.idempotent = idempotent = IdempotentGearbox(width=width)
+ expiration_date = int(sim_memory_size/upstream_width)-1
- m.d.comb += gearbox.bus.data_in.eq(AnySeq(width))
+ number_of_writes = Signal(range(2*expiration_date))
+ wrapped = Signal(1)
+
+ m.submodules.gearbox = gearbox = ArbitraryGearbox(upstream_width=upstream_width, downstream_width=downstream_width)
+ m.submodules.golden = golden = GoldenGearboxModel(upstream_width=upstream_width, downstream_width=downstream_width, sim_memory_size=sim_memory_size)
+
+ m.d.comb += gearbox.bus.data_in.eq(AnySeq(upstream_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 += golden.bus.data_in.eq(gearbox.bus.data_in)
+ m.d.comb += golden.bus.downstream_ready_in.eq(gearbox.bus.downstream_ready_in)
+ m.d.comb += golden.bus.upstream_valid_in.eq(gearbox.bus.upstream_valid_in)
+
+ with m.If(gearbox.bus.upstream_valid_in & gearbox.bus.upstream_ready_out == 1):
+ m.d.sync += number_of_writes.eq(number_of_writes + 1)
+ with m.If(number_of_writes > expiration_date):
+ m.d.sync += wrapped.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(wrapped == 0):
+ m.d.comb += Assert(gearbox.bus.upstream_ready_out == golden.bus.upstream_ready_out)
+ m.d.comb += Assert(gearbox.bus.downstream_valid_out == golden.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)
+ with m.If(gearbox.bus.downstream_valid_out == 1):
+ m.d.comb += Assert(gearbox.bus.data_out == golden.bus.data_out)
return m
diff --git a/rtl_lib/gearbox.sby b/rtl_lib/gearbox.sby
new file mode 100644
index 0000000..3042f9f
--- /dev/null
+++ b/rtl_lib/gearbox.sby
@@ -0,0 +1,24 @@
+[options]
+#mode prove
+mode bmc
+depth 32
+
+multiclock off
+
+[engines]
+smtbmc
+#abc pdr
+#abc bmc3
+
+[script]
+read_ilang gearbox.il
+prep -top top
+proc
+opt
+fsm
+flatten
+show -format dot -notitle -prefix ./dotty.dot
+
+
+[files]
+gearbox.il
\ No newline at end of file
--
GitLab