From 52184e5bf0e02b879d39e5f891bd6c45810abefb Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 19 Feb 2024 21:06:26 +0100 Subject: [PATCH 1/4] Initial support for a multi-task property status database This adds initial support for an sqlite database that is shared across multiple tasks of a single SBY file and that can track the status of individual properties. The amount of information tracked in the database is currently quite minimal and depends on the engine and options used. This can be incrementally extended in the future. The ways in which the information in the database can be queries is even more limited for this initial version, consisting of a single '--status' option which lists all properties and their status. --- sbysrc/sby.py | 45 +++++ sbysrc/sby_autotune.py | 1 + sbysrc/sby_cmdline.py | 5 + sbysrc/sby_core.py | 54 +++++- sbysrc/sby_design.py | 7 + sbysrc/sby_engine_smtbmc.py | 5 + sbysrc/sby_status.py | 344 ++++++++++++++++++++++++++++++++++++ tests/make/collect_tests.py | 6 +- 8 files changed, 462 insertions(+), 5 deletions(-) create mode 100644 sbysrc/sby_status.py diff --git a/sbysrc/sby.py b/sbysrc/sby.py index 986fb9d..99dcc6c 100644 --- a/sbysrc/sby.py +++ b/sbysrc/sby.py @@ -22,6 +22,7 @@ import json, os, sys, shutil, tempfile, re from sby_cmdline import parser_func from sby_core import SbyConfig, SbyTask, SbyAbort, SbyTaskloop, process_filename, dress_message from sby_jobserver import SbyJobClient, process_jobserver_environment +from sby_status import SbyStatusDb import time, platform, click process_jobserver_environment() # needs to be called early @@ -55,6 +56,39 @@ autotune_config = args.autotune_config sequential = args.sequential jobcount = args.jobcount init_config_file = args.init_config_file +status_show = args.status +status_reset = args.status_reset + +if status_show or status_reset: + target = workdir_prefix or workdir or sbyfile + if not os.path.isdir(target) and target.endswith('.sby'): + target = target[:-4] + if not os.path.isdir(target): + print(f"ERROR: No directory found at {target!r}.", file=sys.stderr) + sys.exit(1) + + try: + with open(f"{target}/status.path", "r") as status_path_file: + status_path = f"{target}/{status_path_file.read().rstrip()}" + except FileNotFoundError: + status_path = f"{target}/status.sqlite" + + if not os.path.exists(status_path): + print(f"ERROR: No status database found at {status_path!r}.", file=sys.stderr) + sys.exit(1) + + status_db = SbyStatusDb(status_path, task=None) + + if status_show: + status_db.print_status_summary() + sys.exit(0) + + if status_reset: + status_db.reset() + + status_db.db.close() + sys.exit(0) + if sbyfile is not None: if os.path.isdir(sbyfile): @@ -356,6 +390,7 @@ def start_task(taskloop, taskname): my_opt_tmpdir = opt_tmpdir my_workdir = None + my_status_db = None if workdir is not None: my_workdir = workdir @@ -364,10 +399,12 @@ def start_task(taskloop, taskname): my_workdir = workdir_prefix else: my_workdir = workdir_prefix + "_" + taskname + my_status_db = f"../{os.path.basename(workdir_prefix)}/status.sqlite" if my_workdir is None and sbyfile is not None and not my_opt_tmpdir: my_workdir = sbyfile[:-4] if taskname is not None: + my_status_db = f"../{os.path.basename(my_workdir)}/status.sqlite" my_workdir += "_" + taskname if my_workdir is not None: @@ -399,6 +436,14 @@ def start_task(taskloop, taskname): with open(f"{my_workdir}/.gitignore", "w") as gitignore: print("*", file=gitignore) + if my_status_db is not None: + os.makedirs(f"{my_workdir}/{os.path.dirname(my_status_db)}", exist_ok=True) + if os.getenv("SBY_WORKDIR_GITIGNORE"): + with open(f"{my_workdir}/{os.path.dirname(my_status_db)}/.gitignore", "w") as gitignore: + print("*", file=gitignore) + with open(f"{my_workdir}/status.path", "w") as status_path: + print(my_status_db, file=status_path) + junit_ts_name = os.path.basename(sbyfile[:-4]) if sbyfile is not None else workdir if workdir is not None else "stdin" junit_tc_name = taskname if taskname is not None else "default" diff --git a/sbysrc/sby_autotune.py b/sbysrc/sby_autotune.py index 1d6f102..b861890 100644 --- a/sbysrc/sby_autotune.py +++ b/sbysrc/sby_autotune.py @@ -378,6 +378,7 @@ class SbyAutotune: def run(self): self.task.handle_non_engine_options() + self.task.setup_status_db(':memory:') self.config = self.task.autotune_config or SbyAutotuneConfig() if "expect" not in self.task.options: diff --git a/sbysrc/sby_cmdline.py b/sbysrc/sby_cmdline.py index a75c273..bc45b4a 100644 --- a/sbysrc/sby_cmdline.py +++ b/sbysrc/sby_cmdline.py @@ -69,6 +69,11 @@ def parser_func(): parser.add_argument("--setup", action="store_true", dest="setupmode", help="set up the working directory and exit") + parser.add_argument("--status", action="store_true", dest="status", + help="summarize the contents of the status database") + parser.add_argument("--statusreset", action="store_true", dest="status_reset", + help="reset the contents of the status database") + parser.add_argument("--init-config-file", dest="init_config_file", help="create a default .sby config file") parser.add_argument("sbyfile", metavar=".sby | ", nargs="?", diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index d59ffa1..ecbd081 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -27,6 +27,7 @@ from shutil import copyfile, copytree, rmtree from select import select from time import monotonic, localtime, sleep, strftime from sby_design import SbyProperty, SbyModule, design_hierarchy +from sby_status import SbyStatusDb all_procs_running = [] @@ -674,20 +675,41 @@ class SbySummary: self.engine_summaries[engine_idx] = SbyEngineSummary(engine_idx) return self.engine_summaries[engine_idx] - def add_event(self, *args, **kwargs): + def add_event(self, *args, update_status=True, **kwargs): event = SbySummaryEvent(*args, **kwargs) + + engine = self.engine_summary(event.engine_idx) + + if update_status: + status_metadata = dict(source="summary_event", engine=engine.engine) + if event.prop: if event.type == "$assert": event.prop.status = "FAIL" if event.path: event.prop.tracefiles.append(event.path) + if update_status: + self.task.status_db.add_task_property_data( + event.prop, + "trace", + data=dict(path=event.path, step=event.step, **status_metadata), + ) if event.prop: if event.type == "$cover": event.prop.status = "PASS" if event.path: event.prop.tracefiles.append(event.path) - - engine = self.engine_summary(event.engine_idx) + if update_status: + self.task.status_db.add_task_property_data( + event.prop, + "trace", + data=dict(path=event.path, step=event.step, **status_metadata), + ) + if event.prop and update_status: + self.task.status_db.set_task_property_status( + event.prop, + data=status_metadata + ) if event.trace not in engine.traces: engine.traces[event.trace] = SbyTraceSummary(event.trace, path=event.path, engine_case=event.engine_case) @@ -1041,6 +1063,10 @@ class SbyTask(SbyConfig): if self.design == None: with open(f"{self.workdir}/model/design.json") as f: self.design = design_hierarchy(f) + self.status_db.create_task_properties([ + prop for prop in self.design.properties_by_path.values() + if not prop.type.assume_like + ]) def instance_hierarchy_error_callback(retcode): self.precise_prop_status = False @@ -1186,8 +1212,13 @@ class SbyTask(SbyConfig): self.status = "ERROR" self.terminate() + def pass_unknown_asserts(self, data): + for prop in self.design.pass_unknown_asserts(): + self.status_db.set_task_property_status(prop, data=data) + def update_status(self, new_status): assert new_status in ["PASS", "FAIL", "UNKNOWN", "ERROR"] + self.status_db.set_task_status(new_status) if new_status == "UNKNOWN": return @@ -1199,7 +1230,7 @@ class SbyTask(SbyConfig): assert self.status != "FAIL" self.status = "PASS" if self.opt_mode in ("bmc", "prove") and self.design: - self.design.pass_unknown_asserts() + self.pass_unknown_asserts(dict(source="task_status")) elif new_status == "FAIL": assert self.status != "PASS" @@ -1258,6 +1289,19 @@ class SbyTask(SbyConfig): self.handle_bool_option("assume_early", True) + def setup_status_db(self, status_path=None): + if hasattr(self, 'status_db'): + return + + if status_path is None: + try: + with open(f"{self.workdir}/status.path", "r") as status_path_file: + status_path = f"{self.workdir}/{status_path_file.read().rstrip()}" + except FileNotFoundError: + status_path = f"{self.workdir}/status.sqlite" + + self.status_db = SbyStatusDb(status_path, self) + def setup_procs(self, setupmode): self.handle_non_engine_options() if self.opt_smtc is not None: @@ -1285,6 +1329,8 @@ class SbyTask(SbyConfig): self.retcode = 0 return + self.setup_status_db() + if self.opt_make_model is not None: for name in self.opt_make_model.split(","): self.model(name.strip()) diff --git a/sbysrc/sby_design.py b/sbysrc/sby_design.py index df2977f..d93d17d 100644 --- a/sbysrc/sby_design.py +++ b/sbysrc/sby_design.py @@ -88,6 +88,10 @@ class SbyProperty: return c.FAIR raise ValueError("Unknown property type: " + name) + @property + def assume_like(self): + return self in [self.ASSUME, self.FAIR] + name: str path: Tuple[str, ...] type: Type @@ -171,9 +175,12 @@ class SbyDesign: properties_by_path: dict = field(default_factory=dict) def pass_unknown_asserts(self): + updated = [] for prop in self.hierarchy: if prop.type == prop.Type.ASSERT and prop.status == "UNKNOWN": prop.status = "PASS" + updated.append(prop) + return updated def cell_path(cell): diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 7e15589..3b43113 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -233,6 +233,7 @@ def run(mode, task, engine_idx, engine): cell_name = match[3] or match[2] prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans) prop.status = "FAIL" + task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}")) last_prop.append(prop) return line @@ -241,6 +242,7 @@ def run(mode, task, engine_idx, engine): cell_name = match[2] or match[1] prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans) prop.status = "PASS" + task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}")) last_prop.append(prop) return line @@ -271,6 +273,7 @@ def run(mode, task, engine_idx, engine): cell_name = match[2] prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans) prop.status = "FAIL" + task.status_db.set_task_property_status(prop, data=dict(source="smtbmc", engine=f"engine_{engine_idx}")) return line @@ -288,6 +291,8 @@ def run(mode, task, engine_idx, engine): def last_exit_callback(): if mode == "bmc" or mode == "cover": task.update_status(proc_status) + if proc_status == "FAIL" and mode == "bmc" and keep_going: + task.pass_unknown_asserts(dict(source="smtbmc", keep_going=True, engine=f"engine_{engine_idx}")) proc_status_lower = proc_status.lower() if proc_status == "PASS" else proc_status task.summary.set_engine_status(engine_idx, proc_status_lower) diff --git a/sbysrc/sby_status.py b/sbysrc/sby_status.py new file mode 100644 index 0000000..e4722c3 --- /dev/null +++ b/sbysrc/sby_status.py @@ -0,0 +1,344 @@ +from __future__ import annotations + +import sqlite3 +import os +import time +import json +from collections import defaultdict +from functools import wraps +from pathlib import Path +from typing import Any, Callable, TypeVar, Optional, Iterable +from sby_design import SbyProperty, pretty_path + + +Fn = TypeVar("Fn", bound=Callable[..., Any]) + + +def transaction(method: Fn) -> Fn: + @wraps(method) + def wrapper(self: SbyStatusDb, *args: Any, **kwargs: Any) -> Any: + if self._transaction_active: + return method(self, *args, **kwargs) + + try: + self.log_debug(f"begin {method.__name__!r} transaction") + self.db.execute("begin") + self._transaction_active = True + result = method(self, *args, **kwargs) + self.db.execute("commit") + self._transaction_active = False + self.log_debug(f"comitted {method.__name__!r} transaction") + return result + except sqlite3.OperationalError as err: + self.log_debug(f"failed {method.__name__!r} transaction {err}") + self.db.rollback() + self._transaction_active = False + except Exception as err: + self.log_debug(f"failed {method.__name__!r} transaction {err}") + self.db.rollback() + self._transaction_active = False + raise + try: + self.log_debug( + f"retrying {method.__name__!r} transaction once in immediate mode" + ) + self.db.execute("begin immediate") + self._transaction_active = True + result = method(self, *args, **kwargs) + self.db.execute("commit") + self._transaction_active = False + self.log_debug(f"comitted {method.__name__!r} transaction") + return result + except Exception as err: + self.log_debug(f"failed {method.__name__!r} transaction {err}") + self.db.rollback() + self._transaction_active = False + raise + + return wrapper # type: ignore + + +class SbyStatusDb: + def __init__(self, path: Path, task, timeout: float = 5.0): + self.debug = False + self.task = task + self._transaction_active = False + + setup = not os.path.exists(path) + + self.db = sqlite3.connect(path, isolation_level=None, timeout=timeout) + self.db.row_factory = sqlite3.Row + self.db.execute("PRAGMA journal_mode=WAL") + self.db.execute("PRAGMA synchronous=0") + + if setup: + self._setup() + + if task is not None: + self.task_id = self.create_task(workdir=task.workdir, mode=task.opt_mode) + + def log_debug(self, *args): + if self.debug: + if self.task: + self.task.log(" ".join(str(arg) for arg in args)) + else: + print(*args) + + @transaction + def _setup(self): + script = """ + CREATE TABLE task ( + id INTEGER PRIMARY KEY, + workdir TEXT, + mode TEXT, + created REAL + ); + CREATE TABLE task_status ( + id INTEGER PRIMARY KEY, + task INTEGER, + status TEXT, + data TEXT, + created REAL, + FOREIGN KEY(task) REFERENCES task(id) + ); + CREATE TABLE task_property ( + id INTEGER PRIMARY KEY, + task INTEGER, + src TEXT, + name TEXT, + created REAL, + FOREIGN KEY(task) REFERENCES task(id) + ); + CREATE TABLE task_property_status ( + id INTEGER PRIMARY KEY, + task_property INTEGER, + status TEXT, + data TEXT, + created REAL, + FOREIGN KEY(task_property) REFERENCES task_property(id) + ); + CREATE TABLE task_property_data ( + id INTEGER PRIMARY KEY, + task_property INTEGER, + kind TEXT, + data TEXT, + created REAL, + FOREIGN KEY(task_property) REFERENCES task_property(id) + ); + """ + for statement in script.split(";\n"): + statement = statement.strip() + if statement: + self.db.execute(statement) + + @transaction + def create_task(self, workdir: str, mode: str) -> int: + return self.db.execute( + """ + INSERT INTO task (workdir, mode, created) + VALUES (:workdir, :mode, :now) + """, + dict(workdir=workdir, mode=mode, now=time.time()), + ).lastrowid + + @transaction + def create_task_properties( + self, properties: Iterable[SbyProperty], *, task_id: Optional[int] = None + ): + if task_id is None: + task_id = self.task_id + now = time.time() + self.db.executemany( + """ + INSERT INTO task_property (name, src, task, created) + VALUES (:name, :src, :task, :now) + """, + [ + dict( + name=json.dumps(prop.path), + src=prop.location or "", + task=task_id, + now=now, + ) + for prop in properties + ], + ) + + @transaction + def set_task_status( + self, + status: Optional[str] = None, + data: Any = None, + ): + if status is None: + status = property.status + + now = time.time() + self.db.execute( + """ + INSERT INTO task_status ( + task, status, data, created + ) + VALUES ( + :task, :status, :data, :now + ) + """, + dict( + task=self.task_id, + status=status, + data=json.dumps(data), + now=now, + ), + ) + + @transaction + def set_task_property_status( + self, + property: SbyProperty, + status: Optional[str] = None, + data: Any = None, + ): + if status is None: + status = property.status + + now = time.time() + self.db.execute( + """ + INSERT INTO task_property_status ( + task_property, status, data, created + ) + VALUES ( + (SELECT id FROM task_property WHERE task = :task AND name = :name), + :status, :data, :now + ) + """, + dict( + task=self.task_id, + name=json.dumps(property.path), + status=status, + data=json.dumps(data), + now=now, + ), + ) + + @transaction + def add_task_property_data(self, property: SbyProperty, kind: str, data: Any): + now = time.time() + self.db.execute( + """ + INSERT INTO task_property_data ( + task_property, kind, data, created + ) + VALUES ( + (SELECT id FROM task_property WHERE task = :task AND name = :name), + :kind, :data, :now + ) + """, + dict( + task=self.task_id, + name=json.dumps(property.path), + kind=kind, + data=json.dumps(data), + now=now, + ), + ) + + @transaction + def all_tasks(self): + rows = self.db.execute( + """ + SELECT id, workdir, created FROM task + """ + ).fetchall() + + return {row["id"]: dict(row) for row in rows} + + @transaction + def all_task_properties(self): + rows = self.db.execute( + """ + SELECT id, task, src, name, created FROM task_property + """ + ).fetchall() + + def get_result(row): + row = dict(row) + row["name"] = tuple(json.loads(row.get("name", "[]"))) + row["data"] = json.loads(row.get("data", "null")) + return row + + return {row["id"]: get_result(row) for row in rows} + + @transaction + def all_task_property_statuses(self): + rows = self.db.execute( + """ + SELECT id, task_property, status, data, created + FROM task_property_status + """ + ).fetchall() + + def get_result(row): + row = dict(row) + row["data"] = json.loads(row.get("data", "null")) + return row + + return {row["id"]: get_result(row) for row in rows} + + @transaction + def all_status_data(self): + return ( + self.all_tasks(), + self.all_task_properties(), + self.all_task_property_statuses(), + ) + + @transaction + def reset(self): + self.db.execute("""DELETE FROM task_property_status""") + self.db.execute("""DELETE FROM task_property_data""") + self.db.execute("""DELETE FROM task_property""") + self.db.execute("""DELETE FROM task_status""") + self.db.execute("""DELETE FROM task""") + + def print_status_summary(self): + tasks, task_properties, task_property_statuses = self.all_status_data() + properties = defaultdict(set) + + uniquify_paths = defaultdict(dict) + + def add_status(task_property, status): + + display_name = task_property["name"] + if display_name[-1].startswith("$"): + counters = uniquify_paths[task_property["src"]] + counter = counters.setdefault(display_name[-1], len(counters) + 1) + if task_property["src"]: + if counter < 2: + path_based = f"" + else: + path_based = f"" + else: + path_based = f"" + display_name = (*display_name[:-1], path_based) + + properties[display_name].add(status) + + for task_property in task_properties.values(): + add_status(task_property, "UNKNOWN") + + for status in task_property_statuses.values(): + task_property = task_properties[status["task_property"]] + add_status(task_property, status["status"]) + + for display_name, statuses in sorted(properties.items()): + print(pretty_path(display_name), combine_statuses(statuses)) + + +def combine_statuses(statuses): + statuses = set(statuses) + + if len(statuses) > 1: + statuses.discard("UNKNOWN") + + return ",".join(sorted(statuses)) diff --git a/tests/make/collect_tests.py b/tests/make/collect_tests.py index 2aeccee..636ecb6 100644 --- a/tests/make/collect_tests.py +++ b/tests/make/collect_tests.py @@ -9,7 +9,11 @@ SAFE_PATH = re.compile(r"^[a-zA-Z0-9_./\\]*$") def collect(path): # don't pick up any paths that need escaping nor any sby workdirs - if not SAFE_PATH.match(str(path)) or (path / "config.sby").exists(): + if ( + not SAFE_PATH.match(str(path)) + or (path / "config.sby").exists() + or (path / "status.sqlite").exists() + ): return checked_dirs.append(path) From 6ba762db4cc37247c05513fb41e02da733ec3240 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 7 Feb 2024 18:43:23 +0100 Subject: [PATCH 2/4] Support for "abc --keep-going pdr" via new "pdr -X" mode --- sbysrc/sby_core.py | 2 +- sbysrc/sby_engine_abc.py | 150 +++++++++++++++++++++-- sbysrc/sby_engine_aiger.py | 139 +++++++++++++-------- tests/keepgoing/check_output.py | 2 +- tests/keepgoing/keepgoing_multi_step.py | 39 ++++-- tests/keepgoing/keepgoing_multi_step.sby | 4 +- tests/keepgoing/keepgoing_multi_step.sv | 1 + 7 files changed, 258 insertions(+), 79 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index ecbd081..609be95 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -787,8 +787,8 @@ class SbySummary: event = same_events[0] steps = sorted(e.step for e in same_events) if short and len(steps) > step_limit: - steps = [str(step) for step in steps[:step_limit]] excess = len(steps) - step_limit + steps = [str(step) for step in steps[:step_limit]] omitted_excess = True steps[-1] += f" and {excess} further step{'s' if excess != 1 else ''}" diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 639a7ff..7992377 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -17,32 +17,101 @@ # import re, getopt +import json from sby_core import SbyProc -from sby_engine_aiger import aigsmt_exit_callback +from sby_engine_aiger import aigsmt_exit_callback, aigsmt_trace_callback + + +def abc_getopt(args, long): + long = set(long) + output = [] + parsed = [] + toggles = set() + pos = 0 + + while pos < len(args): + arg = args[pos] + pos += 1 + if not arg.startswith('-'): + output.append(arg) + elif arg == '--': + output.extend(args[pos:]) + break + elif arg.startswith('--'): + if '=' in arg: + prefix, param = arg.split('=', 1) + if prefix + "=" in long: + parsed.append(prefix, param) + elif arg[2:] in long: + parsed.append((arg, '')) + elif arg[2:] + "=" in long: + parsed.append((arg, args[pos])) + pos += 1 + else: + output.append(arg) + elif arg.startswith('-'): + output.append(arg) + for c in arg[1:]: + if 'A' <= c <= 'Z': + if pos < len(args): + output.append(args[pos]) + pos += 1 + else: + toggles.symmetric_difference_update([c]) + + return output, parsed, toggles + def run(mode, task, engine_idx, engine): - abc_opts, abc_command = getopt.getopt(engine[1:], "", []) + keep_going = False + + fold_command = "fold" + if task.opt_aigfolds: + fold_command += " -s" + + abc_command, custom_options, toggles = abc_getopt(engine[1:], [ + "keep-going", + ]) if len(abc_command) == 0: task.error("Missing ABC command.") - for o, a in abc_opts: - task.error("Unexpected ABC engine options.") + if abc_command[0].startswith('-'): + task.error(f"Unexpected ABC engine option '{abc_command[0]}'.") if abc_command[0] == "bmc3": if mode != "bmc": task.error("ABC command 'bmc3' is only valid in bmc mode.") + for o, a in custom_options: + task.error(f"Option {o} not supported by 'abc {abc_command[0]}'") abc_command[0] += f" -F {task.opt_depth} -v" elif abc_command[0] == "sim3": if mode != "bmc": task.error("ABC command 'sim3' is only valid in bmc mode.") + for o, a in custom_options: + task.error(f"Option {o} not supported by 'abc {abc_command[0]}'") abc_command[0] += f" -F {task.opt_depth} -v" elif abc_command[0] == "pdr": if mode != "prove": task.error("ABC command 'pdr' is only valid in prove mode.") - abc_command[0] += f" -v -I engine_{engine_idx}/invariants.pla" + + for o, a in custom_options: + if o == '--keep-going': + keep_going = True + else: + task.error(f"Option {o} not supported by 'abc {abc_command[0]}'") + + abc_command[0] += " -v" + + if keep_going: + abc_command += ["-a", "-X", f"engine_{engine_idx}/trace_"] + + if 'd' in toggles: + abc_command += ["-I", f"engine_{engine_idx}/invariants.pla"] + if not task.opt_aigfolds: + fold_command += " -s" else: task.error(f"Invalid ABC command {abc_command[0]}.") @@ -66,9 +135,8 @@ def run(mode, task, engine_idx, engine): task, f"engine_{engine_idx}", task.model("aig"), - f"""cd {task.workdir}; {task.exe_paths["abc"]} -c 'read_aiger model/design_aiger.aig; fold{ - " -s" if task.opt_aigfolds or (abc_command[0].startswith("pdr ") and "-d" in abc_command[1:]) else "" - }; strash; {" ".join(abc_command)}; write_cex -a engine_{engine_idx}/trace.aiw'""", + f"""cd {task.workdir}; {task.exe_paths["abc"]} -c 'read_aiger model/design_aiger.aig; { + fold_command}; strash; {" ".join(abc_command)}; write_cex -a engine_{engine_idx}/trace.aiw'""", logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile.txt", "w") ) proc.checkretcode = True @@ -76,11 +144,42 @@ def run(mode, task, engine_idx, engine): proc.noprintregex = re.compile(r"^\.+$") proc_status = None + procs_running = 1 + + aiger_props = None + disproved = [] + def output_callback(line): nonlocal proc_status + nonlocal procs_running + nonlocal aiger_props - match = re.match(r"^Output [0-9]+ of miter .* was asserted in frame [0-9]+.", line) - if match: proc_status = "FAIL" + if keep_going and aiger_props is None: + with open(f"{task.workdir}/model/design_aiger.ywa") as ywa_file: + ywa = json.load(ywa_file) + aiger_props = [] + for path in ywa["asserts"]: + aiger_props.append(task.design.properties_by_path[tuple(path)]) + + if keep_going: + match = re.match(r"Writing CEX for output ([0-9]+) to engine_[0-9]+/(.*)\.aiw", line) + if match: + output = int(match[1]) + prop = aiger_props[output] + prop.status = "FAIL" + + task.status_db.set_task_property_status(prop, data=dict(source="abc pdr", engine=f"engine_{engine_idx}")) + disproved.append(output) + proc_status = "FAIL" + proc = aigsmt_trace_callback(task, engine_idx, proc_status, + run_aigsmt=run_aigsmt, smtbmc_vcd=smtbmc_vcd, smtbmc_append=smtbmc_append, sim_append=sim_append, + name=match[2], + ) + proc.register_exit_callback(exit_callback) + procs_running += 1 + else: + match = re.match(r"^Output [0-9]+ of miter .* was asserted in frame [0-9]+.", line) + if match: proc_status = "FAIL" match = re.match(r"^Simulation of [0-9]+ frames for [0-9]+ rounds with [0-9]+ restarts did not assert POs.", line) if match: proc_status = "UNKNOWN" @@ -94,11 +193,38 @@ def run(mode, task, engine_idx, engine): match = re.match(r"^Property proved.", line) if match: proc_status = "PASS" + if keep_going: + match = re.match(r"^Properties: All = (\d+). Proved = (\d+). Disproved = (\d+). Undecided = (\d+).", line) + if match: + all_count = int(match[1]) + proved_count = int(match[2]) + disproved_count = int(match[3]) + undecided_count = int(match[4]) + if ( + all_count == len(aiger_props) and + all_count == proved_count + disproved_count + undecided_count and + disproved_count == len(disproved) and + not undecided_count + ): + for i, prop in enumerate(aiger_props): + if i not in disproved: + prop.status = "PASS" + return line def exit_callback(retcode): - aigsmt_exit_callback(task, engine_idx, proc_status, - run_aigsmt=run_aigsmt, smtbmc_vcd=smtbmc_vcd, smtbmc_append=smtbmc_append, sim_append=sim_append, ) + nonlocal procs_running + if keep_going: + procs_running -= 1 + if not procs_running: + if proc_status == "FAIL" and mode == "bmc" and keep_going: + task.pass_unknown_asserts(dict(source="abc pdr", keep_going=True, engine=f"engine_{engine_idx}")) + task.update_status(proc_status) + task.summary.set_engine_status(engine_idx, proc_status) + task.terminate() + else: + aigsmt_exit_callback(task, engine_idx, proc_status, + run_aigsmt=run_aigsmt, smtbmc_vcd=smtbmc_vcd, smtbmc_append=smtbmc_append, sim_append=sim_append) proc.output_callback = output_callback proc.register_exit_callback(exit_callback) diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index d7a5a31..acba3a2 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -121,70 +121,107 @@ def run(mode, task, engine_idx, engine): def aigsmt_exit_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_vcd, smtbmc_append, sim_append): - if proc_status is None: - task.error(f"engine_{engine_idx}: Could not determine engine status.") + if proc_status is None: + task.error(f"engine_{engine_idx}: Could not determine engine status.") - task.update_status(proc_status) - task.summary.set_engine_status(engine_idx, proc_status) - task.terminate() + task.update_status(proc_status) + task.summary.set_engine_status(engine_idx, proc_status) + task.terminate() + if proc_status == "FAIL" and (not run_aigsmt or task.opt_aigsmt != "none"): + aigsmt_trace_callback(task, engine_idx, proc_status, run_aigsmt=run_aigsmt, smtbmc_vcd=smtbmc_vcd, smtbmc_append=smtbmc_append, sim_append=sim_append) - if proc_status == "FAIL" and (not run_aigsmt or task.opt_aigsmt != "none"): - trace_prefix = f"engine_{engine_idx}/trace" +def aigsmt_trace_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_vcd, smtbmc_append, sim_append, name="trace"): - aiw2yw_suffix = '_aiw' if run_aigsmt else '' + trace_prefix = f"engine_{engine_idx}/{name}" - witness_proc = SbyProc( - task, f"engine_{engine_idx}", [], - f"cd {task.workdir}; {task.exe_paths['witness']} aiw2yw engine_{engine_idx}/trace.aiw model/design_aiger.ywa engine_{engine_idx}/trace{aiw2yw_suffix}.yw", - ) - yw_proc = witness_proc + aiw2yw_suffix = '_aiw' if run_aigsmt else '' - if run_aigsmt: - smtbmc_opts = [] - smtbmc_opts += ["-s", task.opt_aigsmt] - if task.opt_tbtop is not None: - smtbmc_opts += ["--vlogtb-top", task.opt_tbtop] - smtbmc_opts += ["--noprogress", f"--append {smtbmc_append}"] - if smtbmc_vcd: - smtbmc_opts += [f"--dump-vcd {trace_prefix}.vcd"] - smtbmc_opts += [f"--dump-yw {trace_prefix}.yw", f"--dump-vlogtb {trace_prefix}_tb.v", f"--dump-smtc {trace_prefix}.smtc"] + witness_proc = SbyProc( + task, f"engine_{engine_idx}", [], + f"cd {task.workdir}; {task.exe_paths['witness']} aiw2yw engine_{engine_idx}/{name}.aiw model/design_aiger.ywa engine_{engine_idx}/{name}{aiw2yw_suffix}.yw", + ) + final_proc = witness_proc - proc2 = SbyProc( - task, - f"engine_{engine_idx}", - [*task.model("smt2"), witness_proc], - f"cd {task.workdir}; {task.exe_paths['smtbmc']} {' '.join(smtbmc_opts)} --yw engine_{engine_idx}/trace{aiw2yw_suffix}.yw model/design_smt2.smt2", - logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w") - ) + if run_aigsmt: + smtbmc_opts = [] + smtbmc_opts += ["-s", task.opt_aigsmt] + if task.opt_tbtop is not None: + smtbmc_opts += ["--vlogtb-top", task.opt_tbtop] + smtbmc_opts += ["--noprogress", f"--append {smtbmc_append}"] + if smtbmc_vcd: + smtbmc_opts += [f"--dump-vcd {trace_prefix}.vcd"] + smtbmc_opts += [f"--dump-yw {trace_prefix}.yw", f"--dump-vlogtb {trace_prefix}_tb.v", f"--dump-smtc {trace_prefix}.smtc"] - proc2_status = None + proc2 = SbyProc( + task, + f"engine_{engine_idx}", + [*task.model("smt2"), witness_proc], + f"cd {task.workdir}; {task.exe_paths['smtbmc']} {' '.join(smtbmc_opts)} --yw engine_{engine_idx}/{name}{aiw2yw_suffix}.yw model/design_smt2.smt2", + logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w"), + ) - def output_callback2(line): - nonlocal proc2_status + proc2_status = None - match = re.match(r"^## [0-9: ]+ Status: FAILED", line) - if match: proc2_status = "FAIL" + last_prop = [] + current_step = None - match = re.match(r"^## [0-9: ]+ Status: PASSED", line) - if match: proc2_status = "PASS" + def output_callback2(line): + nonlocal proc2_status + nonlocal last_prop + nonlocal current_step - return line + smt2_trans = {'\\':'/', '|':'/'} - def exit_callback2(retcode): - if proc2_status is None: - task.error(f"engine_{engine_idx}: Could not determine aigsmt status.") - if proc2_status != "FAIL": - task.error(f"engine_{engine_idx}: Unexpected aigsmt status.") - if os.path.exists(f"{task.workdir}/engine_{engine_idx}/trace.vcd"): - task.summary.add_event(engine_idx, trace="trace", path=f"engine_{engine_idx}/trace.vcd", type="$assert") + match = re.match(r"^## [0-9: ]+ .* in step ([0-9]+)\.\.", line) + if match: + current_step = int(match[1]) + return line - proc2.output_callback = output_callback2 - proc2.register_exit_callback(exit_callback2) + match = re.match(r"^## [0-9: ]+ Status: FAILED", line) + if match: proc2_status = "FAIL" - yw_proc = proc2 + match = re.match(r"^## [0-9: ]+ Status: PASSED", line) + if match: proc2_status = "PASS" - if task.opt_fst or (task.opt_vcd and task.opt_vcd_sim): - sim_witness_trace(f"engine_{engine_idx}", task, engine_idx, f"engine_{engine_idx}/trace.yw", append=sim_append, deps=[yw_proc]) + match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+)(?: \((\S+)\))?", line) + if match: + cell_name = match[3] or match[2] + prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans) + prop.status = "FAIL" + last_prop.append(prop) + return line - else: - task.log(f"{click.style(f'engine_{engine_idx}', fg='magenta')}: Engine did not produce a counter example.") + match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line) + if match: + tracefile = match[1] + trace = os.path.basename(tracefile)[:-4] + task.summary.add_event(engine_idx=engine_idx, trace=trace, path=tracefile) + + if match and last_prop: + for p in last_prop: + task.summary.add_event( + engine_idx=engine_idx, trace=trace, + type=p.celltype, hdlname=p.hdlname, src=p.location, step=current_step) + p.tracefiles.append(tracefile) + last_prop = [] + return line + + return line + + def exit_callback2(retcode): + if proc2_status is None: + task.error(f"engine_{engine_idx}: Could not determine aigsmt status.") + if proc2_status != "FAIL": + task.error(f"engine_{engine_idx}: Unexpected aigsmt status.") + + proc2.output_callback = output_callback2 + proc2.register_exit_callback(exit_callback2) + + final_proc = proc2 + + if task.opt_fst or (task.opt_vcd and task.opt_vcd_sim): + final_proc = sim_witness_trace(f"engine_{engine_idx}", task, engine_idx, f"engine_{engine_idx}/{name}.yw", append=sim_append, deps=[final_proc]) + elif not run_aigsmt: + task.log(f"{click.style(f'engine_{engine_idx}', fg='magenta')}: Engine did not produce a counter example.") + + return final_proc diff --git a/tests/keepgoing/check_output.py b/tests/keepgoing/check_output.py index ab531eb..fb2b969 100644 --- a/tests/keepgoing/check_output.py +++ b/tests/keepgoing/check_output.py @@ -12,6 +12,6 @@ def line_ref(dir, filename, pattern): for number, line in enumerate(file, 1): if pattern_re.search(line): # Needs to match source locations for both verilog frontends - return fr"{filename}:(?:{number}|\d+.\d+-{number}.\d+)" + return fr"{filename}:(?:{number}|\d+\.\d+-{number}\.\d+)" raise RuntimeError("%s: pattern `%s` not found" % (filename, pattern)) diff --git a/tests/keepgoing/keepgoing_multi_step.py b/tests/keepgoing/keepgoing_multi_step.py index 548f9d2..d250614 100644 --- a/tests/keepgoing/keepgoing_multi_step.py +++ b/tests/keepgoing/keepgoing_multi_step.py @@ -11,21 +11,34 @@ step_5 = line_ref(workdir, src, "step 5") step_7 = line_ref(workdir, src, "step 7") log = open(workdir + "/logfile.txt").read() -log_per_trace = log.split("Writing trace to Yosys witness file")[:-1] +if "_abc]" not in log: + log_per_trace = log.split("Writing trace to Yosys witness file")[:-1] + assert len(log_per_trace) == 4 + assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_0, log_per_trace[0], re.M) + + for i in range(1, 4): + assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % assert_0, log_per_trace[i], re.M) + + + assert re.search(r"Assert failed in test: %s \(.*\)$" % step_3_7, log_per_trace[1], re.M) + assert re.search(r"Assert failed in test: %s \(.*\)$" % step_5, log_per_trace[2], re.M) + assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % step_3_7, log_per_trace[3], re.M) + assert re.search(r"Assert failed in test: %s \(.*\)$" % step_7, log_per_trace[3], re.M) + + pattern = f"Property ASSERT in test at {assert_0} failed. Trace file: engine_0/trace0.(vcd|fst)" + assert re.search(pattern, open(f"{workdir}/{workdir}.xml").read()) + +log_per_trace = log.split("summary: counterexample trace")[1:] assert len(log_per_trace) == 4 +for i in range(4): + assert re.search(r"failed assertion test\..* at %s" % assert_0, log_per_trace[i], re.M) -assert re.search(r"Assert failed in test: %s \(.*\)$" % assert_0, log_per_trace[0], re.M) +step_3_7_traces = [i for i, t in enumerate(log_per_trace) if re.search(r"failed assertion test\..* at %s" % step_3_7, t, re.M)] +step_5_traces = [i for i, t in enumerate(log_per_trace) if re.search(r"failed assertion test\..* at %s" % step_5, t, re.M)] +step_7_traces = [i for i, t in enumerate(log_per_trace) if re.search(r"failed assertion test\..* at %s" % step_7, t, re.M)] -for i in range(1, 4): - assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % assert_0, log_per_trace[i], re.M) - - -assert re.search(r"Assert failed in test: %s \(.*\)$" % step_3_7, log_per_trace[1], re.M) -assert re.search(r"Assert failed in test: %s \(.*\)$" % step_5, log_per_trace[2], re.M) -assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % step_3_7, log_per_trace[3], re.M) -assert re.search(r"Assert failed in test: %s \(.*\)$" % step_7, log_per_trace[3], re.M) - -pattern = f"Property ASSERT in test at {assert_0} failed. Trace file: engine_0/trace0.(vcd|fst)" -assert re.search(pattern, open(f"{workdir}/{workdir}.xml").read()) +assert len(step_3_7_traces) == 2 +assert len(step_5_traces) == 1 +assert len(step_7_traces) == 1 diff --git a/tests/keepgoing/keepgoing_multi_step.sby b/tests/keepgoing/keepgoing_multi_step.sby index b9b0ba5..5e6a985 100644 --- a/tests/keepgoing/keepgoing_multi_step.sby +++ b/tests/keepgoing/keepgoing_multi_step.sby @@ -1,6 +1,7 @@ [tasks] bmc prove +abc : prove [options] bmc: mode bmc @@ -8,7 +9,8 @@ prove: mode prove expect fail [engines] -smtbmc --keep-going boolector +~abc: smtbmc --keep-going boolector +abc: abc --keep-going pdr [script] read -sv keepgoing_multi_step.sv diff --git a/tests/keepgoing/keepgoing_multi_step.sv b/tests/keepgoing/keepgoing_multi_step.sv index 8d5d8e3..553b13c 100644 --- a/tests/keepgoing/keepgoing_multi_step.sv +++ b/tests/keepgoing/keepgoing_multi_step.sv @@ -18,5 +18,6 @@ module test ( if (counter == 7) begin assert(a); // step 7 end + assert(1); end endmodule From d3a6f2d75837e71aa41f133008f94f0a01c9902b Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 20 Feb 2024 13:56:44 +0100 Subject: [PATCH 3/4] Emit status db update from aigsmt --- sbysrc/sby_engine_aiger.py | 1 + 1 file changed, 1 insertion(+) diff --git a/sbysrc/sby_engine_aiger.py b/sbysrc/sby_engine_aiger.py index acba3a2..fbdf999 100644 --- a/sbysrc/sby_engine_aiger.py +++ b/sbysrc/sby_engine_aiger.py @@ -188,6 +188,7 @@ def aigsmt_trace_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_v cell_name = match[3] or match[2] prop = task.design.hierarchy.find_property_by_cellname(cell_name, trans_dict=smt2_trans) prop.status = "FAIL" + task.status_db.set_task_property_status(prop, data=dict(source="aigsmt", engine=f"engine_{engine_idx}")) last_prop.append(prop) return line From b6e41a388b6e929abaf97ae141a11ff8ade04c0a Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 27 Feb 2024 20:09:45 +0100 Subject: [PATCH 4/4] Support for the new anytime schedule in yosys-abc's pdr --- sbysrc/sby_core.py | 4 +++ sbysrc/sby_engine_abc.py | 50 ++++++++++++++++++++++++------------- sbysrc/sby_engine_smtbmc.py | 7 +++--- 3 files changed, 41 insertions(+), 20 deletions(-) diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py index 609be95..c366e1b 100644 --- a/sbysrc/sby_core.py +++ b/sbysrc/sby_core.py @@ -1027,6 +1027,7 @@ class SbyTask(SbyConfig): print("setundef -undriven -anyseq", file=f) print("opt -fast", file=f) if self.opt_witrename: + # we need to run this a second time to handle anything added by prep print("rename -witness", file=f) print("opt_clean", file=f) print(f"""write_rtlil ../model/design_prep.il""", file=f) @@ -1048,6 +1049,9 @@ class SbyTask(SbyConfig): print(cmd, file=f) # the user must designate a top module in [script] print("hierarchy -smtcheck", file=f) + # we need to give flatten-preserved names before write_jny + if self.opt_witrename: + print("rename -witness", file=f) print(f"""write_jny -no-connections ../model/design.json""", file=f) print(f"""write_rtlil ../model/design.il""", file=f) diff --git a/sbysrc/sby_engine_abc.py b/sbysrc/sby_engine_abc.py index 7992377..54ff169 100644 --- a/sbysrc/sby_engine_abc.py +++ b/sbysrc/sby_engine_abc.py @@ -103,7 +103,7 @@ def run(mode, task, engine_idx, engine): else: task.error(f"Option {o} not supported by 'abc {abc_command[0]}'") - abc_command[0] += " -v" + abc_command[0] += " -v -l" if keep_going: abc_command += ["-a", "-X", f"engine_{engine_idx}/trace_"] @@ -142,34 +142,35 @@ def run(mode, task, engine_idx, engine): proc.checkretcode = True proc.noprintregex = re.compile(r"^\.+$") - proc_status = None + proc_status = "UNKNOWN" procs_running = 1 aiger_props = None - disproved = [] + disproved = set() + proved = set() def output_callback(line): nonlocal proc_status nonlocal procs_running nonlocal aiger_props - if keep_going and aiger_props is None: + if aiger_props is None: with open(f"{task.workdir}/model/design_aiger.ywa") as ywa_file: ywa = json.load(ywa_file) aiger_props = [] for path in ywa["asserts"]: - aiger_props.append(task.design.properties_by_path[tuple(path)]) + aiger_props.append(task.design.properties_by_path.get(tuple(path))) if keep_going: match = re.match(r"Writing CEX for output ([0-9]+) to engine_[0-9]+/(.*)\.aiw", line) if match: output = int(match[1]) prop = aiger_props[output] - prop.status = "FAIL" - - task.status_db.set_task_property_status(prop, data=dict(source="abc pdr", engine=f"engine_{engine_idx}")) - disproved.append(output) + if prop: + prop.status = "FAIL" + task.status_db.set_task_property_status(prop, data=dict(source="abc pdr", engine=f"engine_{engine_idx}")) + disproved.add(output) proc_status = "FAIL" proc = aigsmt_trace_callback(task, engine_idx, proc_status, run_aigsmt=run_aigsmt, smtbmc_vcd=smtbmc_vcd, smtbmc_append=smtbmc_append, sim_append=sim_append, @@ -181,6 +182,15 @@ def run(mode, task, engine_idx, engine): match = re.match(r"^Output [0-9]+ of miter .* was asserted in frame [0-9]+.", line) if match: proc_status = "FAIL" + match = re.match(r"^Proved output +([0-9]+) in frame +[0-9]+", line) + if match: + output = int(match[1]) + prop = aiger_props[output] + if prop: + prop.status = "PASS" + task.status_db.set_task_property_status(prop, data=dict(source="abc pdr", engine=f"engine_{engine_idx}")) + proved.add(output) + match = re.match(r"^Simulation of [0-9]+ frames for [0-9]+ rounds with [0-9]+ restarts did not assert POs.", line) if match: proc_status = "UNKNOWN" @@ -201,14 +211,19 @@ def run(mode, task, engine_idx, engine): disproved_count = int(match[3]) undecided_count = int(match[4]) if ( - all_count == len(aiger_props) and - all_count == proved_count + disproved_count + undecided_count and - disproved_count == len(disproved) and - not undecided_count + all_count != len(aiger_props) or + all_count != proved_count + disproved_count + undecided_count or + disproved_count != len(disproved) or + proved_count != len(proved) ): - for i, prop in enumerate(aiger_props): - if i not in disproved: - prop.status = "PASS" + log("WARNING: inconsistent status output") + proc_status = "UNKNOWN" + elif proved_count == all_count: + proc_status = "PASS" + elif disproved_count == 0: + proc_status = "UNKNOWN" + else: + proc_status = "FAIL" return line @@ -221,7 +236,8 @@ def run(mode, task, engine_idx, engine): task.pass_unknown_asserts(dict(source="abc pdr", keep_going=True, engine=f"engine_{engine_idx}")) task.update_status(proc_status) task.summary.set_engine_status(engine_idx, proc_status) - task.terminate() + if proc_status != "UNKNOWN" and not keep_going: + task.terminate() else: aigsmt_exit_callback(task, engine_idx, proc_status, run_aigsmt=run_aigsmt, smtbmc_vcd=smtbmc_vcd, smtbmc_append=smtbmc_append, sim_append=sim_append) diff --git a/sbysrc/sby_engine_smtbmc.py b/sbysrc/sby_engine_smtbmc.py index 3b43113..5fb0b89 100644 --- a/sbysrc/sby_engine_smtbmc.py +++ b/sbysrc/sby_engine_smtbmc.py @@ -295,8 +295,8 @@ def run(mode, task, engine_idx, engine): task.pass_unknown_asserts(dict(source="smtbmc", keep_going=True, engine=f"engine_{engine_idx}")) proc_status_lower = proc_status.lower() if proc_status == "PASS" else proc_status task.summary.set_engine_status(engine_idx, proc_status_lower) - - task.terminate() + if not keep_going: + task.terminate() elif mode in ["prove_basecase", "prove_induction"]: proc_status_lower = proc_status.lower() if proc_status == "PASS" else proc_status @@ -326,7 +326,8 @@ def run(mode, task, engine_idx, engine): if task.basecase_pass and task.induction_pass: task.update_status("PASS") task.summary.append("successful proof by k-induction.") - task.terminate() + if not keep_going: + task.terminate() else: assert False