mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-01-21 17:44:45 +00:00
Code Activity

Deliver more helpful error messages

Browse source
This commit is contained in:
Gus Smith 2026-01-06 16:19:54 -08:00
parent 9f77465170
commit 4d237bdd92
1 changed files with 30 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

32
backends/smt2/smtbmc.py
View file

@ -735,6 +735,12 @@ def ywfile_signal(sig, step, mask=None):
output = []
def ywfile_signal_error(reason, detail=None):
msg = f"Yosys witness signal mismatch for {sig.pretty()}: {reason}"
if detail:
msg += f" ({detail})"
raise ValueError(msg)
if sig.path in smt_wires:
for wire in smt_wires[sig.path]:
width, offset = wire["width"], wire["offset"]
@ -765,6 +771,12 @@ def ywfile_signal(sig, step, mask=None):
for mem in smt_mems[sig.memory_path]:
width, size, bv = mem["width"], mem["size"], mem["statebv"]
if sig.memory_addr is not None and sig.memory_addr >= size:
ywfile_signal_error(
"memory address out of bounds",
f"address={sig.memory_addr} size={size}",
)
smt_expr = smt.net_expr(topmod, f"s{step}", mem["smtpath"])
if bv:
@ -781,18 +793,34 @@ def ywfile_signal(sig, step, mask=None):
smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr)
output.append((0, sig.width, smt_expr))
else:
ywfile_signal_error("memory not found in design")
output.sort()
output = [chunk for chunk in output if chunk[0] != chunk[1]]
if not output:
if sig.memory_path:
ywfile_signal_error("memory signal has no matching bits in design")
else:
ywfile_signal_error("signal not found in design")
pos = 0
for start, end, smt_expr in output:
assert start == pos
if start != pos:
ywfile_signal_error(
"signal width/offset mismatch",
f"expected coverage at bit {pos}",
)
pos = end
assert pos == sig.width
if pos != sig.width:
ywfile_signal_error(
"signal width/offset mismatch",
f"covered {pos} of {sig.width} bits",
)
if len(output) == 1:
return output[0][-1]