mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2026-01-18 18:28:59 +00:00
Code Activity

Enhance BTOR engine options with nomem and syn flags for improved model handling

Browse source
This commit is contained in:
Yuheng Su 2025-12-02 17:01:29 +08:00
parent 1f9ffb73c9
commit c317ed4413
2 changed files with 19 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

4
sbysrc/sby_core.py
View file

@ -1238,8 +1238,8 @@ class SbyTask(SbyConfig):
print("delete -output", file=f)
print("dffunmap", file=f)
print("stat", file=f)
print("write_btor {}-i design_{m}.info -ywmap design_btor.ywb 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 -ywmap design_btor_single.ywb design_{m}_single.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f)
print("write_btor {}-i design_{m}.info -ywmap design_{m}.ywb 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 -ywmap design_{m}_single.ywb design_{m}_single.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f)
proc = SbyProc(
self,

23
sbysrc/sby_engine_btor.py
View file

@ -23,8 +23,10 @@ from sby_sim import sim_witness_trace
def run(mode, task, engine_idx, engine):
random_seed = None
nomem_opt = False
syn_opt = False
opts, solver_args = getopt.getopt(engine[1:], "", ["seed="])
opts, solver_args = getopt.getopt(engine[1:], "", ["nomem", "syn", "seed="])
if len(solver_args) == 0:
task.error("Missing solver command.")
@ -32,9 +34,18 @@ def run(mode, task, engine_idx, engine):
for o, a in opts:
if o == "--seed":
random_seed = a
if o == "--nomem":
nomem_opt = True
elif o == "--syn":
syn_opt = True
else:
task.error("Unexpected BTOR engine options.")
model_name = "btor"
if syn_opt: model_name += "_syn"
if nomem_opt: model_name += "_nomem"
if solver_args[0] == "btormc":
if mode != "bmc":
task.error("The btormc solver is only supported in bmc mode.")
@ -203,7 +214,7 @@ def run(mode, task, engine_idx, engine):
else:
suffix = common_state.produced_cex
model = f"design_btor{'_single' if solver_args[0] == 'pono' else ''}"
model = f"design_{model_name}{'_single' if solver_args[0] == 'pono' else ''}"
yw_proc = SbyProc(
task, f"engine_{engine_idx}.trace{suffix}", [],
@ -219,8 +230,8 @@ def run(mode, task, engine_idx, engine):
proc2 = SbyProc(
task,
f"engine_{engine_idx}.trace{suffix}",
task.model("btor"),
"cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}{i2}.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, i2='' if btorsim_vcd else '_btorsim', s='_single' if solver_args[0] == 'pono' else ''),
task.model(model_name),
"cd {dir} ; btorsim -c --vcd engine_{idx}/trace{i}{i2}.vcd --hierarchical-symbols --info model/design_{m}{s}.info model/design_{m}{s}.btor engine_{idx}/trace{i}.wit".format(dir=task.workdir, idx=engine_idx, i=suffix, i2='' if btorsim_vcd else '_btorsim', m=model_name, s='_single' if solver_args[0] == 'pono' else ''),
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
)
proc2.output_callback = output_callback2
@ -310,8 +321,8 @@ 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{'_single' if solver_args[0]=='pono' else ''}.btor",
f"engine_{engine_idx}", task.model(model_name),
f"cd {task.workdir}; {solver_cmd} model/design_{model_name}{'_single' if solver_args[0] == 'pono' else ''}.btor",
logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w")
)
proc.checkretcode = True