diff --git a/rtio/test/sed/output_network.py b/rtio/test/sed/output_network.py index 88c9895..0139598 100644 --- a/rtio/test/sed/output_network.py +++ b/rtio/test/sed/output_network.py @@ -35,17 +35,48 @@ class OutputNetworkSpec(Elaboratable): for node in output_network.output: with m.If(node.replace_occured): m.d.comb += replacement_occurred.eq(1) - channels_unique = Signal(reset=1) + valid_channels_unique = Signal(reset=1) for node1 in range(len(output_network.input)): - for node2 in range(node1): - k1 = Past(output_network.input[node1].payload.channel, clocks=network_latency) - k2 = Past(output_network.input[node2].payload.channel, clocks=network_latency) - with m.If(k1 == k2): - m.d.comb += channels_unique.eq(0) + with m.If(Past(output_network.input[node1].valid, clocks=network_latency)): + for node2 in range(node1): + with m.If(Past(output_network.input[node2].valid, clocks=network_latency)): + k1 = Past(output_network.input[node1].payload.channel, clocks=network_latency) + k2 = Past(output_network.input[node2].payload.channel, clocks=network_latency) + with m.If(k1 == k2): + m.d.comb += valid_channels_unique.eq(0) + invalid_channels_unique = Signal(reset=1) + for node1 in range(len(output_network.input)): + with m.If(~Past(output_network.input[node1].valid, clocks=network_latency)): + for node2 in range(node1): + with m.If(~Past(output_network.input[node2].valid, clocks=network_latency)): + k1 = Past(output_network.input[node1].payload.channel, clocks=network_latency) + k2 = Past(output_network.input[node2].payload.channel, clocks=network_latency) + with m.If(k1 == k2): + m.d.comb += invalid_channels_unique.eq(0) # If there are no replacements then: # - Input channel numbers are unique among (in)valid nodes # - All inputs make it through the sorting network unmodified - # TODO + with m.If(~replacement_occurred): + m.d.comb += Assert(valid_channels_unique) + m.d.comb += Assert(invalid_channels_unique) + for input_node in output_network.input: + appeared = Signal() + for output_node in output_network.output: + match = Signal(reset=1) + with m.If(Past(input_node.valid, clocks=network_latency) != output_node.valid): + m.d.comb += match.eq(0) + with m.If(Past(input_node.seqn, clocks=network_latency) != output_node.seqn): + m.d.comb += match.eq(0) + with m.If(Past(input_node.replace_occured, clocks=network_latency) != output_node.replace_occured): + m.d.comb += match.eq(0) + with m.If(Past(input_node.nondata_replace_occured, clocks=network_latency) != output_node.nondata_replace_occured): + m.d.comb += match.eq(0) + for field, _ in output_network.layout_payload: + with m.If(Past(getattr(input_node.payload, field), clocks=network_latency) != getattr(output_node.payload, field)): + m.d.comb += match.eq(0) + with m.If(match): + m.d.comb += appeared.eq(1) + m.d.comb += Assert(appeared) # Otherwise, if there are replacements: # - There is a channel number collision among the valid or invalid # nodes @@ -55,7 +86,45 @@ class OutputNetworkSpec(Elaboratable): # information # - Channel numbers in invalid inputs not appearing in valid inputs # as well never appear as a valid output - # TODO + with m.Else(): + m.d.comb += Assert(~valid_channels_unique | ~invalid_channels_unique) + for input_node in output_network.input: + input_channel_valid_once = Const(0) + for node1 in range(len(output_network.output)): + accum = (Past(input_node.payload.channel, clocks=network_latency) == output_network.output[node1].payload.channel) & output_network.output[node1].valid + for node2 in range(len(output_network.output)): + if node1 != node2: + accum = accum & ((Past(input_node.payload.channel, clocks=network_latency) != output_network.output[node2].payload.channel) | ~output_network.output[node2].valid) + input_channel_valid_once = input_channel_valid_once | accum + with m.If(Past(input_node.valid, clocks=network_latency)): + m.d.comb += Assert(input_channel_valid_once) + for output_node in output_network.output: + with m.If(output_node.valid): + found_input = Signal() + for input_node in output_network.input: + match = Signal(reset=1) + with m.If(~Past(input_node.valid, clocks=network_latency)): + m.d.comb += match.eq(0) + with m.If(Past(input_node.seqn, clocks=network_latency) != output_node.seqn): + m.d.comb += match.eq(0) + for field, _ in output_network.layout_payload: + with m.If(Past(getattr(input_node.payload, field), clocks=network_latency) != getattr(output_node.payload, field)): + m.d.comb += match.eq(0) + with m.If(match): + m.d.comb += found_input.eq(1) + m.d.comb += Assert(found_input) + for node1 in output_network.input: + with m.If(~Past(node1.valid, clocks=network_latency)): + has_valid_input = Signal() + for node2 in output_network.input: + with m.If(Past(node2.valid, clocks=network_latency) & (Past(node1.payload.channel, clocks=network_latency) == Past(node2.payload.channel, clocks=network_latency))): + m.d.comb += has_valid_input.eq(1) + with m.If(~has_valid_input): + has_valid_output = Signal() + for output_node in output_network.output: + with m.If(output_node.valid & (output_node.payload.channel == Past(node1.payload.channel, clocks=network_latency))): + m.d.comb += has_valid_output.eq(1) + m.d.comb += Assert(~has_valid_output) return m