mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-07 22:55:18 +00:00
Code Activity

Merge pull request #136 from nakengelhardt/fix_pono

Browse source 
use --witness option when calling pono
This commit is contained in:
Miodrag Milanović 2022-01-12 13:46:25 +01:00 committed by GitHub
parent f5a41e5ab1 257a57d8ed
commit f878a0e517
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 28 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
sbysrc/sby_core.py
View file

@ -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,

6
sbysrc/sby_engine_btor.py
View file

@ -46,7 +46,7 @@ def run(mode, task, engine_idx, engine):
elif solver_args[0] == "pono":
if random_seed:
task.error("Setting the random seed is not available for the pono solver.")
solver_cmd = task.exe_paths["pono"] + f" -v 1 -e bmc -k {task.opt_depth - 1}"
solver_cmd = task.exe_paths["pono"] + f" --witness -v 1 -e bmc -k {task.opt_depth - 1}"
else:
task.error(f"Invalid solver command {solver_args[0]}.")
@ -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")
)

24
tests/multi_assert.sby Normal file
View file

@ -0,0 +1,24 @@
[tasks]
btormc
pono
[options]
mode bmc
depth 5
expect fail
[engines]
btormc: btor btormc
pono: btor pono
[script]
read_verilog -sv multi_assert.v
prep -top test
[file multi_assert.v]
module test();
always @* begin
assert (1);
assert (0);
end
endmodule