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

smtbmc: Use fewer smt commands while writing .yw traces 

Depending on the used solver and design this can be a signficant
performance improvement.
This commit is contained in:
Jannis Harder 2023-12-14 16:42:48 +01:00
parent 449e3dbbd3
commit 111085669b
1 changed files with 11 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

12
backends/smt2/smtbmc.py
View File

@ -1327,6 +1327,9 @@ def write_yw_trace(steps, index, allregs=False, filename=None):
sig = yw.add_sig(word_path, overlap_start, overlap_end - overlap_start, True)
mem_init_values.append((sig, overlap_bits.replace("x", "?")))
exprs = []
all_sigs = []
for i, k in enumerate(steps):
step_values = WitnessValues()
@ -1337,8 +1340,15 @@ def write_yw_trace(steps, index, allregs=False, filename=None):
else:
sigs = seqs
exprs.extend(smt.witness_net_expr(topmod, f"s{k}", sig) for sig in sigs)
all_sigs.append(sigs)
bvs = iter(smt.get_list(exprs))
for sigs in all_sigs:
for sig in sigs:
value = smt.bv2bin(smt.get(smt.witness_net_expr(topmod, f"s{k}", sig)))
value = smt.bv2bin(next(bvs))
step_values[sig["sig"]] = value
yw.step(step_values)