Add unbounded proof for 2 lanes

This commit is contained in:
Donald Sebastian Leung 2020-11-10 13:00:18 +08:00
parent 96e7a79502
commit 7b87d8012c
1 changed files with 4 additions and 0 deletions

View File

@ -116,6 +116,10 @@ class OutputNetworkTestCase(FHDLTestCase):
# OutputNetworkSpec(8, 2, [("data", 32), ("channel", 3)]),
# mode="bmc", depth=40)
# Unbounded proofs
# 2 lanes
self.assertFormal(
OutputNetworkSpec(2, 2, [("data", 32), ("channel", 3)]),
mode="prove", depth=latency(2))
# 4 lanes
self.assertFormal(
OutputNetworkSpec(4, 2, [("data", 32), ("channel", 3)]),