mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2026-07-14 23:35:42 +00:00
Code Activity

don't call yosys-witness on (unsupported) justice witnesses

Browse source
This commit is contained in:
N. Engelhardt 2026-07-07 12:50:02 +02:00
parent d11cc34cb3
commit b2b067757e
1 changed files with 3 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
sbysrc/sby_engine_aiger.py
View file

@ -181,6 +181,9 @@ def aigsmt_exit_callback(task, engine_idx, proc_status, *, run_aigsmt, smtbmc_vc
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 task.opt_mode == "live":
# we don't have any tools to process or visualize justice (lasso) witnesses
return
if proc_status == "FAIL" and (not run_aigsmt or task.opt_aigsmt != "none"): 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) aigsmt_trace_callback(task, engine_idx, proc_status, run_aigsmt=run_aigsmt, smtbmc_vcd=smtbmc_vcd, smtbmc_append=smtbmc_append, sim_append=sim_append)