Add unbounded proof for output network with 4 lanes

This commit is contained in:
Donald Sebastian Leung 2020-11-09 11:47:47 +08:00
parent 25715683ab
commit 2d801d1aef
2 changed files with 15 additions and 6 deletions

View File

@ -26,7 +26,7 @@ $ python -m rtio.test.sed.output_network
- - [x] `rtio.sed.layouts`
- - [x] `rtio.sed.output_network`
- - [x] `rtio.sed.output_driver`
- [ ] Add suitable assertions for verification (BMC / unbounded proof?)
- [ ] Add suitable assertions for verification
- - [ ] `rtio.cri` (`Interface` and `CRIDecoder` only)
- - [x] `rtio.sed.output_network` - Sorting network (high priority)
- - [ ] `rtio.sed.output_driver`

View File

@ -8,9 +8,13 @@ Verification tasks for OutputNetwork
"""
class OutputNetworkSpec(Elaboratable):
def __init__(self, lane_count, seqn_width, layout_payload):
self.lane_count = lane_count
self.seqn_width = seqn_width
self.layout_payload = layout_payload
def elaborate(self, platform):
m = Module()
m.submodules.output_network = output_network = OutputNetwork(4, 2, [("data", 32), ("channel", 3)])
m.submodules.output_network = output_network = OutputNetwork(self.lane_count, self.seqn_width, self.layout_payload)
# Model arbitrary inputs for network nodes
for i in range(output_network.lane_count):
@ -130,10 +134,15 @@ class OutputNetworkSpec(Elaboratable):
class OutputNetworkTestCase(FHDLTestCase):
def verify(self):
# Bounded model check
# Bounded proofs
# 8 lanes (failing)
# self.assertFormal(
# OutputNetworkSpec(8, 2, [("data", 32), ("channel", 3)]),
# mode="bmc", depth=40)
# Unbounded proofs
# 4 lanes
self.assertFormal(
OutputNetworkSpec(),
mode="bmc", depth=40)
# TODO: unbounded proof
OutputNetworkSpec(4, 2, [("data", 32), ("channel", 3)]),
mode="prove", depth=latency(4))
OutputNetworkTestCase().verify()