oddswitch.py

import unittest
import os
import re
import shutil
import subprocess
import textwrap
import traceback
import warnings
from contextlib import contextmanager

from nmigen import *
from nmigen.back import rtlil
from nmigen.asserts import *
from nmigen.back.pysim import *
from nmigen._toolchain import require_tool

class Impl1(Elaboratable):
    def __init__(self):
        self.sel = Signal()
        self.A = Signal()
        self.B = Signal()

    def elaborate(self, platform):
        m = Module()

        with m.Switch(self.sel):
            with m.Case():
                m.d.comb += [
                    self.A.eq(1),
                    self.B.eq(1),
                ]
            with m.Case(0):
                m.d.comb += [
                    self.A.eq(1),
                    self.B.eq(0),
                ]
            with m.Case(1):
                m.d.comb += [
                    self.A.eq(0),
                    self.B.eq(0)
                ]

        return m

class Impl2(Elaboratable):
    def __init__(self):
        self.sel = Signal()
        self.A = Signal()
        self.B = Signal()

    def elaborate(self, platform):
        m = Module()

        with m.Switch(self.sel):
            with m.Case(0):
                m.d.comb += [
                    self.A.eq(1),
                    self.B.eq(0),
                ]
            with m.Case(1):
                m.d.comb += [
                    self.A.eq(0),
                    self.B.eq(0)
                ]
            with m.Case():
                m.d.comb += [
                    self.A.eq(1),
                    self.B.eq(1),
                ]

        return m

class SwitchBehaviorSpec(Elaboratable):
    def elaborate(self, platform):
        m = Module()

        m.submodules.dut1 = dut1 = Impl1()
        m.submodules.dut2 = dut2 = Impl2()

        m.d.comb += Assume(dut1.sel == dut2.sel)
        m.d.sync += [
            Assert(dut1.A == dut2.A),
            Assert(dut1.B == dut2.B),
        ]

        return m

class SwitchTestCase(unittest.TestCase):
    def assertFormal(self, spec, mode="bmc", depth=1):
        caller, *_ = traceback.extract_stack(limit=2)
        spec_root, _ = os.path.splitext(caller.filename)
        spec_dir = os.path.dirname(spec_root)
        spec_name = "{}_{}".format(
            os.path.basename(spec_root).replace("test_", "spec_"),
            caller.name.replace("test_", "")
        )

        # The sby -f switch seems not fully functional when sby is reading from stdin.
        if os.path.exists(os.path.join(spec_dir, spec_name)):
            shutil.rmtree(os.path.join(spec_dir, spec_name))

        if mode == "hybrid":
            # A mix of BMC and k-induction, as per personal communication with Clifford Wolf.
            script = "setattr -unset init w:* a:nmigen.sample_reg %d"
            mode   = "bmc"
        else:
            script = ""

        config = textwrap.dedent("""\
        [options]
        mode {mode}
        depth {depth}
        wait on
        [engines]
        smtbmc
        [script]
        read_ilang top.il
        prep
        {script}
        [file top.il]
        {rtlil}
        """).format(
            mode=mode,
            depth=depth,
            script=script,
            rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
        )
        with subprocess.Popen([require_tool("sby"), "-f", "-d", spec_name], cwd=spec_dir,
                              universal_newlines=True,
                              stdin=subprocess.PIPE, stdout=subprocess.PIPE) as proc:
            stdout, stderr = proc.communicate(config)
            if proc.returncode != 0:
                self.fail("Formal verification failed:\n" + stdout)

    def test_result(self):
        self.assertFormal(SwitchBehaviorSpec(), mode="bmc", depth=10)

if __name__ == "__main__":
    SwitchTestCase().test_result()