mirror of
https://github.com/YosysHQ/sby.git
synced 2025-04-05 22:14:08 +00:00
create only a single bad when using pono solver; workaround for #137
This commit is contained in:
parent
ad07ea0e85
commit
257a57d8ed
|
@ -449,6 +449,7 @@ class SbyTask:
|
|||
print("dffunmap", file=f)
|
||||
print("stat", file=f)
|
||||
print("write_btor {}-i design_{m}.info design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f)
|
||||
print("write_btor -s {}-i design_{m}_single.info design_{m}_single.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f)
|
||||
|
||||
proc = SbyProc(
|
||||
self,
|
||||
|
|
|
@ -153,7 +153,7 @@ def run(mode, task, engine_idx, engine):
|
|||
task,
|
||||
f"engine_{engine_idx}_{common_state.produced_cex}",
|
||||
task.model("btor"),
|
||||
"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=task.workdir, idx=engine_idx, i=suffix),
|
||||
"cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}.vcd --hierarchical-symbols --info model/design_btor{s}.info model/design_btor{s}.btor engine_{idx}/trace{i}.wit".format(dir=task.workdir, idx=engine_idx, i=suffix, s='_single' if solver_args[0] == 'pono' else ''),
|
||||
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
|
||||
)
|
||||
proc2.output_callback = output_callback2
|
||||
|
@ -216,7 +216,7 @@ def run(mode, task, engine_idx, engine):
|
|||
proc = SbyProc(
|
||||
task,
|
||||
f"engine_{engine_idx}", task.model("btor"),
|
||||
f"cd {task.workdir}; {solver_cmd} model/design_btor.btor",
|
||||
f"cd {task.workdir}; {solver_cmd} model/design_btor{'_single' if solver_args[0]=='pono' else ''}.btor",
|
||||
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
|
||||
)
|
||||
|
||||
|
|
Loading…
Reference in a new issue