mirrors/sby
3
0
Fork 0
mirror of https://github.com/YosysHQ/sby.git synced 2025-08-16 01:45:30 +00:00
Code Activity

Don't fail cover props on failed assert

Browse source
This commit is contained in:
Krystine Sherwin 2025-07-05 12:53:54 +12:00
parent 911ae02ee5
commit ef8ca40a5d
No known key found for this signature in database
1 changed files with 4 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

5
sbysrc/sby_engine_smtbmc.py
View file

@ -187,6 +187,7 @@ def run(mode, task, engine_idx, engine):
pending_sim = None pending_sim = None
current_step = None current_step = None
procs_running = 1 procs_running = 1
failed_assert = False
def output_callback(line): def output_callback(line):
nonlocal proc_status nonlocal proc_status
@ -194,6 +195,7 @@ def run(mode, task, engine_idx, engine):
nonlocal pending_sim nonlocal pending_sim
nonlocal current_step nonlocal current_step
nonlocal procs_running nonlocal procs_running
nonlocal failed_assert
if pending_sim: if pending_sim:
sim_proc = sim_witness_trace(procname, task, engine_idx, pending_sim, append=sim_append, inductive=mode == "prove_induction") sim_proc = sim_witness_trace(procname, task, engine_idx, pending_sim, append=sim_append, inductive=mode == "prove_induction")
@ -235,6 +237,7 @@ def run(mode, task, engine_idx, engine):
match = re.match(r"^## [0-9: ]+ Assert failed in ([^:]+): (\S+)(?: \((\S+)\))?", line) match = re.match(r"^## [0-9: ]+ Assert failed in ([^:]+): (\S+)(?: \((\S+)\))?", line)
if match: if match:
failed_assert = not keep_going
path = parse_mod_path(match[1]) path = parse_mod_path(match[1])
cell_name = match[3] or match[2] cell_name = match[3] or match[2]
prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans) prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans)
@ -276,7 +279,7 @@ def run(mode, task, engine_idx, engine):
pending_sim = tracefile pending_sim = tracefile
match = re.match(r"^## [0-9: ]+ Unreached cover statement at ([^:]+): (\S+)(?: \((\S+)\))?", line) match = re.match(r"^## [0-9: ]+ Unreached cover statement at ([^:]+): (\S+)(?: \((\S+)\))?", line)
if match: if match and not failed_assert:
path = parse_mod_path(match[1]) path = parse_mod_path(match[1])
cell_name = match[3] or match[2] cell_name = match[3] or match[2]
prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans) prop = task.design.hierarchy.find_property(path, cell_name, trans_dict=smt2_trans)