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

Add assertions for case with replacements

This commit is contained in:
Donald Sebastian Leung 2020-10-22 12:53:55 +08:00
parent 04640794b9
commit 40930878a2
1 changed files with 28 additions and 26 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

54
rtio/sed/output_network.py
View File

@ -134,18 +134,21 @@ class OutputNetwork(Elaboratable):
for node in self.output: for node in self.output:
with m.If(node.replace_occured): with m.If(node.replace_occured):
m.d.comb += replacement_occurred.eq(1) 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 node1 in range(len(self.input)):
for node2 in range(node1): for node2 in range(node1):
k1 = Cat(Past(self.input[node1].payload.channel, clocks=network_latency), ~Past(self.input[node1].valid, clocks=network_latency)) k1 = Past(self.input[node1].payload.channel, clocks=network_latency)
k2 = Cat(Past(self.input[node2].payload.channel, clocks=network_latency), ~Past(self.input[node2].valid, clocks=network_latency)) k2 = Past(self.input[node2].payload.channel, clocks=network_latency)
with m.If(k1 == k2): 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: # If there are no replacements then:
# - All input data are unique # - (Input) channel numbers are unique
# - They all make it through the sorting network # - All outputs are valid
# - All inputs make it through the sorting network
with m.If(~replacement_occurred): 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: for input_node in self.input:
appeared = Signal() appeared = Signal()
for output_node in self.output: for output_node in self.output:
@ -164,25 +167,24 @@ class OutputNetwork(Elaboratable):
with m.If(match): with m.If(match):
m.d.comb += appeared.eq(1) m.d.comb += appeared.eq(1)
m.d.comb += Assert(appeared) m.d.comb += Assert(appeared)
# Otherwise, TODO # Otherwise, if there are replacements:
# - Channel numbers are not unique
with m.If(f_output_valid): # - Not all outputs are valid
nodes_unique = Signal(reset=1) # - All channel numbers in the input appear somewhere as a
for node1 in range(len(self.input)): # valid output
for node2 in range(node1): with m.Else():
k1 = Cat(Past(self.input[node1].payload.channel, clocks=network_latency), ~Past(self.input[node1].valid, clocks=network_latency)) m.d.comb += Assert(~channels_unique)
k2 = Cat(Past(self.input[node2].payload.channel, clocks=network_latency), ~Past(self.input[node2].valid, clocks=network_latency)) all_valid = Signal(reset=1)
with m.If(k1 == k2): for node in self.output:
m.d.comb += nodes_unique.eq(0) with m.If(~node.valid):
replacement_occurred = Signal() m.d.comb += all_valid.eq(0)
for output_node in self.output: m.d.comb += Assert(~all_valid)
with m.If(output_node.replace_occured): for input_node in self.input:
m.d.comb += replacement_occurred.eq(1) appeared_valid = Signal()
# If the valid bit / channel no. combinations of all input data for output_node in self.output:
# are unique then there should be no replacements with m.If((Past(input_node.payload.channel, clocks=network_latency) == output_node.payload.channel) & output_node.valid):
with m.If(nodes_unique): m.d.comb += appeared_valid.eq(1)
m.d.comb += Assert(~replacement_occurred) m.d.comb += Assert(appeared_valid)
# Otherwise, TODO
def elaborate(self, platform): def elaborate(self, platform):
return self.m return self.m