diff --git a/rtl_lib/gearbox.py b/rtl_lib/gearbox.py
index c560cd8ef949f2953c2b0a3c9c94f0c7d5a84ad8..27f72fd191d40c75271a431dc28c05473fd0cea5 100644
--- a/rtl_lib/gearbox.py
+++ b/rtl_lib/gearbox.py
@@ -38,10 +38,10 @@ class ArbitraryGearbox(Elaboratable):
 
             self.bus = GearboxBus(upstream_width=upstream_width, downstream_width=downstream_width)
 
-            shift_reg_len        = upstream_width + downstream_width
-            self.shift_reg            = Signal(shift_reg_len)
+            self.shift_reg_len        = upstream_width + downstream_width
+            self.shift_reg            = Signal(self.shift_reg_len)
 
-            self.valid_bit_count = Signal(range(shift_reg_len+1))
+            self.valid_bit_count = Signal(range(self.shift_reg_len+1))
 
         def elaborate(self, platform):
             m = Module()
@@ -277,10 +277,19 @@ class DummyPlug(Elaboratable):
 
 
 
+        valid_slice_gearbox = Signal(8)
+        slice_golden = Signal(8)
 
+        with m.If(wrapped == 0):
+            with m.Switch(gearbox.valid_bit_count):
+                for cand_valids in range(0, gearbox.shift_reg_len+1):
+                    with m.Case(cand_valids):
+                        m.d.comb += Assert(0 == gearbox.shift_reg.bit_select(cand_valids, gearbox.shift_reg_len-cand_valids))
+                        m.d.comb += valid_slice_gearbox.eq(golden.memory.bit_select(golden.read_ptr, cand_valids))
+                        m.d.comb += slice_golden.eq(gearbox.shift_reg.bit_select(0, cand_valids))
+                        m.d.comb += Assert(valid_slice_gearbox == slice_golden)
 
 
-        with m.If(wrapped == 0):
             m.d.comb += Assert(golden.read_ptr == downstream_txn)
             m.d.comb += Assert(golden.write_ptr == upstream_txn)
             m.d.comb += Assert(gearbox.valid_bit_count == golden.fake_occupied)
@@ -288,6 +297,9 @@ class DummyPlug(Elaboratable):
 
             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.valid_bit_count == 0):
+                m.d.comb += Assert(gearbox.shift_reg == 0)
+
             #m.d.comb += Assert(gearbox.shift_reg.bit_select(0,gearbox.valid_bit_count) == 1)
             with m.If(gearbox.bus.downstream_valid_out == 1):
                 m.d.comb += Assert(gearbox.bus.data_out == golden.bus.data_out)
diff --git a/rtl_lib/gearbox.sby b/rtl_lib/gearbox.sby
index 6319213a59ebb38b95c25bcb555b78e0b5c9f390..77c7b2375368d622beb03809bf020387799c9084 100644
--- a/rtl_lib/gearbox.sby
+++ b/rtl_lib/gearbox.sby
@@ -1,7 +1,7 @@
 [options]
-#mode prove
-mode bmc
-depth 1
+mode prove
+#mode bmc
+#depth 9
 
 multiclock off