From 50112450073abecf267e4e94889fa6042ce117a5 Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung
Date: Fri, 16 Oct 2020 13:41:38 +0800
Subject: [PATCH] Increase BMC depth for sorting network assertions
---
rtio/sed/output_network.py | 8 +++-----
rtio/test/sed/output_network.py | 2 +-
2 files changed, 4 insertions(+), 6 deletions(-)
diff --git a/rtio/sed/output_network.py b/rtio/sed/output_network.py
index 9919815..dfa3c1c 100644
--- a/rtio/sed/output_network.py
+++ b/rtio/sed/output_network.py
@@ -119,12 +119,10 @@ class OutputNetwork(Elaboratable):
f_past_valid = Signal()
m.d.sync += f_past_valid.eq(1)
- # TODO: assert outputs is a permutation of inputs
-
- # Channel numbers for outputs are sorted in increasing order
+ # Valid nodes always come first in outputs
with m.If(f_past_valid):
- # TODO: Get the below (bogus) assertion to fail
- m.d.comb += Assert(self.output[7].payload.channel == 0)
+ for i in range(lane_count - 1):
+ m.d.comb += Assert(self.output[i].valid | ~self.output[i + 1].valid) # TODO: Figure out why this is failing
def elaborate(self, platform):
return self.m
diff --git a/rtio/test/sed/output_network.py b/rtio/test/sed/output_network.py
index 180d0fd..deb2317 100644
--- a/rtio/test/sed/output_network.py
+++ b/rtio/test/sed/output_network.py
@@ -12,7 +12,7 @@ class OutputNetworkTestCase(FHDLTestCase):
# Bounded model check
self.assertFormal(
OutputNetwork(16, 2, [("data", 32), ("channel", 3)], fv_mode=True),
- mode="bmc", depth=10)
+ mode="bmc", depth=40)
# TODO: unbounded proof
OutputNetworkTestCase().verify()