From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Tue, 28 Jan 2020 21:27:58 +0000 (+0000)
Subject: read proof file from any location
X-Git-Tag: ls180-24jan2020~313
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7d13474a565d676c21542b14138503352ea5ebb9;p=ieee754fpu.git

read proof file from any location
---

diff --git a/src/ieee754/fpmax/formal/proof_fmax_mod.py b/src/ieee754/fpmax/formal/proof_fmax_mod.py
index 5471eee6..b16b5e0b 100644
--- a/src/ieee754/fpmax/formal/proof_fmax_mod.py
+++ b/src/ieee754/fpmax/formal/proof_fmax_mod.py
@@ -9,6 +9,7 @@ from ieee754.fpcommon.fpbase import FPNumDecode, FPNumBaseRecord
 from ieee754.fpmax.fpmax import FPMAXPipeMod
 from ieee754.pipeline import PipelineSpec
 import subprocess
+import os
 
 
 # This defines a module to drive the device under test and assert
@@ -86,7 +87,8 @@ def run_test(bits=32):
     il = rtlil.convert(m, ports=m.ports())
     with open("proof.il", "w") as f:
         f.write(il)
-    p = subprocess.Popen(['sby', '-f', 'proof.sby'],
+    dirs = os.path.split(__file__)[0]
+    p = subprocess.Popen(['sby', '-f', '%s/proof.sby' % dirs],
                          stdout=subprocess.PIPE,
                          stderr=subprocess.PIPE)
     if p.wait() == 0: