From 6ba762db4cc37247c05513fb41e02da733ec3240 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Wed, 7 Feb 2024 18:43:23 +0100 Subject: [PATCH] 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