aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--backends/aiger/aiger.cc13
-rw-r--r--backends/btor/btor.cc13
-rw-r--r--backends/smt2/witness.py71
-rw-r--r--kernel/yw.cc2
-rw-r--r--kernel/yw.h12
-rw-r--r--passes/sat/sim.cc95
6 files changed, 154 insertions, 52 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:
diff --git a/kernel/yw.cc b/kernel/yw.cc
index 4a6e37a13..73e7710db 100644
--- a/kernel/yw.cc
+++ b/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);
}
diff --git a/kernel/yw.h b/kernel/yw.h
index 8b651fd83..503319b1d 100644
--- a/kernel/yw.h
+++ b/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 {
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index af3a38be8..1dd406f22 100644
--- a/passes/sat/sim.cc
+++ b/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,7 +909,11 @@ struct SimInstance
int output_id = shared->next_output_id++;
Const data;
if (!shared->output_data.empty()) {
- data = mem.get_init_data().extract(index * mem.width, mem.width);
+ 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);
}
trace_mem_database[memid].emplace(index, make_pair(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()) {
- found_path.instance->register_memory_addr(found_path.memid, found_path.addr);
+ 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;
generated by cgit v1.2.3 (git 2.25.1) at 2024-09-29 21:59:52 +0000