diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 5b84132..aed3e04 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -305,7 +305,9 @@ class SbyConfig: if section == "engines": mode = "engines" - if args is not None: + if args is None: + engine_mode = None + else: section_args = args.split() if len(section_args) > 1: @@ -314,11 +316,16 @@ class SbyConfig: if section_args[0] not in ("bmc", "prove", "cover", "live"): self.error(f"sby file syntax error: Expected one of 'bmc', 'prove', 'cover', 'live' as '[engines]' argument, got '{section_args[0]}'") - if section_args[0] in self.engines: - self.error(f"Already defined engine block for mode '{section_args[0]}'") + engine_mode = section_args[0] + + if engine_mode in self.engines: + if engine_mode is None: + self.error(f"Already defined engine block") else: - self.engines[section_args[0]] = list() - engine_mode = section_args[0] + self.error(f"Already defined engine block for mode '{engine_mode}'") + else: + self.engines[engine_mode] = list() + continue if section == "setup": @@ -415,8 +422,6 @@ class SbyConfig: if mode == "engines": args = line.strip().split() - if engine_mode not in self.engines: - self.engines[engine_mode] = list() self.engines[engine_mode].append(args) continue @@ -642,7 +647,8 @@ class SbyTask(SbyConfig): print(line, file=f) def engine_list(self): - return list(enumerate(self.engines.items())) + engines = self.engines.get(None, []) + self.engines.get(self.opt_mode, []) + return list(enumerate(engines)) def check_timeout(self): if self.opt_timeout is not None: diff --git a/sbysrc/sby_mode_bmc.py b/sbysrc/sby_mode_bmc.py index 2613efa..399f267 100644 --- a/sbysrc/sby_mode_bmc.py +++ b/sbysrc/sby_mode_bmc.py @@ -24,20 +24,8 @@ def run(task): task.handle_int_option("append", 0) task.handle_str_option("aigsmt", "yices") - for engine_idx, engine_section in task.engine_list(): - if isinstance(engine_section, list): - engine = engine_section - engine_name = None - else: - assert len(engine_section[1]) > 0 - engine = engine_section[1][0] - engine_name = engine_section[0] - - if engine_name is None: - engine_name = engine_idx - - - task.log(f"""engine_{engine_name}: {" ".join(engine)}""") + for engine_idx, engine in task.engine_list(): + task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") task.makedirs(f"{task.workdir}/engine_{engine_idx}") if engine[0] == "smtbmc": diff --git a/sbysrc/sby_mode_cover.py b/sbysrc/sby_mode_cover.py index 61d0b07..02b586f 100644 --- a/sbysrc/sby_mode_cover.py +++ b/sbysrc/sby_mode_cover.py @@ -23,19 +23,8 @@ def run(task): task.handle_int_option("depth", 20) task.handle_int_option("append", 0) - for engine_idx, engine_section in task.engine_list(): - if isinstance(engine_section, list): - engine = engine_section - engine_name = None - else: - assert len(engine_section[1]) > 0 - engine = engine_section[1][0] - engine_name = engine_section[0] - - if engine_name is None: - engine_name = engine_idx - - task.log(f"""engine_{engine_name}: {" ".join(engine)}""") + for engine_idx, engine in task.engine_list(): + task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") task.makedirs(f"{task.workdir}/engine_{engine_idx}") if engine[0] == "smtbmc": diff --git a/sbysrc/sby_mode_live.py b/sbysrc/sby_mode_live.py index c624ec5..437fe8d 100644 --- a/sbysrc/sby_mode_live.py +++ b/sbysrc/sby_mode_live.py @@ -24,19 +24,8 @@ def run(task): task.status = "UNKNOWN" - for engine_idx, engine_section in task.engine_list(): - if isinstance(engine_section, list): - engine = engine_section - engine_name = None - else: - assert len(engine_section[1]) > 0 - engine = engine_section[1][0] - engine_name = engine_section[0] - - if engine_name is None: - engine_name = engine_idx - - task.log(f"""engine_{engine_name}: {" ".join(engine)}""") + for engine_idx, engine in task.engine_list(): + task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") task.makedirs(f"{task.workdir}/engine_{engine_idx}") if engine[0] == "aiger": diff --git a/sbysrc/sby_mode_prove.py b/sbysrc/sby_mode_prove.py index f3dc1b7..1118232 100644 --- a/sbysrc/sby_mode_prove.py +++ b/sbysrc/sby_mode_prove.py @@ -31,19 +31,8 @@ def run(task): task.basecase_procs = list() task.induction_procs = list() - for engine_idx, engine_section in task.engine_list(): - if isinstance(engine_section, list): - engine = engine_section - engine_name = None - else: - assert len(engine_section[1]) > 0 - engine = engine_section[1][0] - engine_name = engine_section[0] - - if engine_name is None: - engine_name = engine_idx - - task.log(f"""engine_{engine_name}: {" ".join(engine)}""") + for engine_idx, engine in task.engine_list(): + task.log(f"""engine_{engine_idx}: {" ".join(engine)}""") task.makedirs(f"{task.workdir}/engine_{engine_idx}") if engine[0] == "smtbmc": diff --git a/tests/regression/option_skip.sby b/tests/regression/option_skip.sby new file mode 100644 index 0000000..75a2bd5 --- /dev/null +++ b/tests/regression/option_skip.sby @@ -0,0 +1,33 @@ +[tasks] +smtbmc_pass: smtbmc pass +smtbmc_fail: smtbmc fail +btormc_pass: btormc pass +btormc_fail: btormc fail + +[options] +mode bmc +pass: expect pass +fail: expect fail +pass: depth 5 +fail: depth 6 + +skip 2 + +[engines] +smtbmc: smtbmc boolector +[engines bmc] +btormc: btor btormc + +[script] +read -formal top.sv +prep -top top + +[file top.sv] +module top(input clk); + reg [7:0] counter = 0; + + always @(posedge clk) begin + counter <= counter + 1; + assert (counter < 4); + end +endmodule