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

btor: Add unknown props

Browse source 
First during the init, then again at the end.  Depth information isn't available, since there may be a pending trace job for that depth which would provide a known status.
This commit is contained in:
Krystine Sherwin 2025-07-08 17:26:55 +12:00
parent 73c5e5cae6
commit af511945a3
No known key found for this signature in database
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
sbysrc/sby_engine_btor.py
View file

@ -91,6 +91,7 @@ def run(mode, task, engine_idx, engine):
proc_status = "FAIL" proc_status = "FAIL"
else: else:
task.error(f"engine_{engine_idx}: Engine terminated without status.") task.error(f"engine_{engine_idx}: Engine terminated without status.")
task.update_unknown_props(dict(source="btor", engine=f"engine_{engine_idx}"))
else: else:
if common_state.expected_cex == 0: if common_state.expected_cex == 0:
proc_status = "pass" proc_status = "pass"
@ -143,6 +144,7 @@ def run(mode, task, engine_idx, engine):
common_state.expected_cex = int(match[1]) common_state.expected_cex = int(match[1])
if common_state.produced_cex != 0: if common_state.produced_cex != 0:
task.error(f"engine_{engine_idx}: Unexpected engine output (property count).") task.error(f"engine_{engine_idx}: Unexpected engine output (property count).")
task.update_unknown_props(dict(source="btor_init", engine=f"engine_{engine_idx}"))
else: else:
task.error(f"engine_{engine_idx}: BTOR solver '{solver_args[0]}' is currently not supported in cover mode.") task.error(f"engine_{engine_idx}: BTOR solver '{solver_args[0]}' is currently not supported in cover mode.")