Support for the new anytime schedule in yosys-abc's pdr

sbysrc/sby_core.py

@@ -1027,6 +1027,7 @@ def make_model(self, model_name):
                     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 @@ def make_model(self, model_name):
                     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)
 

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)])
+                    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 output_callback(line):
             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 output_callback(line):
                 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 exit_callback(retcode):
                     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)

sbysrc/sby_engine_smtbmc.py

@@ -295,8 +295,8 @@ def last_exit_callback():
                 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 last_exit_callback():
             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