Support for "abc --keep-going pdr" via new "pdr -X" mode

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 ''}"
 

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:
+    if abc_command[0].startswith('-'):
-        task.error("Unexpected ABC engine options.")
+        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{
+        f"""cd {task.workdir}; {task.exe_paths["abc"]} -c 'read_aiger model/design_aiger.aig; {
-                " -s" if task.opt_aigfolds or (abc_command[0].startswith("pdr ") and "-d" in abc_command[1:]) else ""
+            fold_command}; strash; {" ".join(abc_command)}; write_cex -a engine_{engine_idx}/trace.aiw'""",
-                }; 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 keep_going and aiger_props is None:
-        if match: proc_status = "FAIL"
+            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,
+        nonlocal procs_running
-            run_aigsmt=run_aigsmt, smtbmc_vcd=smtbmc_vcd, smtbmc_append=smtbmc_append, sim_append=sim_append, )
+        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)

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:
+    if proc_status is None:
-            task.error(f"engine_{engine_idx}: Could not determine engine status.")
+        task.error(f"engine_{engine_idx}: Could not determine engine status.")
 
-        task.update_status(proc_status)
+    task.update_status(proc_status)
-        task.summary.set_engine_status(engine_idx, proc_status)
+    task.summary.set_engine_status(engine_idx, proc_status)
-        task.terminate()
+    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"):
+def aigsmt_trace_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_vcd, smtbmc_append, sim_append, name="trace"):
-            trace_prefix = f"engine_{engine_idx}/trace"
 
-            aiw2yw_suffix = '_aiw' if run_aigsmt else ''
+    trace_prefix = f"engine_{engine_idx}/{name}"
 
-            witness_proc = SbyProc(
+    aiw2yw_suffix = '_aiw' if run_aigsmt else ''
-                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
 
-            if run_aigsmt:
+    witness_proc = SbyProc(
-                smtbmc_opts = []
+        task, f"engine_{engine_idx}", [],
-                smtbmc_opts += ["-s", task.opt_aigsmt]
+        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",
-                if task.opt_tbtop is not None:
+    )
-                    smtbmc_opts  += ["--vlogtb-top", task.opt_tbtop]
+    final_proc = witness_proc
-                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 = SbyProc(
+    if run_aigsmt:
-                    task,
+        smtbmc_opts = []
-                    f"engine_{engine_idx}",
+        smtbmc_opts += ["-s", task.opt_aigsmt]
-                    [*task.model("smt2"), witness_proc],
+        if task.opt_tbtop is not None:
-                    f"cd {task.workdir}; {task.exe_paths['smtbmc']} {' '.join(smtbmc_opts)} --yw engine_{engine_idx}/trace{aiw2yw_suffix}.yw model/design_smt2.smt2",
+            smtbmc_opts  += ["--vlogtb-top", task.opt_tbtop]
-                    logfile=open(f"{task.workdir}/engine_{engine_idx}/logfile2.txt", "w")
+        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):
+        proc2_status = None
-                    nonlocal proc2_status
 
-                    match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
+        last_prop = []
-                    if match: proc2_status = "FAIL"
+        current_step = None
 
-                    match = re.match(r"^## [0-9: ]+ Status: PASSED", line)
+        def output_callback2(line):
-                    if match: proc2_status = "PASS"
+            nonlocal proc2_status
+            nonlocal last_prop
+            nonlocal current_step
 
-                    return line
+            smt2_trans = {'\\':'/', '|':'/'}
 
-                def exit_callback2(retcode):
+            match = re.match(r"^## [0-9: ]+ .* in step ([0-9]+)\.\.", line)
-                    if proc2_status is None:
+            if match:
-                        task.error(f"engine_{engine_idx}: Could not determine aigsmt status.")
+                current_step = int(match[1])
-                    if proc2_status != "FAIL":
+                return line
-                        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")
 
-                proc2.output_callback = output_callback2
+            match = re.match(r"^## [0-9: ]+ Status: FAILED", line)
-                proc2.register_exit_callback(exit_callback2)
+            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):
+            match = re.match(r"^## [0-9: ]+ Assert failed in (\S+): (\S+)(?: \((\S+)\))?", line)
-                sim_witness_trace(f"engine_{engine_idx}", task, engine_idx, f"engine_{engine_idx}/trace.yw", append=sim_append, deps=[yw_proc])
+            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:
+            match = re.match(r"^## [0-9: ]+ Writing trace to VCD file: (\S+)", line)
-                task.log(f"{click.style(f'engine_{engine_idx}', fg='magenta')}: Engine did not produce a counter example.")
+            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

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))

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 len(step_3_7_traces) == 2
-    assert re.search(r"Assert failed in test: %s \(.*\) \[failed before\]$" % assert_0, log_per_trace[i], re.M)
+assert len(step_5_traces) == 1
-
+assert len(step_7_traces) == 1
-
-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())

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

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