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