2020-10-16 12:18:09 +08:00
|
|
|
from nmigen import *
|
|
|
|
|
from nmigen.asserts import *
|
|
|
|
|
from nmigen.test.utils import *
|
|
|
|
|
from ...sed.output_network import *
|
|
|
|
|
|
|
|
|
|
"""
|
|
|
|
|
Verification tasks for OutputNetwork
|
|
|
|
|
"""
|
|
|
|
|
|
|
|
|
|
class OutputNetworkTestCase(FHDLTestCase):
|
|
|
|
|
def verify(self):
|
|
|
|
|
# Bounded model check
|
|
|
|
|
self.assertFormal(
|
2020-10-20 11:40:19 +08:00
|
|
|
OutputNetwork(4, 2, [("data", 32), ("channel", 3)], fv_mode=True),
|
2020-10-16 13:41:38 +08:00
|
|
|
mode="bmc", depth=40)
|
2020-10-16 12:18:09 +08:00
|
|
|
# TODO: unbounded proof
|
|
|
|
|
|
|
|
|
|
OutputNetworkTestCase().verify()
|
