edge case ferreted out!

rtl_lib/gearbox.py

@@ -46,7 +46,7 @@ class ArbitraryGearbox(Elaboratable):
 
             shift_reg_len        = upstream_width + downstream_width
             shift_reg            = Signal(shift_reg_len)
-            valid_bit_count = Signal(range(shift_reg_len))
+            valid_bit_count = Signal(range(shift_reg_len+1))
 
 
             upstream_transaction = Signal(1)
@@ -140,7 +140,7 @@ class GoldenGearboxModel(Elaboratable):
 
             # 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))
+            fake_occupied = Signal(range(1 + self.upstream_width + self.downstream_width))
 
             upstream_transaction = Signal(1)
             downstream_transaction = Signal(1)
@@ -202,13 +202,13 @@ class DummyPlug(Elaboratable):
     def elaborate(self, platform):
         m = Module()
 
-        upstream_width   = 5
-        downstream_width = 9
-        sim_memory_size = 32
+        upstream_width   = 1
+        downstream_width = 3
+        sim_memory_size = 8
 
         expiration_date = int(sim_memory_size/upstream_width)-1
 
-        number_of_writes = Signal(range(2*expiration_date))
+        number_of_writes = Signal(range(1024))
         wrapped = Signal(1)
 
         m.submodules.gearbox = gearbox = ArbitraryGearbox(upstream_width=upstream_width, downstream_width=downstream_width)

rtl_lib/gearbox.sby

 [options]
-#mode prove
-mode bmc
-depth 32
+mode prove
+#mode bmc
+#depth 32
 
 multiclock off
 
 [engines]
-smtbmc
-#abc pdr
+#smtbmc
+abc pdr
 #abc bmc3
 
 [script]