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

More depth tracking

Browse source 
`SbyTask::update_status()` optionally takes the current step/depth, which gets used for some solvers/engines when exiting to pass unknown properties.
btor engine tracks the current step, but it doesn't track/report which property triggered a CEX so it's only useful on exit.
Use data source as a fallback if engine isn't provided (such as when coming from the `task_status` instead of an engine update).
This commit is contained in:
Krystine Sherwin 2025-07-08 15:47:31 +12:00
parent 0367db76f5
commit a332b017e4
No known key found for this signature in database
4 changed files with 18 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

7
sbysrc/sby_engine_smtbmc.py
View file

@ -300,10 +300,11 @@ def run(mode, task, engine_idx, engine):
simple_exit_callback(retcode)
def last_exit_callback():
nonlocal current_step
if mode == "bmc" or mode == "cover":
task.update_status(proc_status)
task.update_status(proc_status, current_step)
if proc_status == "FAIL" and mode == "bmc" and keep_going:
task.pass_unknown_asserts(dict(source="smtbmc", keep_going=True, engine=f"engine_{engine_idx}"))
task.pass_unknown_asserts(dict(source="smtbmc", keep_going=True, engine=f"engine_{engine_idx}", step=current_step))
proc_status_lower = proc_status.lower() if proc_status == "PASS" else proc_status
task.summary.set_engine_status(engine_idx, proc_status_lower)
if not keep_going:
@ -335,7 +336,7 @@ def run(mode, task, engine_idx, engine):
assert False
if task.basecase_pass and task.induction_pass:
task.update_status("PASS")
task.update_status("PASS", current_step)
task.summary.append("successful proof by k-induction.")
if not keep_going:
task.terminate()