From e6f39148009df28280eacb25c0392c5bfbb39ce0 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Thu, 18 May 2023 11:58:09 +0200
Subject: [PATCH] smt2: Use smt bv offset for `$any*`'s smtoffset
While not setting the smtoffset here was clearly a bug, I think using
`chunk.offset` only worked incidentally. The `smtoffset` is an offset
into the `smtname, smtid` pair (here `"", idcounter`) which corresponds
to the smt bitvector `stringf("%s#%d", get_id(module), idcounter)` which
contains all the chunks this loop is iterating over.
Thus using an incrementing `smtoffset` (like the `$ff`/`$dff` case above
already does) should be the correct fix.
---
backends/smt2/smt2.cc | 7 +++++--
1 file changed, 5 insertions(+), 2 deletions(-)
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index bdef8d569..0ca3fbcac 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -626,9 +626,12 @@ struct Smt2Worker
}
bool init_only = cell->type.in(ID($anyconst), ID($anyinit), ID($allconst));
- for (auto chunk : cell->getPort(QY).chunks())
+ int smtoffset = 0;
+ for (auto chunk : cell->getPort(QY).chunks()) {
if (chunk.is_wire())
- decls.push_back(witness_signal(init_only ? "init" : "seq", chunk.width, chunk.offset, "", idcounter, chunk.wire, chunk.offset));
+ decls.push_back(witness_signal(init_only ? "init" : "seq", chunk.width, chunk.offset, "", idcounter, chunk.wire, smtoffset));
+ smtoffset += chunk.width;
+ }
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(QY)), log_signal(cell->getPort(QY)));
if (cell->type == ID($anyseq))