From: Luke Kenneth Casson Leighton <lkcl@lkcl.net>
Date: Tue, 28 Jan 2020 19:34:45 +0000 (+0000)
Subject: allow fsgnj proof to be run from any location
X-Git-Tag: ls180-24jan2020~320
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5b2c064542a0889358558162c48dcdf165e673a0;p=ieee754fpu.git

allow fsgnj proof to be run from any location
---

diff --git a/src/ieee754/fsgnj/formal/proof_fsgnj_mod.py b/src/ieee754/fsgnj/formal/proof_fsgnj_mod.py
index 699ed25c..8c3fe9c1 100644
--- a/src/ieee754/fsgnj/formal/proof_fsgnj_mod.py
+++ b/src/ieee754/fsgnj/formal/proof_fsgnj_mod.py
@@ -9,7 +9,7 @@ from ieee754.fpcommon.fpbase import FPNumDecode, FPNumBaseRecord
 from ieee754.fsgnj.fsgnj import FSGNJPipeMod
 from ieee754.pipeline import PipelineSpec
 import subprocess
-
+import os
 
 # This defines a module to drive the device under test and assert
 # properties about its outputs
@@ -89,7 +89,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: