sim: Improvements and fixes for yw cosim

  * Fixed $cover handling
  * Improved sparse memory handling when writing traces
  * JSON summary output

3 files changed, 50 insertions, 47 deletions

diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 5cfdff3fb..4ef28be9f 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -20,6 +20,7 @@
 #include "kernel/yosys.h"
 #include "kernel/sigtools.h"
 #include "kernel/json.h"
+#include "kernel/yw.h"
 #include "libs/json11/json11.hpp"
 
 USING_YOSYS_NAMESPACE
@@ -710,18 +711,6 @@ struct AigerWriter
 			f << it.second;
 	}
 
-	template<class T> static std::vector<std::string> witness_path(T *obj) {
-		std::vector<std::string> path;
-		if (obj->name.isPublic()) {
-			auto hdlname = obj->get_string_attribute(ID::hdlname);
-			for (auto token : split_tokens(hdlname))
-				path.push_back("\\" + token);
-		}
-		if (path.empty())
-			path.push_back(obj->name.str());
-		return path;
-	}
-
 	void write_ywmap(PrettyJson &json)
 	{
 		json.begin_object();
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 4315f6f67..4eb675c3c 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -29,6 +29,7 @@
 #include "kernel/log.h"
 #include "kernel/mem.h"
 #include "kernel/json.h"
+#include "kernel/yw.h"
 #include <string>
 
 USING_YOSYS_NAMESPACE
@@ -141,18 +142,6 @@ struct BtorWorker
 		return " " + infostr;
 	}
 
-	template<class T> static std::vector<std::string> witness_path(T *obj) {
-		std::vector<std::string> path;
-		if (obj->name.isPublic()) {
-			auto hdlname = obj->get_string_attribute(ID::hdlname);
-			for (auto token : split_tokens(hdlname))
-				path.push_back("\\" + token);
-		}
-		if (path.empty())
-			path.push_back(obj->name.str());
-		return path;
-	}
-
 	void ywmap_state(const SigSpec &sig) {
 		if (ywmap_json.active())
 			ywmap_states.emplace_back(sig);
diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py
index 14cf61fd7..8d0cc8112 100644
--- a/backends/smt2/witness.py
+++ b/backends/smt2/witness.py
@@ -316,6 +316,7 @@ def wit2yw(input, mapfile, output):
         if current_t > t:
             t = current_t
             values = WitnessValues()
+            array_inits = set()
             frames.append(values)
 
         line = next(input, None)
@@ -327,39 +328,63 @@ def wit2yw(input, mapfile, output):
             line = next(input, None)
 
             btor_sig = btor_map.data[mode][int(tokens[0])]
+            btor_sigs = [btor_sig]
 
             if btor_sig is None:
                 continue
 
             if isinstance(btor_sig, dict):
                 addr = tokens[1]
-                if not addr.startswith('[') or not addr.endswith(']'):
+                if not addr.startswith('['):
+                    addr = '[*]'
+                    value = tokens[1]
+                else:
+                    value = tokens[2]
+                if not addr.endswith(']'):
                     raise click.ClickException(f"{input_name}: expected address in BTOR witness file")
-                addr = int(addr[1:-1], 2)
+                path = btor_sig["path"]
+                width = btor_sig["width"]
+                size = btor_sig["size"]
+                if addr == '[*]':
+                    btor_sigs = [
+                        [{
+                            "path": (*path, f"\\[{addr}]"),
+                            "width": width,
+                            "offset": 0,
+                        }]
+                        for addr in range(size)
+                        if (path, addr) not in array_inits
+                    ]
+                    array_inits.update((path, addr) for addr in range(size))
+                else:
+                    addr = int(addr[1:-1], 2)
+
+                    if addr < 0 or addr >= size:
+                        raise click.ClickException(f"{input_name}: out of bounds address in BTOR witness file")
+
+                    array_inits.add((path, addr))
+                    btor_sig = [{
+                        "path": (*path, f"\\[{addr}]"),
+                        "width": width,
+                        "offset": 0,
+                    }]
+                    btor_sigs = [btor_sig]
+            else:
+                value = tokens[1]
 
-                if addr < 0 or addr >= btor_sig["size"]:
-                    raise click.ClickException(f"{input_name}: out of bounds address in BTOR witness file")
+            for btor_sig in btor_sigs:
+                value_bits = iter(reversed(value))
 
-                btor_sig = [{
-                    "path": (*btor_sig["path"], f"\\[{addr}]"),
-                    "width": btor_sig["width"],
-                    "offset": 0,
-                }]
+                for chunk in btor_sig:
+                    offset = chunk["offset"]
+                    path = chunk["path"]
+                    for i in range(offset, offset + chunk["width"]):
+                        key = (path, i)
+                        bits[key] = mode == "inputs"
+                        values[key] = next(value_bits)
 
-                signal_value = iter(reversed(tokens[2]))
-            else:
-                signal_value = iter(reversed(tokens[1]))
-
-            for chunk in btor_sig:
-                offset = chunk["offset"]
-                path = chunk["path"]
-                for i in range(offset, offset + chunk["width"]):
-                    key = (path, i)
-                    bits[key] = mode == "inputs"
-                    values[key] = next(signal_value)
-
-            if next(signal_value, None) is not None:
-                raise click.ClickException(f"{input_name}: excess bits in BTOR witness file")
+                if next(value_bits, None) is not None:
+                    raise click.ClickException(f"{input_name}: excess bits in BTOR witness file")
 
 
     if line is None: