From b5031fe8ab3fe4b1d6395489b6b6f4a042c1e0d9 Mon Sep 17 00:00:00 2001
From: Kia <kia@special-circumstanc.es>
Date: Tue, 9 Mar 2021 21:02:53 -0700
Subject: [PATCH] width_converter_simulator.py
---
gearbox.py | 31 +++++++++++++---
width_converter_simulator.py | 69 ++++++++++++++++++++++++++++++++++++
2 files changed, 96 insertions(+), 4 deletions(-)
create mode 100644 width_converter_simulator.py
diff --git a/gearbox.py b/gearbox.py
index 3283bc9..66d370d 100755
--- a/gearbox.py
+++ b/gearbox.py
@@ -346,16 +346,39 @@ class IdempotentGearbox(Elaboratable):
m.d.sync += self.bus.data_out.eq(self.bus.data_in)
- eggdrop = Signal(3)
+ with m.If(Past(ResetSignal()) == 0):
+ with m.If((self.bus.valid_in == 1) & (Past(self.bus.valid_in) == 1)):
+ m.d.comb += Assert(Rose(self.bus.valid_out))
+ return m
- m.d.comb += eggdrop.eq(Past(self.bus.data_in))
- with m.If(self.bus.ready_in == 1):
- m.d.sync += Assert(self.bus.data_out == eggdrop)
+# This is non-synthesizable but is intended to provide a model for non-unitary ratio gearbox
+# in order to do formal verification and model-checking against both the unitary-ratio gearbox
+# and also the arbitrary ratio gearbox.
+
+class GoldenGearboxModel(Elaboratable):
+ def __init__(self, *, in_width, out_width, sim_memory_size):
+ self.in_width = in_width
+ self.out_width = out_width
+ assert(in_width == out_width)
+
+ self.memory = Signal(sim_memory_size)
+
+ self.bus = GearboxBus(in_width=in_width, out_width=out_width)
+ def elaborate(self, platform):
+
+
+ write_ptr = Signal(range(sim_memory_size))
+ read_ptr = Signal(range(sim_memory_size))
+
+
+ m = Module()
return m
+
+
class DummyPlug(Elaboratable):
#def __init__(self):
diff --git a/width_converter_simulator.py b/width_converter_simulator.py
new file mode 100644
index 0000000..23e0d08
--- /dev/null
+++ b/width_converter_simulator.py
@@ -0,0 +1,69 @@
+import math
+
+real_width = 8
+
+fake_width = 19
+
+
+
+def first_word(fake_idx):
+ # Calculate first index
+
+ # bit index in an unrolled array
+ bit_index = fake_width*fake_idx
+ print("bit index is", bit_index)
+
+ # starting word of memory is
+
+ starting_word = math.floor(bit_index/real_width)
+
+ print("starting memory word", starting_word)
+
+ starting_bit_index = bit_index % real_width
+
+ print("starting bit index", starting_bit_index)
+
+ unwrapped_end_bit_index = (fake_width + starting_bit_index)
+
+ print("unwrapped_end_bit_index", unwrapped_end_bit_index)
+
+ number_of_words = math.floor(unwrapped_end_bit_index/real_width)
+
+ print("number_of_words", number_of_words)
+
+ end_bit_index = unwrapped_end_bit_index % real_width
+
+ print("end_bit_index", end_bit_index)
+
+ # print the fetch pattern:
+
+ # There are three kinds of fetches:
+
+ # Memory index left bit index right bit index
+ # Start word starting_bit_index max(unwrapped_end_bit_index, real_width)
+ # Middle words 0 real_width
+ # End word 0 end_bit_index
+
+
+ # We special-case the first fetch outside of the loop, since it always happens
+ # and has special-case logic used nowhere else.
+
+ # The microsequencer then iterate over the "middle words", and if there's a partial slice needed to be taken
+ # from the end word, we do that as well before returning
+
+ bits_snarfed = 0
+ words_fetched = 0
+
+ while True:
+
+
+ start_cut = starting_bit_index
+
+ print("fetching")
+ bits_snarfed +=
+
+
+for i in range(4):
+ print("fake index is", i)
+ first_word(i)
+ print("\n")
\ No newline at end of file
--
GitLab