mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-04-05 14:04:07 +00:00
Code Activity

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

Browse source
This commit is contained in:
Jannis Harder 2024-02-27 20:09:45 +01:00
parent d3a6f2d758
commit b6e41a388b
3 changed files with 41 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
sbysrc/sby_core.py
View file

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

50
sbysrc/sby_engine_abc.py
View file

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

7
sbysrc/sby_engine_smtbmc.py
View file

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