M-Labs
/
rtio-nmigen
7
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Remove assertions involving invalid inputs

master
Donald Sebastian Leung 2020-11-10 12:53:30 +08:00
parent 2d801d1aef
commit 96e7a79502
1 changed files with 12 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

48
rtio/test/sed/output_network.py
View File

@ -35,10 +35,10 @@ class OutputNetworkSpec(Elaboratable):
m.d.comb += f_output_valid.eq(counter == network_latency)
with m.If(f_output_valid):
replacement_occurred = Signal()
valid_replacement_occurred = Signal()
for node in output_network.output:
with m.If(node.replace_occured):
m.d.comb += replacement_occurred.eq(1)
with m.If(node.valid & node.replace_occured):
m.d.comb += valid_replacement_occurred.eq(1)
valid_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)):
@ -48,21 +48,11 @@ class OutputNetworkSpec(Elaboratable):
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
with m.If(~replacement_occurred):
# Among the valid outputs, if there are no replacements then:
# - Channel numbers are unique among valid inputs
# - All valid inputs make it through the sorting network unmodified
with m.If(~valid_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:
@ -80,18 +70,16 @@ class OutputNetworkSpec(Elaboratable):
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
with m.If(Past(input_node.valid, clocks=network_latency)):
m.d.comb += Assert(appeared)
# Otherwise:
# - There is a channel number collision among the valid inputs
# - All channel numbers in valid inputs appear exactly once as a
# valid output
# - All valid outputs correspond to a valid input modulo accounting
# information
# - Channel numbers in invalid inputs not appearing in valid inputs
# as well never appear as a valid output
with m.Else():
m.d.comb += Assert(~valid_channels_unique | ~invalid_channels_unique)
m.d.comb += Assert(~valid_channels_unique)
for input_node in output_network.input:
input_channel_valid_once = Const(0)
for node1 in range(len(output_network.output)):
@ -117,18 +105,6 @@ class OutputNetworkSpec(Elaboratable):
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