mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-04 05:49:57 +00:00
Code Activity

Merge pull request #297 from jix/imctk-eqy-engine

Browse source 
Add support for the imctk-eqy-engine
This commit is contained in:
Miodrag Milanović 2024-09-16 17:39:53 +02:00 committed by GitHub
parent 8bd07192ac b8a001eab2
commit d9a5845323
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 32 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
sbysrc/sby_core.py
View file

@ -851,6 +851,7 @@ class SbyTask(SbyConfig):
"avy": os.getenv("AVY", "avy"),
"btormc": os.getenv("BTORMC", "btormc"),
"pono": os.getenv("PONO", "pono"),
"imctk-eqy-engine": os.getenv("IMCTK_EQY_ENGINE", "imctk-eqy-engine"),
}
self.taskloop = taskloop or SbyTaskloop()

32
sbysrc/sby_engine_aiger.py
View file

@ -16,7 +16,7 @@
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
#
import re, os, getopt, click
import re, os, getopt, click, json
from sby_core import SbyProc
from sby_sim import sim_witness_trace
@ -32,6 +32,7 @@ def run(mode, task, engine_idx, engine):
status_2 = "UNKNOWN"
model_variant = ""
json_output = False
if solver_args[0] == "suprove":
if mode not in ["live", "prove"]:
@ -52,6 +53,14 @@ def run(mode, task, engine_idx, engine):
solver_cmd = " ".join([task.exe_paths["aigbmc"], str(task.opt_depth - 1)] + solver_args[1:])
status_2 = "PASS" # aigbmc outputs status 2 when BMC passes
elif solver_args[0] == "imctk-eqy-engine":
model_variant = "_fold"
json_output = True
if mode != "prove":
task.error("The aiger solver 'imctk-eqy-engine' is only supported in prove mode.")
args = ["--bmc-depth", str(task.opt_depth), "--jsonl-output"]
solver_cmd = " ".join([task.exe_paths["imctk-eqy-engine"], *args, *solver_args[1:]])
else:
task.error(f"Invalid solver command {solver_args[0]}.")
@ -91,6 +100,27 @@ def run(mode, task, engine_idx, engine):
nonlocal produced_cex
nonlocal end_of_cex
if json_output:
# Forward log messages, but strip the prefix containing runtime and memory stats
if not line.startswith('{'):
print(line, file=proc.logfile, flush=True)
matched = re.match(r".*(TRACE|DEBUG|INFO|WARN|ERROR) (.*)", line)
if matched:
if matched[1] == "INFO":
task.log(matched[2])
else:
task.log(f"{matched[1]} {matched[2]}")
return None
event = json.loads(line)
if "aiw" in event:
print(event["aiw"], file=aiw_file)
if "status" in event:
if event["status"] == "pass":
proc_status = "PASS"
elif event["status"] == "fail":
proc_status = "FAIL"
return None
if proc_status is not None:
if not end_of_cex and not produced_cex and line.isdigit():
produced_cex = True