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(
            OutputNetwork(4, 2, [("data", 32), ("channel", 3)], fv_mode=True),
            mode="bmc", depth=40)
        # TODO: unbounded proof

OutputNetworkTestCase().verify()