From 25a8a741bb2ba2f660bb8175551839be2898a933 Mon Sep 17 00:00:00 2001 From: Donald Sebastian Leung Date: Thu, 22 Oct 2020 13:32:12 +0800 Subject: [PATCH] Refine assertions for case with replacements in sorting network --- rtio/sed/output_network.py | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/rtio/sed/output_network.py b/rtio/sed/output_network.py index 932ef18..4308575 100644 --- a/rtio/sed/output_network.py +++ b/rtio/sed/output_network.py @@ -170,7 +170,7 @@ class OutputNetwork(Elaboratable): # 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 + # - All channel numbers in the input appear exactly once as a # valid output with m.Else(): m.d.comb += Assert(~channels_unique) @@ -180,11 +180,14 @@ class OutputNetwork(Elaboratable): 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) + input_channel_valid_once = Const(0) + for node1 in range(len(self.output)): + accum = (Past(input_node.payload.channel, clocks=network_latency) == self.output[node1].payload.channel) & self.output[node1].valid + for node2 in range(len(self.output)): + if node1 != node2: + accum = accum & ((Past(input_node.payload.channel, clocks=network_latency) != self.output[node2].payload.channel) | ~self.output[node2].valid) + input_channel_valid_once = input_channel_valid_once | accum + m.d.comb += Assert(input_channel_valid_once) def elaborate(self, platform): return self.m