From: N. Engelhardt <nak@symbioticeda.com>
Date: Wed, 8 Apr 2020 13:25:00 +0000 (+0200)
Subject: use info file for btorsim
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1b8f3df8bda798efae80c55b65917dc97c69a5a4;p=SymbiYosys.git

use info file for btorsim
---

diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py
index af942a9..55d45ac 100644
--- a/sbysrc/sby_engine_btor.py
+++ b/sbysrc/sby_engine_btor.py
@@ -113,46 +113,60 @@ def run(mode, job, engine_idx, engine):
         else:
             task_status = "FAIL" if solver_status == "sat" else "PASS"
 
-        job.update_status(task_status)
-        job.log("engine_{}: Status returned by engine: {}".format(engine_idx, task_status))
-        job.summary.append("engine_{} ({}) returned {}".format(engine_idx, " ".join(engine), task_status))
-
-        job.terminate()
+        if mode == "cover":
+            def output_callback2(line):
+                nonlocal task_status
+                match = re.search(r"Assert failed in test", line)
+                if match:
+                    task_status = "FAIL"
+                return line
+        else:
+            def output_callback2(line):
+                return line
 
         if produced_cex == 0:
+            job.update_status(task_status)
+            job.log("engine_{}: Status returned by engine: {}".format(engine_idx, task_status))
+            job.summary.append("engine_{} ({}) returned {}".format(engine_idx, " ".join(engine), task_status))
+
+            job.terminate()
             job.log("engine_{}: Engine did not produce a counter example.".format(engine_idx))
         elif produced_cex == 1:
             task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("btor"),
-                    "cd {dir}; btorsim -c --vcd engine_{idx}/trace.vcd --hierarchical-symbols model/design_btor.btor engine_{idx}/trace.wit".format(dir=job.workdir, idx=engine_idx),
+                    "cd {dir}; btorsim -c --vcd engine_{idx}/trace.vcd --hierarchical-symbols --info model/design_btor.info model/design_btor.btor engine_{idx}/trace.wit".format(dir=job.workdir, idx=engine_idx),
                     logfile=open("{dir}/engine_{idx}/logfile2.txt".format(dir=job.workdir, idx=engine_idx), "w"))
 
-            def output_callback2(line):
-                return line
-
             def exit_callback2(line):
                 assert retcode == 0
+                job.update_status(task_status)
+                job.log("engine_{}: Status returned by engine: {}".format(engine_idx, task_status))
+                job.summary.append("engine_{} ({}) returned {}".format(engine_idx, " ".join(engine), task_status))
+
+                job.terminate()
 
                 if os.path.exists("{}/engine_{}/trace.vcd".format(job.workdir, engine_idx)):
-                    job.summary.append("counterexample trace: {}/engine_{}/trace.vcd".format(job.workdir, engine_idx))
+                    job.summary.append("{}trace: {}/engine_{}/trace.vcd".format("" if mode == "cover" else "counterexample ", job.workdir, engine_idx))
 
             task2.output_callback = output_callback2
             task2.exit_callback = exit_callback2
 
         else:
-            def output_callback2(line):
-                return line
-
             def make_exit_callback2(i):
                 def exit_callback2(line):
                     assert retcode == 0
+                    job.update_status(task_status)
+                    job.log("engine_{}: Status returned by engine: {}".format(engine_idx, task_status))
+                    job.summary.append("engine_{} ({}) returned {}".format(engine_idx, " ".join(engine), task_status))
+
+                    job.terminate()
 
                     if os.path.exists("{}/engine_{}/trace{}.vcd".format(job.workdir, engine_idx, i)):
-                        job.summary.append("counterexample trace: {}/engine_{}/trace{}.vcd".format(job.workdir, engine_idx, i))
+                        job.summary.append("{}trace: {}/engine_{}/trace{}.vcd".format("" if mode == "cover" else "counterexample ", job.workdir, engine_idx, i))
                 return exit_callback2
 
             for i in range(produced_cex):
                 task2 = SbyTask(job, "engine_{}".format(engine_idx), job.model("btor"),
-                        "cd {dir}; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols model/design_btor.btor engine_{idx}/trace{i}.wit".format(dir=job.workdir, idx=engine_idx, i=i),
+                        "cd {dir}; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols --info model/design_btor.info model/design_btor.btor engine_{idx}/trace{i}.wit".format(dir=job.workdir, idx=engine_idx, i=i),
                         logfile=open("{dir}/engine_{idx}/logfile{}.txt".format(i+2, dir=job.workdir, idx=engine_idx), "w"))
 
                 task2.output_callback = output_callback2