riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #4431 from jix/smtbmc-fixes 

smtbmc: Fix two .yw handling related crashes
This commit is contained in:
Miodrag Milanović 2024-06-06 18:19:06 +02:00 committed by GitHub
parent 855ac285f4 094fa8caba
commit baccf87d9c
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
1 changed files with 5 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
backends/smt2/smtbmc.py
View File

@ -719,6 +719,8 @@ def smt_extract_mask(smt_expr, mask):
return combined_chunks, ''.join(mask_index_order[start:end] for start, end in chunks)[::-1] return combined_chunks, ''.join(mask_index_order[start:end] for start, end in chunks)[::-1]
def smt_concat(exprs): def smt_concat(exprs):
if not isinstance(exprs, (tuple, list)):
exprs = tuple(exprs)
if not exprs: if not exprs:
return "" return ""
if len(exprs) == 1: if len(exprs) == 1:
@ -818,6 +820,9 @@ def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False):
if not bits_re.match(bits): if not bits_re.match(bits):
raise ValueError("unsupported bit value in Yosys witness file") raise ValueError("unsupported bit value in Yosys witness file")
if bits.count('?') == len(bits):
continue
smt_expr = ywfile_signal(sig, map_steps.get(t, t)) smt_expr = ywfile_signal(sig, map_steps.get(t, t))
smt_expr, bits = smt_extract_mask(smt_expr, bits) smt_expr, bits = smt_extract_mask(smt_expr, bits)