diff options
| author | Jannis Harder <me@jix.one> | 2022-10-12 20:50:00 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2022-10-12 20:50:00 +0200 |
| commit | 33a2773de0605cb19e26fc6675fb3e86273c5087 (patch) | |
| tree | 54858b2035152d683f0b3d00c10f6dbe7d97430a /backends/smt2/smtbmc.py | |
| parent | f35c062354668b817a0f911fe9158b6b1e150617 (diff) | |
| parent | 4d334fd3e352f86e46e5810ae021b9ba0bf03752 (diff) | |
| download | yosys-33a2773de0605cb19e26fc6675fb3e86273c5087.tar.gz yosys-33a2773de0605cb19e26fc6675fb3e86273c5087.tar.bz2 yosys-33a2773de0605cb19e26fc6675fb3e86273c5087.zip | |
Merge pull request #3510 from jix/ff_witness_fixes
smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs
Diffstat (limited to 'backends/smt2/smtbmc.py')
| -rw-r--r-- | backends/smt2/smtbmc.py | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 5f05287de..ac329053f 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -669,7 +669,7 @@ if inywfile is not None: if common_end <= common_offset: continue - smt_expr = smt.net_expr(topmod, f"s{t}", wire["smtpath"]) + smt_expr = smt.witness_net_expr(topmod, f"s{t}", wire) if not smt_bool: slice_high = common_end - offset - 1 @@ -1267,7 +1267,8 @@ def write_yw_trace(steps_start, steps_stop, index, allregs=False): sigs = seqs for sig in sigs: - step_values[sig["sig"]] = smt.bv2bin(smt.get(smt.net_expr(topmod, f"s{k}", sig["smtpath"]))) + value = smt.bv2bin(smt.get(smt.witness_net_expr(topmod, f"s{k}", sig))) + step_values[sig["sig"]] = value yw.step(step_values) yw.end_trace() |