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

Amend assertion; add unbounded proof for 8 lanes

This commit is contained in:
Donald Sebastian Leung 2020-11-10 17:12:49 +08:00
parent 7b87d8012c
commit d5a83a65c8
1 changed files with 9 additions and 17 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -74,22 +74,19 @@ class OutputNetworkSpec(Elaboratable):
m.d.comb += Assert(appeared) m.d.comb += Assert(appeared)
# Otherwise: # Otherwise:
# - There is a channel number collision among the valid inputs # - There is a channel number collision among the valid inputs
# - All channel numbers in valid inputs appear exactly once as a # - All channel numbers in valid inputs appear at least once as a
# valid output # valid output
# - All valid outputs correspond to a valid input modulo accounting # - All valid outputs correspond to a valid input modulo accounting
# information # information
with m.Else(): with m.Else():
m.d.comb += Assert(~valid_channels_unique) m.d.comb += Assert(~valid_channels_unique)
for input_node in output_network.input: 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)): with m.If(Past(input_node.valid, clocks=network_latency)):
m.d.comb += Assert(input_channel_valid_once) appeared = Signal()
for output_node in output_network.output:
with m.If(output_node.valid & (output_node.payload.channel == Past(input_node.payload.channel, clocks=network_latency))):
m.d.comb += appeared.eq(1)
m.d.comb += Assert(appeared)
for output_node in output_network.output: for output_node in output_network.output:
with m.If(output_node.valid): with m.If(output_node.valid):
found_input = Signal() found_input = Signal()
@ -110,19 +107,14 @@ class OutputNetworkSpec(Elaboratable):
class OutputNetworkTestCase(FHDLTestCase): class OutputNetworkTestCase(FHDLTestCase):
def verify(self): def verify(self):
# Bounded proofs
# 8 lanes (failing)
# self.assertFormal(
# OutputNetworkSpec(8, 2, [("data", 32), ("channel", 3)]),
# mode="bmc", depth=40)
# Unbounded proofs
# 2 lanes
self.assertFormal( self.assertFormal(
OutputNetworkSpec(2, 2, [("data", 32), ("channel", 3)]), OutputNetworkSpec(2, 2, [("data", 32), ("channel", 3)]),
mode="prove", depth=latency(2)) mode="prove", depth=latency(2))
# 4 lanes
self.assertFormal( self.assertFormal(
OutputNetworkSpec(4, 2, [("data", 32), ("channel", 3)]), OutputNetworkSpec(4, 2, [("data", 32), ("channel", 3)]),
mode="prove", depth=latency(4)) mode="prove", depth=latency(4))
self.assertFormal(
OutputNetworkSpec(8, 2, [("data", 32), ("channel", 3)]),
mode="prove", depth=latency(8))
OutputNetworkTestCase().verify() OutputNetworkTestCase().verify()