From a6069081c72aa16cc8a7bc6628921894ed4624da Mon Sep 17 00:00:00 2001 From: Yuheng Su Date: Tue, 2 Dec 2025 17:01:29 +0800 Subject: [PATCH] Enhance BTOR engine options with nomem and syn flags for improved model handling --- sbysrc/sby_core.py | 4 ++-- sbysrc/sby_engine_btor.py | 23 +++++++++++++++++------ 2 files changed, 19 insertions(+), 8 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index af9a064..aeb9b21 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1239,8 +1239,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, diff --git a/sbysrc/sby_engine_btor.py b/sbysrc/sby_engine_btor.py index 31cd6c9..47b1ec6 100644 --- a/sbysrc/sby_engine_btor.py +++ b/sbysrc/sby_engine_btor.py @@ -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