Refine assertions for case with replacements in sorting network

This commit is contained in:
Donald Sebastian Leung 2020-10-23 10:31:56 +08:00
parent 25a8a741bb
commit 01026026fa
1 changed files with 15 additions and 0 deletions

View File

@ -172,6 +172,8 @@ class OutputNetwork(Elaboratable):
# - Not all outputs are valid # - Not all outputs are valid
# - All channel numbers in the input appear exactly once as a # - All channel numbers in the input appear exactly once as a
# valid output # valid output
# - All valid outputs match an input modulo accounting
# information
with m.Else(): with m.Else():
m.d.comb += Assert(~channels_unique) m.d.comb += Assert(~channels_unique)
all_valid = Signal(reset=1) all_valid = Signal(reset=1)
@ -188,6 +190,19 @@ class OutputNetwork(Elaboratable):
accum = accum & ((Past(input_node.payload.channel, clocks=network_latency) != self.output[node2].payload.channel) | ~self.output[node2].valid) 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 input_channel_valid_once = input_channel_valid_once | accum
m.d.comb += Assert(input_channel_valid_once) m.d.comb += Assert(input_channel_valid_once)
for output_node in self.output:
with m.If(output_node.valid):
found_input = Signal()
for input_node in self.input:
match = Signal(reset=1)
with m.If(Past(input_node.seqn, clocks=network_latency) != output_node.seqn):
m.d.comb += match.eq(0)
for field, _ in 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)
def elaborate(self, platform): def elaborate(self, platform):
return self.m return self.m