From 52ad7a47f3798f17d9c33209649136418fe1194f Mon Sep 17 00:00:00 2001
From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com>
Date: Thu, 18 May 2023 10:37:55 +1200
Subject: [PATCH 1/3] Assign wires an smtoffset

Wires weren't being assigned an smtoffset value so when generating a yosys witness trace it would also use an offset of 0.
Not sure if this has any other effects, but it fixes the bug I was having.
@jix could you take a look at this?
---
 backends/smt2/smt2.cc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 48da3f4be..bdef8d569 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -628,7 +628,7 @@ struct Smt2Worker
 				bool init_only = cell->type.in(ID($anyconst), ID($anyinit), ID($allconst));
 				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));
+						decls.push_back(witness_signal(init_only ? "init" : "seq", chunk.width, chunk.offset, "", idcounter, chunk.wire, chunk.offset));
 
 				makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(QY)), log_signal(cell->getPort(QY)));
 				if (cell->type == ID($anyseq))

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 2/3] 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))

From ad2b04d63a8639a294bfe6148ee262980fc962e1 Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Thu, 18 May 2023 16:50:11 +0200
Subject: [PATCH 3/3] sim: Fix cosimulation with nested modules having
 unconnected inputs

When assigning values to input ports of nested modules in cosimulation,
sim needs to find the actual driver of the signal to perform the
assignment. The existing code didn't handle unconnected inputs in that
scenario.
---
 passes/sat/sim.cc | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index fe1635249..273e9db86 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -223,7 +223,8 @@ struct SimInstance
 
 			if (wire->port_input && instance != nullptr && parent != nullptr) {
 				for (int i = 0; i < GetSize(sig); i++) {
-					in_parent_drivers.emplace(sig[i], parent->sigmap(instance->getPort(wire->name)[i]));
+					if (instance->hasPort(wire->name))
+						in_parent_drivers.emplace(sig[i], parent->sigmap(instance->getPort(wire->name)[i]));
 				}
 			}
 		}