src/nmutil/formaltest.py

   1 import re
   2 import shutil
   3 import subprocess
   4 import textwrap
   5 import unittest
   6 from nmigen.hdl.ast import Statement
   7 from nmigen.hdl.ir import Fragment
   8 from nmigen.back import rtlil
   9 from nmutil.toolchain import require_tool
  10 from nmutil.get_test_path import get_test_path
  11
  12
  13 __all__ = ["FHDLTestCase"]
  14
  15
  16 class FHDLTestCase(unittest.TestCase):
  17     def assertRepr(self, obj, repr_str):
  18         if isinstance(obj, list):
  19             obj = Statement.cast(obj)
  20
  21         def prepare_repr(repr_str):
  22             repr_str = re.sub(r"\s+",   " ",  repr_str)
  23             repr_str = re.sub(r"\( (?=\()", "(", repr_str)
  24             repr_str = re.sub(r"\) (?=\))", ")", repr_str)
  25             return repr_str.strip()
  26         self.assertEqual(prepare_repr(repr(obj)), prepare_repr(repr_str))
  27
  28     def assertFormal(self, spec, mode="bmc", depth=1, solver="",
  29                      base_path="formal_test_temp", smtbmc_opts="--logic=ALL"):
  30         path = get_test_path(self, base_path)
  31
  32         # The sby -f switch seems not fully functional when sby is
  33         # reading from stdin.
  34         shutil.rmtree(path, ignore_errors=True)
  35         path.mkdir(parents=True)
  36
  37         if mode == "hybrid":
  38             # A mix of BMC and k-induction, as per personal
  39             # communication with Clifford Wolf.
  40             script = "setattr -unset init w:* a:nmigen.sample_reg %d"
  41             mode = "bmc"
  42         else:
  43             script = ""
  44
  45         config = textwrap.dedent("""\
  46         [options]
  47         mode {mode}
  48         depth {depth}
  49         wait on
  50
  51         [engines]
  52         smtbmc {solver} -- -- {smtbmc_opts}
  53
  54         [script]
  55         read_ilang top.il
  56         prep
  57         {script}
  58
  59         [file top.il]
  60         {rtlil}
  61         """).format(
  62             mode=mode,
  63             depth=depth,
  64             solver=solver,
  65             script=script,
  66             smtbmc_opts=smtbmc_opts,
  67             rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
  68         )
  69         with subprocess.Popen([require_tool("sby"), "-d", "job"],
  70                               cwd=path,
  71                               universal_newlines=True,
  72                               stdin=subprocess.PIPE,
  73                               stdout=subprocess.PIPE) as proc:
  74             stdout, stderr = proc.communicate(config)
  75             if proc.returncode != 0:
  76                 self.fail(f"Formal verification failed:\nIn {path}\n{stdout}")