From 7d13474a565d676c21542b14138503352ea5ebb9 Mon Sep 17 00:00:00 2001 From: Luke Kenneth Casson Leighton Date: Tue, 28 Jan 2020 21:27:58 +0000 Subject: [PATCH] read proof file from any location --- src/ieee754/fpmax/formal/proof_fmax_mod.py | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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: -- 2.30.2