sim: Improvements and fixes for yw cosim

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

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();

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

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,28 +328,52 @@ 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"]
-                if addr < 0 or addr >= btor_sig["size"]:
+                size = btor_sig["size"]
-                    raise click.ClickException(f"{input_name}: out of bounds address in BTOR witness file")
+                if addr == '[*]':
-
+                    btor_sigs = [
-                btor_sig = [{
+                        [{
-                    "path": (*btor_sig["path"], f"\\[{addr}]"),
+                            "path": (*path, f"\\[{addr}]"),
-                    "width": btor_sig["width"],
+                            "width": width,
                             "offset": 0,
                         }]
-
+                        for addr in range(size)
-                signal_value = iter(reversed(tokens[2]))
+                        if (path, addr) not in array_inits
+                    ]
+                    array_inits.update((path, addr) for addr in range(size))
                 else:
-                signal_value = iter(reversed(tokens[1]))
+                    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]
+
+            for btor_sig in btor_sigs:
+                value_bits = iter(reversed(value))
 
                 for chunk in btor_sig:
                     offset = chunk["offset"]
@@ -356,9 +381,9 @@ def wit2yw(input, mapfile, output):
                     for i in range(offset, offset + chunk["width"]):
                         key = (path, i)
                         bits[key] = mode == "inputs"
-                    values[key] = next(signal_value)
+                        values[key] = next(value_bits)
 
-            if next(signal_value, None) is not None:
+                if next(value_bits, None) is not None:
                     raise click.ClickException(f"{input_name}: excess bits in BTOR witness file")
 
 

kernel/yw.cc

@@ -161,7 +161,7 @@ ReadWitness::ReadWitness(const std::string &filename) :
 		signal.offset = signal_json["offset"].int_value();
 		if (signal.offset < 0)
 			log_error("Failed to parse `%s`: Invalid offset for signal `%s`\n", filename.c_str(), signal_json.dump().c_str());
-		signal.init_only = json["init_only"].bool_value();
+		signal.init_only = signal_json["init_only"].bool_value();
 		signals.push_back(signal);
 	}
 

kernel/yw.h

@@ -52,6 +52,18 @@ struct WitnessHierarchyItem {
 template<typename D, typename T>
 void witness_hierarchy(RTLIL::Module *module, D data, T callback);
 
+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;
+}
+
 struct ReadWitness
 {
 	struct Clock {

passes/sat/sim.cc

@@ -24,6 +24,7 @@
 #include "kernel/fstdata.h"
 #include "kernel/ff.h"
 #include "kernel/yw.h"
+#include "kernel/json.h"
 
 #include <ctime>
 
@@ -75,6 +76,17 @@ struct OutputWriter
 	SimWorker *worker;
 };
 
+struct SimInstance;
+struct TriggeredAssertion {
+	int step;
+	SimInstance *instance;
+	Cell *cell;
+
+	TriggeredAssertion(int step, SimInstance *instance, Cell *cell) :
+		step(step), instance(instance), cell(cell)
+	{ }
+};
+
 struct SimShared
 {
 	bool debug = false;
@@ -95,6 +107,8 @@ struct SimShared
 	bool date = false;
 	bool multiclock = false;
 	int next_output_id = 0;
+	int step = 0;
+	std::vector<TriggeredAssertion> triggered_assertions;
 };
 
 void zinit(State &v)
@@ -161,6 +175,7 @@ struct SimInstance
 
 	dict<Wire*, pair<int, Const>> signal_database;
 	dict<IdString, std::map<int, pair<int, Const>>> trace_mem_database;
+	dict<std::pair<IdString, int>, Const> trace_mem_init_database;
 	dict<Wire*, fstHandle> fst_handles;
 	dict<Wire*, fstHandle> fst_inputs;
 	dict<IdString, dict<int,fstHandle>> fst_memories;
@@ -306,6 +321,21 @@ struct SimInstance
 		return log_id(module->name);
 	}
 
+	vector<std::string> witness_full_path() const
+	{
+		if (instance != nullptr)
+			return parent->witness_full_path(instance);
+		return vector<std::string>();
+	}
+
+	vector<std::string> witness_full_path(Cell *cell) const
+	{
+		auto result = witness_full_path();
+		auto cell_path = witness_path(cell);
+		result.insert(result.end(), cell_path.begin(), cell_path.end());
+		return result;
+	}
+
 	Const get_state(SigSpec sig)
 	{
 		Const value;
@@ -700,7 +730,11 @@ struct SimInstance
 				State a = get_state(cell->getPort(ID::A))[0];
 				State en = get_state(cell->getPort(ID::EN))[0];
 
-				if (cell->type == ID($cover) && en == State::S1 && a != State::S1)
+				if (en == State::S1 && (cell->type == ID($cover) ? a == State::S1 : a != State::S1)) {
+					shared->triggered_assertions.emplace_back(shared->step, this, cell);
+				}
+
+				if (cell->type == ID($cover) && en == State::S1 && a == State::S1)
 					log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str());
 
 				if (cell->type == ID($assume) && en == State::S1 && a != State::S1)
@@ -875,6 +909,10 @@ struct SimInstance
 		int output_id = shared->next_output_id++;
 		Const data;
 		if (!shared->output_data.empty()) {
+			auto init_it = trace_mem_init_database.find(std::make_pair(memid, addr));
+			if (init_it != trace_mem_init_database.end())
+				data = init_it->second;
+			else
 				data = mem.get_init_data().extract(index * mem.width, mem.width);
 			shared->output_data.front().second.emplace(output_id, data);
 		}
@@ -1060,6 +1098,7 @@ struct SimWorker : SimShared
 	std::string timescale;
 	std::string sim_filename;
 	std::string map_filename;
+	std::string summary_filename;
 	std::string scope;
 
 	~SimWorker()
@@ -1103,6 +1142,9 @@ struct SimWorker : SimShared
 
 	void update(bool gclk)
 	{
+		if (gclk)
+			step += 1;
+
 		while (1)
 		{
 			if (debug)
@@ -1130,7 +1172,7 @@ struct SimWorker : SimShared
 		top->update_ph1();
 		if (debug)
 			log("\n-- ph3 (initialize) --\n");
-		top->update_ph3(false);
+		top->update_ph3(true);
 	}
 
 	void set_inports(pool<IdString> ports, State value)
@@ -1709,7 +1751,10 @@ struct SimWorker : SimShared
 						SigChunk(found_path.wire, signal.offset, signal.width),
 						value);
 			} else if (!found_path.memid.empty()) {
+				if (t >= 1)
 					found_path.instance->register_memory_addr(found_path.memid, found_path.addr);
+				else
+					found_path.instance->trace_mem_init_database.emplace(make_pair(found_path.memid, found_path.addr), value);
 				found_path.instance->set_memory_state(
 						found_path.memid, found_path.addr,
 						value);
@@ -1793,6 +1838,37 @@ struct SimWorker : SimShared
 		write_output_files();
 	}
 
+	void write_summary()
+	{
+		if (summary_filename.empty())
+			return;
+
+		PrettyJson json;
+		if (!json.write_to_file(summary_filename))
+			log_error("Can't open file `%s' for writing: %s\n", summary_filename.c_str(), strerror(errno));
+
+		json.begin_object();
+		json.entry("version", "Yosys sim summary");
+		json.entry("generator", yosys_version_str);
+		json.entry("steps", step);
+		json.entry("top", log_id(top->module->name));
+		json.name("assertions");
+		json.begin_array();
+		for (auto &assertion : triggered_assertions) {
+			json.begin_object();
+			json.entry("step", assertion.step);
+			json.entry("type", log_id(assertion.cell->type));
+			json.entry("path", assertion.instance->witness_full_path(assertion.cell));
+			auto src = assertion.cell->get_string_attribute(ID::src);
+			if (!src.empty()) {
+				json.entry("src", src);
+			}
+			json.end_object();
+		}
+		json.end_array();
+		json.end_object();
+	}
+
 	std::string define_signal(Wire *wire)
 	{
 		std::stringstream f;
@@ -2330,6 +2406,9 @@ struct SimPass : public Pass {
 		log("    -append <integer>\n");
 		log("        number of extra clock cycles to simulate for a Yosys witness input\n");
 		log("\n");
+		log("    -summary <filename>\n");
+		log("        write a JSON summary to the given file\n");
+		log("\n");
 		log("    -map <filename>\n");
 		log("        read file with port and latch symbols, needed for AIGER witness input\n");
 		log("\n");
@@ -2469,6 +2548,12 @@ struct SimPass : public Pass {
 				worker.map_filename = map_filename;
 				continue;
 			}
+			if (args[argidx] == "-summary" && argidx+1 < args.size()) {
+				std::string summary_filename = args[++argidx];
+				rewrite_filename(summary_filename);
+				worker.summary_filename = summary_filename;
+				continue;
+			}
 			if (args[argidx] == "-scope" && argidx+1 < args.size()) {
 				worker.scope = args[++argidx];
 				continue;
@@ -2558,6 +2643,8 @@ struct SimPass : public Pass {
 				log_cmd_error("Unhandled extension for simulation input file `%s`.\n", worker.sim_filename.c_str());
 			}
 		}
+
+		worker.write_summary();
 	}
 } SimPass;