From: Jacob Lifshay <programmerjake@gmail.com>
Date: Thu, 2 Dec 2021 01:26:13 +0000 (-0800)
Subject: change FHDLTestCase to use get_test_path
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=69d9c2c9cfc5f2a08debd4c7bc6c429d8eb53bd4;p=nmutil.git

change FHDLTestCase to use get_test_path

Fixes the issue with FHDLTestCase sometimes using the same directory for
different test cases, causing problems for running tests in parallel.
---

diff --git a/src/nmutil/formaltest.py b/src/nmutil/formaltest.py
index 8e16623..be41bab 100644
--- a/src/nmutil/formaltest.py
+++ b/src/nmutil/formaltest.py
@@ -1,9 +1,7 @@
-import os
 import re
 import shutil
 import subprocess
 import textwrap
-import traceback
 import unittest
 import warnings
 from contextlib import contextmanager
@@ -12,6 +10,8 @@ from nmigen.hdl.ir import Fragment
 from nmigen.back import rtlil
 from nmigen._toolchain import require_tool
 
+from nmutil.get_test_path import get_test_path
+
 
 __all__ = ["FHDLTestCase"]
 
@@ -53,19 +53,14 @@ class FHDLTestCase(unittest.TestCase):
         if msg is not None:
             self.assertEqual(str(warns[0].message), msg)
 
-    def assertFormal(self, spec, mode="bmc", depth=1, solver=""):
-        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_", "")
-        )
+    def assertFormal(self, spec, mode="bmc", depth=1, solver="",
+                     base_path="formal_test_temp"):
+        path = get_test_path(self, base_path)
 
         # 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))
+        shutil.rmtree(path, ignore_errors=True)
+        path.mkdir(parents=True)
 
         if mode == "hybrid":
             # A mix of BMC and k-induction, as per personal
@@ -98,8 +93,8 @@ class FHDLTestCase(unittest.TestCase):
             script=script,
             rtlil=rtlil.convert(Fragment.get(spec, platform="formal"))
         )
-        with subprocess.Popen([require_tool("sby"), "-f", "-d", spec_name],
-                              cwd=spec_dir,
+        with subprocess.Popen([require_tool("sby"), "-d", "job"],
+                              cwd=path,
                               universal_newlines=True,
                               stdin=subprocess.PIPE,
                               stdout=subprocess.PIPE) as proc: