diff options
| author | Jannis Harder <me@jix.one> | 2022-10-12 19:01:24 +0200 |
|---|---|---|
| committer | Jannis Harder <me@jix.one> | 2022-10-12 19:48:36 +0200 |
| commit | 4d334fd3e352f86e46e5810ae021b9ba0bf03752 (patch) | |
| tree | 54858b2035152d683f0b3d00c10f6dbe7d97430a /backends/smt2/smtbmc.py | |
| parent | f35c062354668b817a0f911fe9158b6b1e150617 (diff) | |
| download | yosys-4d334fd3e352f86e46e5810ae021b9ba0bf03752.tar.gz yosys-4d334fd3e352f86e46e5810ae021b9ba0bf03752.tar.bz2 yosys-4d334fd3e352f86e46e5810ae021b9ba0bf03752.zip | |
smt2/smtbmc: Fix FF witness data for fine grained or multi chunk FFs
The witness metadata was missing fine grained FFs completely and for
coarse grained FFs where the output connection has multiple chunks it
lacked the offset of the chunk within the SMT expression. This fixes
both, the later by adding an "smtoffset" field to the metadata.
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() |