From 037e25fb2f4e7555015206a71b872c4df9ee4383 Mon Sep 17 00:00:00 2001
From: Kia <kia@special-circumstanc.es>
Date: Mon, 29 Mar 2021 15:53:33 -0600
Subject: [PATCH] passes k-induction
---
rtl_lib/gearbox.py | 20 ++++++++++++++++----
rtl_lib/gearbox.sby | 6 +++---
2 files changed, 19 insertions(+), 7 deletions(-)
diff --git a/rtl_lib/gearbox.py b/rtl_lib/gearbox.py
index c560cd8..27f72fd 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 6319213..77c7b23 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
--
GitLab