mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-06 14:24:08 +00:00
Code Activity

Add support for "abc pdr -d" engine

Browse source 
Signed-off-by: Claire Xenia Wolf <claire@clairexen.net>
This commit is contained in:
Claire Xenia Wolf 2023-06-07 22:21:06 +02:00
parent 8b3ba68845
commit f692eff845
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
sbysrc/sby_engine_abc.py
View file

@ -42,7 +42,7 @@ def run(mode, task, engine_idx, engine):
elif abc_command[0] == "pdr": elif abc_command[0] == "pdr":
if mode != "prove": if mode != "prove":
task.error("ABC command 'pdr' is only valid in prove mode.") task.error("ABC command 'pdr' is only valid in prove mode.")
abc_command[0] += f" -v" abc_command[0] += f" -v -I engine_{engine_idx}/invariants.pla"
else: else:
task.error(f"Invalid ABC command {abc_command[0]}.") task.error(f"Invalid ABC command {abc_command[0]}.")
@ -66,7 +66,9 @@ def run(mode, task, engine_idx, engine):
task, task,
f"engine_{engine_idx}", f"engine_{engine_idx}",
task.model("aig"), task.model("aig"),
f"""cd {task.workdir}; {task.exe_paths["abc"]} -c 'read_aiger model/design_aiger.aig; fold{" -s" if task.opt_aigfolds else ""}; strash; {" ".join(abc_command)}; write_cex -a engine_{engine_idx}/trace.aiw'""", f"""cd {task.workdir}; {task.exe_paths["abc"]} -c 'read_aiger model/design_aiger.aig; fold{
" -s" if task.opt_aigfolds or (abc_command[0].startswith("pdr ") and "-d" in abc_command[1:]) else ""
}; strash; {" ".join(abc_command)}; write_cex -a engine_{engine_idx}/trace.aiw'""",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w") logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
) )
proc.checkretcode = True proc.checkretcode = True