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 699ed25ce26110f588af5b18e4762c9af3e375df..8c3fe9c15cc818ae95d949fc621cdeee47a57649 100644 (file)
--- 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: