From 40930878a2744de672b6b57d38958961febadcb4 Mon Sep 17 00:00:00 2001
From: Donald Sebastian Leung
Date: Thu, 22 Oct 2020 12:53:55 +0800
Subject: [PATCH] Add assertions for case with replacements
---
rtio/sed/output_network.py | 54 ++++++++++++++++++++------------------
1 file changed, 28 insertions(+), 26 deletions(-)
diff --git a/rtio/sed/output_network.py b/rtio/sed/output_network.py
index 3905a78..932ef18 100644
--- a/rtio/sed/output_network.py
+++ b/rtio/sed/output_network.py
@@ -134,18 +134,21 @@ class OutputNetwork(Elaboratable):
for node in self.output:
with m.If(node.replace_occured):
m.d.comb += replacement_occurred.eq(1)
- nodes_unique = Signal(reset=1)
+ channels_unique = Signal(reset=1)
for node1 in range(len(self.input)):
for node2 in range(node1):
- k1 = Cat(Past(self.input[node1].payload.channel, clocks=network_latency), ~Past(self.input[node1].valid, clocks=network_latency))
- k2 = Cat(Past(self.input[node2].payload.channel, clocks=network_latency), ~Past(self.input[node2].valid, clocks=network_latency))
+ k1 = Past(self.input[node1].payload.channel, clocks=network_latency)
+ k2 = Past(self.input[node2].payload.channel, clocks=network_latency)
with m.If(k1 == k2):
- m.d.comb += nodes_unique.eq(0)
+ m.d.comb += channels_unique.eq(0)
# If there are no replacements then:
- # - All input data are unique
- # - They all make it through the sorting network
+ # - (Input) channel numbers are unique
+ # - All outputs are valid
+ # - All inputs make it through the sorting network
with m.If(~replacement_occurred):
- m.d.comb += Assert(nodes_unique)
+ m.d.comb += Assert(channels_unique)
+ for node in self.output:
+ m.d.comb += Assert(node.valid)
for input_node in self.input:
appeared = Signal()
for output_node in self.output:
@@ -164,25 +167,24 @@ class OutputNetwork(Elaboratable):
with m.If(match):
m.d.comb += appeared.eq(1)
m.d.comb += Assert(appeared)
- # Otherwise, TODO
-
- with m.If(f_output_valid):
- nodes_unique = Signal(reset=1)
- for node1 in range(len(self.input)):
- for node2 in range(node1):
- k1 = Cat(Past(self.input[node1].payload.channel, clocks=network_latency), ~Past(self.input[node1].valid, clocks=network_latency))
- k2 = Cat(Past(self.input[node2].payload.channel, clocks=network_latency), ~Past(self.input[node2].valid, clocks=network_latency))
- with m.If(k1 == k2):
- m.d.comb += nodes_unique.eq(0)
- replacement_occurred = Signal()
- for output_node in self.output:
- with m.If(output_node.replace_occured):
- m.d.comb += replacement_occurred.eq(1)
- # If the valid bit / channel no. combinations of all input data
- # are unique then there should be no replacements
- with m.If(nodes_unique):
- m.d.comb += Assert(~replacement_occurred)
- # Otherwise, TODO
+ # Otherwise, if there are replacements:
+ # - Channel numbers are not unique
+ # - Not all outputs are valid
+ # - All channel numbers in the input appear somewhere as a
+ # valid output
+ with m.Else():
+ m.d.comb += Assert(~channels_unique)
+ all_valid = Signal(reset=1)
+ for node in self.output:
+ with m.If(~node.valid):
+ m.d.comb += all_valid.eq(0)
+ m.d.comb += Assert(~all_valid)
+ for input_node in self.input:
+ appeared_valid = Signal()
+ for output_node in self.output:
+ with m.If((Past(input_node.payload.channel, clocks=network_latency) == output_node.payload.channel) & output_node.valid):
+ m.d.comb += appeared_valid.eq(1)
+ m.d.comb += Assert(appeared_valid)
def elaborate(self, platform):
return self.m