mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-05 09:04:08 +00:00
Code Activity

smt2: Use smt bv offset for $any*'s smtoffset

Browse source 
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.
This commit is contained in:
Jannis Harder 2023-05-18 11:58:09 +02:00
parent 52ad7a47f3
commit e6f3914800
1 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
backends/smt2/smt2.cc
View file

@ -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))