aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--backends/aiger/aiger.cc111
-rw-r--r--backends/btor/btor.cc164
-rw-r--r--backends/smt2/smt2.cc9
-rw-r--r--backends/smt2/witness.py156
-rw-r--r--backends/smt2/ywio.py5
-rw-r--r--kernel/constids.inc1
-rw-r--r--kernel/json.cc172
-rw-r--r--kernel/json.h104
-rw-r--r--kernel/yw.cc209
-rw-r--r--kernel/yw.h182
-rw-r--r--passes/cmds/setundef.cc10
-rw-r--r--passes/cmds/xprop.cc3
-rw-r--r--passes/sat/formalff.cc216
-rw-r--r--passes/sat/sim.cc491
15 files changed, 1722 insertions, 113 deletions
diff --git a/Makefile b/Makefile
index 2a05fcc50..dbaf9e2b0 100644
--- a/Makefile
+++ b/Makefile
@@ -653,7 +653,7 @@ ifneq ($(ABCEXTERNAL),)
kernel/yosys.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"'
endif
endif
-OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o
+OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o kernel/yw.o kernel/json.o
ifeq ($(ENABLE_ZLIB),1)
OBJS += kernel/fstdata.o
endif
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 513f9d95a..4ef28be9f 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -19,6 +19,8 @@
#include "kernel/yosys.h"
#include "kernel/sigtools.h"
+#include "kernel/json.h"
+#include "kernel/yw.h"
#include "libs/json11/json11.hpp"
USING_YOSYS_NAMESPACE
@@ -709,30 +711,19 @@ 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(std::ostream &f)
+ void write_ywmap(PrettyJson &json)
{
- f << "{\n";
- f << " \"version\": \"Yosys Witness Aiger Map\",\n";
- f << stringf(" \"generator\": %s,\n", json11::Json(yosys_version_str).dump().c_str());
- f << stringf(" \"latch_count\": %d,\n", aig_l);
- f << stringf(" \"input_count\": %d,\n", aig_i);
+ json.begin_object();
+ json.entry("version", "Yosys Witness Aiger map");
+ json.entry("gennerator", yosys_version_str);
- dict<int, string> clock_lines;
- dict<int, string> input_lines;
- dict<int, string> init_lines;
- dict<int, string> seq_lines;
+ json.entry("latch_count", aig_l);
+ json.entry("input_count", aig_i);
+
+ dict<int, Json> clock_lines;
+ dict<int, Json> input_lines;
+ dict<int, Json> init_lines;
+ dict<int, Json> seq_lines;
for (auto cell : module->cells())
{
@@ -751,21 +742,21 @@ struct AigerWriter
if (init_inputs.count(sig[i])) {
int a = init_inputs.at(sig[i]);
log_assert((a & 1) == 0);
- init_lines[a] += json11::Json(json11::Json::object {
+ init_lines[a] = json11::Json(json11::Json::object {
{ "path", witness_path(wire) },
{ "input", (a >> 1) - 1 },
{ "offset", sig_qy[i].offset },
- }).dump();
+ });
}
if (input_bits.count(sig[i])) {
int a = aig_map.at(sig[i]);
log_assert((a & 1) == 0);
- seq_lines[a] += json11::Json(json11::Json::object {
+ seq_lines[a] = json11::Json(json11::Json::object {
{ "path", witness_path(wire) },
{ "input", (a >> 1) - 1 },
{ "offset", sig_qy[i].offset },
- }).dump();
+ });
}
}
}
@@ -783,60 +774,55 @@ struct AigerWriter
int a = aig_map.at(sig[i]);
log_assert((a & 1) == 0);
- input_lines[a] += json11::Json(json11::Json::object {
+ input_lines[a] = json11::Json(json11::Json::object {
{ "path", path },
{ "input", (a >> 1) - 1 },
{ "offset", i },
- }).dump();
+ });
if (ywmap_clocks.count(sig[i])) {
int clock_mode = ywmap_clocks[sig[i]];
if (clock_mode != 3) {
- clock_lines[a] += json11::Json(json11::Json::object {
+ clock_lines[a] = json11::Json(json11::Json::object {
{ "path", path },
{ "input", (a >> 1) - 1 },
{ "offset", i },
{ "edge", clock_mode == 1 ? "posedge" : "negedge" },
- }).dump();
+ });
}
}
}
}
}
- f << " \"clocks\": [";
+ json.name("clocks");
+ json.begin_array();
clock_lines.sort();
- const char *sep = "\n ";
- for (auto &it : clock_lines) {
- f << sep << it.second;
- sep = ",\n ";
- }
- f << "\n ],\n";
+ for (auto &it : clock_lines)
+ json.value(it.second);
+ json.end_array();
- f << " \"inputs\": [";
+ json.name("inputs");
+ json.begin_array();
input_lines.sort();
- sep = "\n ";
- for (auto &it : input_lines) {
- f << sep << it.second;
- sep = ",\n ";
- }
- f << "\n ],\n";
+ for (auto &it : input_lines)
+ json.value(it.second);
+ json.end_array();
- f << " \"seqs\": [";
- sep = "\n ";
- for (auto &it : seq_lines) {
- f << sep << it.second;
- sep = ",\n ";
- }
- f << "\n ],\n";
+ json.name("seqs");
+ json.begin_array();
+ input_lines.sort();
+ for (auto &it : seq_lines)
+ json.value(it.second);
+ json.end_array();
- f << " \"inits\": [";
- sep = "\n ";
- for (auto &it : init_lines) {
- f << sep << it.second;
- sep = ",\n ";
- }
- f << "\n ]\n}\n";
+ json.name("inits");
+ json.begin_array();
+ input_lines.sort();
+ for (auto &it : init_lines)
+ json.value(it.second);
+ json.end_array();
+ json.end_object();
}
};
@@ -991,9 +977,12 @@ struct AigerBackend : public Backend {
if (!yw_map_filename.empty()) {
std::ofstream mapf;
mapf.open(yw_map_filename.c_str(), std::ofstream::trunc);
- if (mapf.fail())
- log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
- writer.write_ywmap(mapf);
+
+ PrettyJson json;
+
+ if (!json.write_to_file(yw_map_filename))
+ log_error("Can't open file `%s' for writing: %s\n", yw_map_filename.c_str(), strerror(errno));
+ writer.write_ywmap(json);
}
}
} AigerBackend;
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 8368ab82d..4c43e91e7 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -28,6 +28,8 @@
#include "kernel/celltypes.h"
#include "kernel/log.h"
#include "kernel/mem.h"
+#include "kernel/json.h"
+#include "kernel/yw.h"
#include <string>
USING_YOSYS_NAMESPACE
@@ -83,6 +85,22 @@ struct BtorWorker
vector<string> info_lines;
dict<int, int> info_clocks;
+ struct ywmap_btor_sig {
+ SigSpec sig;
+ Cell *cell = nullptr;
+
+ ywmap_btor_sig(const SigSpec &sig) : sig(sig) {}
+ ywmap_btor_sig(Cell *cell) : cell(cell) {}
+ };
+
+ vector<ywmap_btor_sig> ywmap_inputs;
+ vector<ywmap_btor_sig> ywmap_states;
+ dict<SigBit, int> ywmap_clock_bits;
+ dict<SigBit, int> ywmap_clock_inputs;
+
+
+ PrettyJson ywmap_json;
+
void btorf(const char *fmt, ...) YS_ATTRIBUTE(format(printf, 2, 3))
{
va_list ap;
@@ -126,6 +144,50 @@ struct BtorWorker
return " " + infostr;
}
+ void ywmap_state(const SigSpec &sig) {
+ if (ywmap_json.active())
+ ywmap_states.emplace_back(sig);
+ }
+
+ void ywmap_state(Cell *cell) {
+ if (ywmap_json.active())
+ ywmap_states.emplace_back(cell);
+ }
+
+ void ywmap_input(const SigSpec &sig) {
+ if (ywmap_json.active())
+ ywmap_inputs.emplace_back(sig);
+ }
+
+ void emit_ywmap_btor_sig(const ywmap_btor_sig &btor_sig) {
+ if (btor_sig.cell == nullptr) {
+ if (btor_sig.sig.empty()) {
+ ywmap_json.value(nullptr);
+ return;
+ }
+ ywmap_json.begin_array();
+ ywmap_json.compact();
+ for (auto &chunk : btor_sig.sig.chunks()) {
+ log_assert(chunk.is_wire());
+
+ ywmap_json.begin_object();
+ ywmap_json.entry("path", witness_path(chunk.wire));
+ ywmap_json.entry("width", chunk.width);
+ ywmap_json.entry("offset", chunk.offset);
+ ywmap_json.end_object();
+ }
+ ywmap_json.end_array();
+ } else {
+ ywmap_json.begin_object();
+ ywmap_json.compact();
+ ywmap_json.entry("path", witness_path(btor_sig.cell));
+ Mem *mem = mem_cells[btor_sig.cell];
+ ywmap_json.entry("width", mem->width);
+ ywmap_json.entry("size", mem->size);
+ ywmap_json.end_object();
+ }
+ }
+
void btorf_push(const string &id)
{
if (verbose) {
@@ -617,7 +679,7 @@ struct BtorWorker
SigSpec sig_d = sigmap(cell->getPort(ID::D));
SigSpec sig_q = sigmap(cell->getPort(ID::Q));
- if (!info_filename.empty() && cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)))
+ if ((!info_filename.empty() || ywmap_json.active()) && cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)))
{
SigSpec sig_c = sigmap(cell->getPort(cell->type == ID($dff) ? ID::CLK : ID::C));
int nid = get_sig_nid(sig_c);
@@ -629,7 +691,11 @@ struct BtorWorker
if (cell->type == ID($dff) && !cell->getParam(ID::CLK_POLARITY).as_bool())
negedge = true;
- info_clocks[nid] |= negedge ? 2 : 1;
+ if (!info_filename.empty())
+ info_clocks[nid] |= negedge ? 2 : 1;
+
+ if (ywmap_json.active())
+ ywmap_clock_bits[sig_c] |= negedge ? 2 : 1;
}
IdString symbol;
@@ -662,6 +728,8 @@ struct BtorWorker
else
btorf("%d state %d %s\n", nid, sid, log_id(symbol));
+ ywmap_state(sig_q);
+
if (nid_init_val >= 0) {
int nid_init = next_nid++;
if (verbose)
@@ -683,6 +751,8 @@ struct BtorWorker
btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str());
+ ywmap_state(sig_y);
+
if (cell->type == ID($anyconst)) {
int nid2 = next_nid++;
btorf("%d next %d %d %d\n", nid2, sid, nid, nid);
@@ -705,6 +775,8 @@ struct BtorWorker
btorf("%d state %d%s\n", initstate_nid, sid, getinfo(cell).c_str());
btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid);
+
+ ywmap_state(sig_y);
}
add_nid_sig(initstate_nid, sig_y);
@@ -768,6 +840,8 @@ struct BtorWorker
nid_init_val = next_nid++;
btorf("%d state %d\n", nid_init_val, sid);
+ ywmap_state(nullptr);
+
for (int i = 0; i < mem->size; i++) {
Const thisword = initdata.extract(i*mem->width, mem->width);
if (thisword.is_fully_undef())
@@ -793,6 +867,8 @@ struct BtorWorker
else
btorf("%d state %d %s\n", nid, sid, log_id(mem->memid));
+ ywmap_state(cell);
+
if (nid_init_val >= 0)
{
int nid_init = next_nid++;
@@ -915,10 +991,13 @@ struct BtorWorker
int sid = get_bv_sid(GetSize(sig));
int nid_input = next_nid++;
- if (is_init)
+ if (is_init) {
btorf("%d state %d\n", nid_input, sid);
- else
+ ywmap_state(sig);
+ } else {
btorf("%d input %d\n", nid_input, sid);
+ ywmap_input(sig);
+ }
int nid_masked_input;
if (sig_mask_undef.is_fully_ones()) {
@@ -993,6 +1072,7 @@ struct BtorWorker
int sid = get_bv_sid(GetSize(s));
int nid = next_nid++;
btorf("%d input %d\n", nid, sid);
+ ywmap_input(s);
nid_width[nid] = GetSize(s);
for (int j = 0; j < GetSize(s); j++)
@@ -1075,12 +1155,15 @@ struct BtorWorker
return nid;
}
- BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad, bool cover_mode, bool print_internal_names, string info_filename) :
+ BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad, bool cover_mode, bool print_internal_names, string info_filename, string ywmap_filename) :
f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad), cover_mode(cover_mode), print_internal_names(print_internal_names), info_filename(info_filename)
{
if (!info_filename.empty())
infof("name %s\n", log_id(module));
+ if (!ywmap_filename.empty())
+ ywmap_json.write_to_file(ywmap_filename);
+
memories = Mem::get_all_memories(module);
dict<IdString, Mem*> mem_dict;
@@ -1094,6 +1177,20 @@ struct BtorWorker
btorf_push("inputs");
+ if (ywmap_json.active()) {
+ for (auto wire : module->wires())
+ {
+ auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
+ if (gclk_attr == wire->attributes.end())
+ continue;
+ SigSpec sig = sigmap(wire);
+ if (gclk_attr->second == State::S1)
+ ywmap_clock_bits[sig] |= 1;
+ else if (gclk_attr->second == State::S0)
+ ywmap_clock_bits[sig] |= 2;
+ }
+ }
+
for (auto wire : module->wires())
{
if (wire->attributes.count(ID::init)) {
@@ -1111,6 +1208,7 @@ struct BtorWorker
int nid = next_nid++;
btorf("%d input %d%s\n", nid, sid, getinfo(wire).c_str());
+ ywmap_input(wire);
add_nid_sig(nid, sig);
if (!info_filename.empty()) {
@@ -1122,6 +1220,16 @@ struct BtorWorker
info_clocks[nid] |= 2;
}
}
+
+ if (ywmap_json.active()) {
+ for (int i = 0; i < GetSize(sig); i++) {
+ auto input_bit = SigBit(wire, i);
+ auto bit = sigmap(input_bit);
+ if (!ywmap_clock_bits.count(bit))
+ continue;
+ ywmap_clock_inputs[input_bit] = ywmap_clock_bits[bit];
+ }
+ }
}
btorf_pop("inputs");
@@ -1378,6 +1486,42 @@ struct BtorWorker
f << it;
f.close();
}
+
+ if (ywmap_json.active())
+ {
+ ywmap_json.begin_object();
+ ywmap_json.entry("version", "Yosys Witness BTOR map");
+ ywmap_json.entry("generator", yosys_version_str);
+
+ ywmap_json.name("clocks");
+ ywmap_json.begin_array();
+ for (auto &entry : ywmap_clock_inputs) {
+ if (entry.second != 1 && entry.second != 2)
+ continue;
+ log_assert(entry.first.is_wire());
+ ywmap_json.begin_object();
+ ywmap_json.compact();
+ ywmap_json.entry("path", witness_path(entry.first.wire));
+ ywmap_json.entry("offset", entry.first.offset);
+ ywmap_json.entry("edge", entry.second == 1 ? "posedge" : "negedge");
+ ywmap_json.end_object();
+ }
+ ywmap_json.end_array();
+
+ ywmap_json.name("inputs");
+ ywmap_json.begin_array();
+ for (auto &entry : ywmap_inputs)
+ emit_ywmap_btor_sig(entry);
+ ywmap_json.end_array();
+
+ ywmap_json.name("states");
+ ywmap_json.begin_array();
+ for (auto &entry : ywmap_states)
+ emit_ywmap_btor_sig(entry);
+ ywmap_json.end_array();
+
+ ywmap_json.end_object();
+ }
}
};
@@ -1406,11 +1550,15 @@ struct BtorBackend : public Backend {
log(" -x\n");
log(" Output symbols for internal netnames (starting with '$')\n");
log("\n");
+ log(" -ywmap <filename>\n");
+ log(" Create a map file for conversion to and from Yosys witness traces\n");
+ log("\n");
}
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
{
bool verbose = false, single_bad = false, cover_mode = false, print_internal_names = false;
string info_filename;
+ string ywmap_filename;
log_header(design, "Executing BTOR backend.\n");
@@ -1443,6 +1591,10 @@ struct BtorBackend : public Backend {
print_internal_names = true;
continue;
}
+ if (args[argidx] == "-ywmap" && argidx+1 < args.size()) {
+ ywmap_filename = args[++argidx];
+ continue;
+ }
break;
}
extra_args(f, filename, args, argidx);
@@ -1455,7 +1607,7 @@ struct BtorBackend : public Backend {
*f << stringf("; BTOR description generated by %s for module %s.\n",
yosys_version_str, log_id(topmod));
- BtorWorker(*f, topmod, verbose, single_bad, cover_mode, print_internal_names, info_filename);
+ BtorWorker(*f, topmod, verbose, single_bad, cover_mode, print_internal_names, info_filename, ywmap_filename);
*f << stringf("; end of yosys output\n");
}
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index fe50ca7f6..1ab39a405 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -458,7 +458,7 @@ struct Smt2Worker
{
RTLIL::SigSpec sig_a, sig_b;
RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y));
- bool is_signed = cell->getParam(ID::A_SIGNED).as_bool();
+ bool is_signed = type == 'U' ? false : cell->getParam(ID::A_SIGNED).as_bool();
int width = GetSize(sig_y);
if (type == 's' || type == 'S' || type == 'd' || type == 'b') {
@@ -483,6 +483,7 @@ struct Smt2Worker
if (ch == 'A') processed_expr += get_bv(sig_a);
else if (ch == 'B') processed_expr += get_bv(sig_b);
else if (ch == 'P') processed_expr += get_bv(cell->getPort(ID::B));
+ else if (ch == 'S') processed_expr += get_bv(cell->getPort(ID::S));
else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
else processed_expr += ch;
@@ -639,6 +640,9 @@ struct Smt2Worker
if (cell->type == ID($xor)) return export_bvop(cell, "(bvxor A B)");
if (cell->type == ID($xnor)) return export_bvop(cell, "(bvxnor A B)");
+ if (cell->type == ID($bweqx)) return export_bvop(cell, "(bvxnor A B)", 'U');
+ if (cell->type == ID($bwmux)) return export_bvop(cell, "(bvor (bvand A (bvnot S)) (bvand B S))", 'U');
+
if (cell->type == ID($shl)) return export_bvop(cell, "(bvshl A B)", 's');
if (cell->type == ID($shr)) return export_bvop(cell, "(bvlshr A B)", 's');
if (cell->type == ID($sshl)) return export_bvop(cell, "(bvshl A B)", 's');
@@ -994,7 +998,7 @@ struct Smt2Worker
if (contains_clock && GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
- if (contains_clock) {
+ if (wire->port_input && contains_clock) {
for (int i = 0; i < GetSize(sig); i++) {
bool is_posedge = clock_posedge.count(sig[i]);
bool is_negedge = clock_negedge.count(sig[i]);
@@ -1744,7 +1748,6 @@ struct Smt2Backend : public Backend {
log_push();
Pass::call(design, "bmuxmap");
Pass::call(design, "demuxmap");
- Pass::call(design, "bwmuxmap");
log_pop();
size_t argidx;
diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py
index a1e65569d..8d0cc8112 100644
--- a/backends/smt2/witness.py
+++ b/backends/smt2/witness.py
@@ -110,6 +110,10 @@ class AigerMap:
def __init__(self, mapfile):
data = json.load(mapfile)
+ version = data.get("version") if isinstance(data, dict) else {}
+ if version != "Yosys Witness Aiger map":
+ raise click.ClickException(f"{mapfile.name}: unexpected file format version {version!r}")
+
self.latch_count = data["latch_count"]
self.input_count = data["input_count"]
@@ -250,5 +254,157 @@ def yw2aiw(input, mapfile, output):
click.echo(f"Converted {len(inyw)} time steps.")
+class BtorMap:
+ def __init__(self, mapfile):
+ self.data = data = json.load(mapfile)
+
+ version = data.get("version") if isinstance(data, dict) else {}
+ if version != "Yosys Witness BTOR map":
+ raise click.ClickException(f"{mapfile.name}: unexpected file format version {version!r}")
+
+ self.sigmap = WitnessSigMap()
+
+ for mode in ("states", "inputs"):
+ for btor_signal_def in data[mode]:
+ if btor_signal_def is None:
+ continue
+ if isinstance(btor_signal_def, dict):
+ btor_signal_def["path"] = tuple(btor_signal_def["path"])
+ else:
+ for chunk in btor_signal_def:
+ chunk["path"] = tuple(chunk["path"])
+
+
+@cli.command(help="""
+Convert a BTOR witness trace into a Yosys witness trace.
+
+This requires a Yosys witness BTOR map file as generated by 'write_btor -ywmap'.
+""")
+@click.argument("input", type=click.File("r"))
+@click.argument("mapfile", type=click.File("r"))
+@click.argument("output", type=click.File("w"))
+def wit2yw(input, mapfile, output):
+ input_name = input.name
+ click.echo(f"Converting BTOR witness trace {input_name!r} to Yosys witness trace {output.name!r}...")
+ click.echo(f"Using Yosys witness BTOR map file {mapfile.name!r}")
+ btor_map = BtorMap(mapfile)
+
+ input = filter(None, (line.split(';', 1)[0].strip() for line in input))
+
+ sat = next(input, None)
+ if sat != "sat":
+ raise click.ClickException(f"{input_name}: not a BTOR witness file")
+
+ props = next(input, None)
+
+ t = -1
+
+ line = next(input, None)
+
+ frames = []
+ bits = {}
+
+ while line and not line.startswith('.'):
+ current_t = int(line[1:].strip())
+ if line[0] == '#':
+ mode = "states"
+ elif line[0] == '@':
+ mode = "inputs"
+ else:
+ raise click.ClickException(f"{input_name}: unexpected data in BTOR witness file")
+
+ if current_t > t:
+ t = current_t
+ values = WitnessValues()
+ array_inits = set()
+ frames.append(values)
+
+ line = next(input, None)
+ while line and line[0] not in "#@.":
+ if current_t > 0 and mode == "states":
+ line = next(input, None)
+ continue
+ tokens = line.split()
+ 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('['):
+ addr = '[*]'
+ value = tokens[1]
+ else:
+ value = tokens[2]
+ if not addr.endswith(']'):
+ raise click.ClickException(f"{input_name}: expected address in BTOR witness file")
+ 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]
+
+ for btor_sig in btor_sigs:
+ value_bits = iter(reversed(value))
+
+ 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)
+
+ if next(value_bits, None) is not None:
+ raise click.ClickException(f"{input_name}: excess bits in BTOR witness file")
+
+
+ if line is None:
+ raise click.ClickException(f"{input_name}: unexpected end of BTOR witness file")
+ if line.strip() != '.':
+ raise click.ClickException(f"{input_name}: unexpected data in BTOR witness file")
+ if next(input, None) is not None:
+ raise click.ClickException(f"{input_name}: unexpected trailing data in BTOR witness file")
+
+ outyw = WriteWitness(output, 'yosys-witness wit2yw')
+
+ outyw.signals = coalesce_signals((), bits)
+ for clock in btor_map.data["clocks"]:
+ outyw.add_clock(clock["path"], clock["offset"], clock["edge"])
+
+ for values in frames:
+ outyw.step(values)
+
+ outyw.end_trace()
+ click.echo(f"Converted {outyw.t} time steps.")
+
if __name__ == "__main__":
cli()
diff --git a/backends/smt2/ywio.py b/backends/smt2/ywio.py
index 8469b4162..39cfac41e 100644
--- a/backends/smt2/ywio.py
+++ b/backends/smt2/ywio.py
@@ -175,8 +175,9 @@ class WitnessSig:
return self.sort_key < other.sort_key
-def coalesce_signals(signals):
- bits = {}
+def coalesce_signals(signals, bits=None):
+ if bits is None:
+ bits = {}
for sig in signals:
for bit in sig.bits():
if sig.init_only:
diff --git a/kernel/constids.inc b/kernel/constids.inc
index 239381f85..39211d0c7 100644
--- a/kernel/constids.inc
+++ b/kernel/constids.inc
@@ -259,5 +259,6 @@ X(WR_PORTS)
X(WR_PRIORITY_MASK)
X(WR_WIDE_CONTINUATION)
X(X)
+X(xprop_decoder)
X(Y)
X(Y_WIDTH)
diff --git a/kernel/json.cc b/kernel/json.cc
new file mode 100644
index 000000000..738746267
--- /dev/null
+++ b/kernel/json.cc
@@ -0,0 +1,172 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/json.h"
+
+USING_YOSYS_NAMESPACE
+
+void PrettyJson::emit_to_log()
+{
+ struct LogTarget : public Target {
+ void emit(const char *data) override { log("%s", data); }
+ };
+
+ targets.push_back(std::unique_ptr<Target>(new LogTarget));
+}
+
+void PrettyJson::append_to_string(std::string &target)
+{
+ struct AppendStringTarget : public Target {
+ std::string &target;
+ AppendStringTarget(std::string &target) : target(target) {}
+ void emit(const char *data) override { target += data; }
+ };
+
+ targets.push_back(std::unique_ptr<Target>(new AppendStringTarget(target)));
+}
+
+bool PrettyJson::write_to_file(const std::string &path)
+{
+ struct WriteFileTarget : public Target {
+ std::ofstream target;
+ void emit(const char *data) override { target << data; }
+ void flush() override { target.flush(); }
+ };
+
+ auto target = std::unique_ptr<WriteFileTarget>(new WriteFileTarget);
+ target->target.open(path);
+ if (target->target.fail())
+ return false;
+ targets.push_back(std::unique_ptr<Target>(target.release()));
+ return true;
+}
+
+void PrettyJson::line(bool space_if_inline)
+{
+ if (compact_depth != INT_MAX) {
+ if (space_if_inline)
+ raw(" ");
+ return;
+ }
+ int indent = state.size() - (state.empty() ? 0 : state.back() == VALUE);
+ newline_indent.resize(1 + 2 * indent, ' ');
+ raw(newline_indent.c_str());
+}
+
+void PrettyJson::raw(const char *raw_json)
+{
+ for (auto &target : targets)
+ target->emit(raw_json);
+}
+
+void PrettyJson::flush()
+{
+ for (auto &target : targets)
+ target->flush();
+}
+
+void PrettyJson::begin_object()
+{
+ begin_value();
+ raw("{");
+ state.push_back(OBJECT_FIRST);
+}
+
+void PrettyJson::begin_array()
+{
+ begin_value();
+ raw("[");
+ state.push_back(ARRAY_FIRST);
+}
+
+void PrettyJson::end_object()
+{
+ Scope top_scope = state.back();
+ state.pop_back();
+ if (top_scope == OBJECT)
+ line(false);
+ else
+ log_assert(top_scope == OBJECT_FIRST);
+ raw("}");
+ end_value();
+}
+
+void PrettyJson::end_array()
+{
+ Scope top_scope = state.back();
+ state.pop_back();
+ if (top_scope == ARRAY)
+ line(false);
+ else
+ log_assert(top_scope == ARRAY_FIRST);
+ raw("]");
+ end_value();
+}
+
+void PrettyJson::name(const char *name)
+{
+ if (state.back() == OBJECT_FIRST) {
+ state.back() = OBJECT;
+ line(false);
+ } else {
+ raw(",");
+ line();
+ }
+ raw(Json(name).dump().c_str());
+ raw(": ");
+ state.push_back(VALUE);
+}
+
+void PrettyJson::begin_value()
+{
+ if (state.back() == ARRAY_FIRST) {
+ line(false);
+ state.back() = ARRAY;
+ } else if (state.back() == ARRAY) {
+ raw(",");
+ line();
+ } else {
+ log_assert(state.back() == VALUE);
+ state.pop_back();
+ }
+}
+
+void PrettyJson::end_value()
+{
+ if (state.empty()) {
+ raw("\n");
+ flush();
+ }
+ if (GetSize(state) < compact_depth)
+ compact_depth = INT_MAX;
+}
+
+void PrettyJson::value_json(const Json &value)
+{
+ begin_value();
+ raw(value.dump().c_str());
+ end_value();
+}
+
+void PrettyJson::entry_json(const char *name, const Json &value)
+{
+ this->name(name);
+ this->value(value);
+}
+
diff --git a/kernel/json.h b/kernel/json.h
new file mode 100644
index 000000000..c9aa0e045
--- /dev/null
+++ b/kernel/json.h
@@ -0,0 +1,104 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#ifndef JSON_H
+#define JSON_H
+
+#include "kernel/yosys.h"
+#include "libs/json11/json11.hpp"
+#include <functional>
+
+YOSYS_NAMESPACE_BEGIN
+
+using json11::Json;
+
+class PrettyJson
+{
+ enum Scope {
+ VALUE,
+ OBJECT_FIRST,
+ OBJECT,
+ ARRAY_FIRST,
+ ARRAY,
+ };
+
+ struct Target {
+ virtual void emit(const char *data) = 0;
+ virtual void flush() {};
+ virtual ~Target() {};
+ };
+
+ std::string newline_indent = "\n";
+ std::vector<std::unique_ptr<Target>> targets;
+ std::vector<Scope> state = {VALUE};
+ int compact_depth = INT_MAX;
+public:
+
+ void emit_to_log();
+ void append_to_string(std::string &target);
+ bool write_to_file(const std::string &path);
+
+ bool active() { return !targets.empty(); }
+
+ void compact() { compact_depth = GetSize(state); }
+
+ void line(bool space_if_inline = true);
+ void raw(const char *raw_json);
+ void flush();
+ void begin_object();
+ void begin_array();
+ void end_object();
+ void end_array();
+ void name(const char *name);
+ void begin_value();
+ void end_value();
+ void value_json(const Json &value);
+ void value(unsigned int value) { value_json(Json((int)value)); }
+ template<typename T>
+ void value(T &&value) { value_json(Json(std::forward<T>(value))); };
+
+ void entry_json(const char *name, const Json &value);
+ void entry(const char *name, unsigned int value) { entry_json(name, Json((int)value)); }
+ template<typename T>
+ void entry(const char *name, T &&value) { entry_json(name, Json(std::forward<T>(value))); };
+
+ template<typename T>
+ void object(const T &&values)
+ {
+ begin_object();
+ for (auto &item : values)
+ entry(item.first, item.second);
+ end_object();
+ }
+
+ template<typename T>
+ void array(const T &&values)
+ {
+ begin_object();
+ for (auto &item : values)
+ value(item);
+ end_object();
+ }
+};
+
+
+
+YOSYS_NAMESPACE_END
+
+#endif
diff --git a/kernel/yw.cc b/kernel/yw.cc
new file mode 100644
index 000000000..73e7710db
--- /dev/null
+++ b/kernel/yw.cc
@@ -0,0 +1,209 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/yw.h"
+#include "libs/json11/json11.hpp"
+
+USING_YOSYS_NAMESPACE
+
+// Use the same formatting as witness.py uses
+static const char *pretty_name(IdString id)
+{
+ const char *c_str = id.c_str();
+ const char *p = c_str;
+
+ if (*p != '\\')
+ return c_str;
+ p++;
+
+ if (*p == '[') {
+ p++;
+ while (*p >= '0' && *p <= '9')
+ p++;
+ if (p[0] != ']' || p[1] != 0)
+ return c_str;
+ return c_str + 1;
+ }
+
+ if (!(*p >= 'a' && *p <= 'z') && !(*p >= 'A' && *p <= 'Z') && *p != '_')
+ return c_str;
+ p++;
+ while ((*p >= '0' && *p <= '9') || (*p >= 'a' && *p <= 'z') || (*p >= 'A' && *p <= 'Z') || *p == '_')
+ p++;
+
+ if (*p != 0)
+ return c_str;
+ return c_str + 1;
+}
+
+std::string IdPath::str() const
+{
+ std::string result;
+
+ for (auto &item : *this) {
+ const char *pretty = pretty_name(item);
+ if (pretty[0] == '[') {
+ result += pretty;
+ continue;
+ }
+ if (!result.empty())
+ result += '.';
+ result += pretty;
+ if (pretty[0] == '\\' || pretty[0] == '$')
+ result += ' ';
+ }
+
+ return result;
+}
+
+bool IdPath::get_address(int &addr) const
+{
+ if (empty())
+ return false;
+ auto &last = back();
+ if (!last.begins_with("\\["))
+ return false;
+ if (last == "\\[0]") {
+ addr = 0;
+ return true;
+ }
+ char first = last.c_str()[2];
+ if (first < '1' || first > '9')
+ return false;
+ char *endptr;
+ addr = std::strtol(last.c_str() + 2, &endptr, 10);
+ return endptr[0] == ']' && endptr[1] == 0;
+}
+
+static std::vector<IdString> get_path(const json11::Json &json)
+{
+ std::vector<IdString> result;
+ for (auto &path_item : json.array_items()) {
+ auto const &path_item_str = path_item.string_value();
+ if (path_item_str.empty())
+ return {};;
+ result.push_back(path_item_str);
+ }
+ return result;
+}
+
+ReadWitness::ReadWitness(const std::string &filename) :
+ filename(filename)
+{
+ std::ifstream f(filename.c_str());
+ if (f.fail() || GetSize(filename) == 0)
+ log_error("Cannot open file `%s`\n", filename.c_str());
+ std::stringstream buf;
+ buf << f.rdbuf();
+ std::string err;
+ json11::Json json = json11::Json::parse(buf.str(), err);
+ if (!err.empty())
+ log_error("Failed to parse `%s`: %s\n", filename.c_str(), err.c_str());
+
+ std::string format = json["format"].string_value();
+
+ if (format.empty())
+ log_error("Failed to parse `%s`: Unknown format\n", filename.c_str());
+ if (format != "Yosys Witness Trace")
+ log_error("Failed to parse `%s`: Unsupported format `%s`\n", filename.c_str(), format.c_str());
+
+ for (auto &clock_json : json["clocks"].array_items()) {
+ Clock clock;
+ clock.path = get_path(clock_json["path"]);
+ if (clock.path.empty())
+ log_error("Failed to parse `%s`: Missing path for clock `%s`\n", filename.c_str(), clock_json.dump().c_str());
+ auto edge_str = clock_json["edge"];
+ if (edge_str.string_value() == "posedge")
+ clock.is_posedge = true;
+ else if (edge_str.string_value() == "negedge")
+ clock.is_negedge = true;
+ else
+ log_error("Failed to parse `%s`: Unknown edge type for clock `%s`\n", filename.c_str(), clock_json.dump().c_str());
+ if (!clock_json["offset"].is_number())
+ log_error("Failed to parse `%s`: Unknown offset for clock `%s`\n", filename.c_str(), clock_json.dump().c_str());
+ clock.offset = clock_json["offset"].int_value();
+ if (clock.offset < 0)
+ log_error("Failed to parse `%s`: Invalid offset for clock `%s`\n", filename.c_str(), clock_json.dump().c_str());
+ clocks.push_back(clock);
+ }
+
+ int bits_offset = 0;
+ for (auto &signal_json : json["signals"].array_items()) {
+ Signal signal;
+ signal.bits_offset = bits_offset;
+ signal.path = get_path(signal_json["path"]);
+ if (signal.path.empty())
+ log_error("Failed to parse `%s`: Missing path for signal `%s`\n", filename.c_str(), signal_json.dump().c_str());
+ if (!signal_json["width"].is_number())
+ log_error("Failed to parse `%s`: Unknown width for signal `%s`\n", filename.c_str(), signal_json.dump().c_str());
+ signal.width = signal_json["width"].int_value();
+ if (signal.width < 0)
+ log_error("Failed to parse `%s`: Invalid width for signal `%s`\n", filename.c_str(), signal_json.dump().c_str());
+ bits_offset += signal.width;
+ if (!signal_json["offset"].is_number())
+ log_error("Failed to parse `%s`: Unknown offset for signal `%s`\n", filename.c_str(), signal_json.dump().c_str());
+ 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 = signal_json["init_only"].bool_value();
+ signals.push_back(signal);
+ }
+
+ for (auto &step_json : json["steps"].array_items()) {
+ Step step;
+ if (!step_json["bits"].is_string())
+ log_error("Failed to parse `%s`: Expected string as bits value for step %d\n", filename.c_str(), GetSize(steps));
+ step.bits = step_json["bits"].string_value();
+ for (char c : step.bits) {
+ if (c != '0' && c != '1' && c != 'x' && c != '?')
+ log_error("Failed to parse `%s`: Invalid bit '%c' value for step %d\n", filename.c_str(), c, GetSize(steps));
+ }
+ steps.push_back(step);
+ }
+}
+
+RTLIL::Const ReadWitness::get_bits(int t, int bits_offset, int width) const
+{
+ log_assert(t >= 0 && t < GetSize(steps));
+
+ const std::string &bits = steps[t].bits;
+
+ RTLIL::Const result(State::Sa, width);
+ result.bits.reserve(width);
+
+ int read_begin = GetSize(bits) - 1 - bits_offset;
+ int read_end = max(-1, read_begin - width);
+
+ min(width, GetSize(bits) - bits_offset);
+
+ for (int i = read_begin, j = 0; i > read_end; i--, j++) {
+ RTLIL::State bit = State::Sa;
+ switch (bits[i]) {
+ case '0': bit = State::S0; break;
+ case '1': bit = State::S1; break;
+ case 'x': bit = State::Sx; break;
+ case '?': bit = State::Sa; break;
+ default:
+ log_abort();
+ }
+ result.bits[j] = bit;
+ }
+
+ return result;
+}
diff --git a/kernel/yw.h b/kernel/yw.h
new file mode 100644
index 000000000..c2f5921b1
--- /dev/null
+++ b/kernel/yw.h
@@ -0,0 +1,182 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#ifndef YW_H
+#define YW_H
+
+#include "kernel/yosys.h"
+#include "kernel/mem.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+struct IdPath : public std::vector<RTLIL::IdString>
+{
+ template<typename... T>
+ IdPath(T&&... args) : std::vector<RTLIL::IdString>(std::forward<T>(args)...) { }
+ IdPath prefix() const { return {begin(), end() - !empty()}; }
+ std::string str() const;
+
+ bool has_address() const { int tmp; return get_address(tmp); };
+ bool get_address(int &addr) const;
+
+ int hash() const { return hashlib::hash_ops<std::vector<RTLIL::IdString>>::hash(*this); }
+};
+
+struct WitnessHierarchyItem {
+ RTLIL::Module *module;
+ RTLIL::Wire *wire = nullptr;
+ RTLIL::Cell *cell = nullptr;
+ Mem *mem = nullptr;
+
+ WitnessHierarchyItem(RTLIL::Module *module, RTLIL::Wire *wire) : module(module), wire(wire) {}
+ WitnessHierarchyItem(RTLIL::Module *module, RTLIL::Cell *cell) : module(module), cell(cell) {}
+ WitnessHierarchyItem(RTLIL::Module *module, Mem *mem) : module(module), mem(mem) {}
+};
+
+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 {
+ IdPath path;
+ int offset;
+ bool is_posedge = false;
+ bool is_negedge = false;
+ };
+
+ struct Signal {
+ IdPath path;
+ int offset;
+ int width;
+ bool init_only;
+
+ int bits_offset;
+ };
+
+ struct Step {
+ std::string bits;
+ };
+
+ std::string filename;
+ std::vector<Clock> clocks;
+ std::vector<Signal> signals;
+ std::vector<Step> steps;
+
+ ReadWitness(const std::string &filename);
+
+ RTLIL::Const get_bits(int t, int bits_offset, int width) const;
+};
+
+template<typename D, typename T>
+void witness_hierarchy_recursion(IdPath &path, int hdlname_mode, RTLIL::Module *module, D data, T &callback)
+{
+ auto const &const_path = path;
+ size_t path_size = path.size();
+ for (auto wire : module->wires())
+ {
+ auto hdlname = hdlname_mode < 0 ? std::vector<std::string>() : wire->get_hdlname_attribute();
+ for (auto item : hdlname)
+ path.push_back("\\" + item);
+ if (hdlname.size() == 1 && path.back() == wire->name)
+ hdlname.clear();
+ if (!hdlname.empty())
+ callback(const_path, WitnessHierarchyItem(module, wire), data);
+ path.resize(path_size);
+ if (hdlname.empty() || hdlname_mode <= 0) {
+ path.push_back(wire->name);
+ callback(const_path, WitnessHierarchyItem(module, wire), data);
+ path.pop_back();
+ }
+ }
+
+ for (auto cell : module->cells())
+ {
+ Module *child = module->design->module(cell->type);
+ if (child == nullptr)
+ continue;
+
+ auto hdlname = hdlname_mode < 0 ? std::vector<std::string>() : cell->get_hdlname_attribute();
+ for (auto item : hdlname)
+ path.push_back("\\" + item);
+ if (hdlname.size() == 1 && path.back() == cell->name)
+ hdlname.clear();
+ if (!hdlname.empty()) {
+ D child_data = callback(const_path, WitnessHierarchyItem(module, cell), data);
+ witness_hierarchy_recursion<D, T>(path, 1, child, child_data, callback);
+ }
+ path.resize(path_size);
+ if (hdlname.empty() || hdlname_mode <= 0) {
+ path.push_back(cell->name);
+ D child_data = callback(const_path, WitnessHierarchyItem(module, cell), data);
+ witness_hierarchy_recursion<D, T>(path, hdlname.empty() ? hdlname_mode : -1, child, child_data, callback);
+ path.pop_back();
+ }
+ }
+
+ for (auto mem : Mem::get_all_memories(module)) {
+ std::vector<std::string> hdlname;
+
+ if (hdlname_mode >= 0 && mem.cell != nullptr)
+ hdlname = mem.cell->get_hdlname_attribute();
+ for (auto item : hdlname)
+ path.push_back("\\" + item);
+ if (hdlname.size() == 1 && path.back() == mem.cell->name)
+ hdlname.clear();
+ if (!hdlname.empty()) {
+ callback(const_path, WitnessHierarchyItem(module, &mem), data);
+ }
+ path.resize(path_size);
+
+ if (hdlname.empty() || hdlname_mode <= 0) {
+ path.push_back(mem.memid);
+ callback(const_path, WitnessHierarchyItem(module, &mem), data);
+ path.pop_back();
+
+ if (mem.cell != nullptr && mem.cell->name != mem.memid) {
+ path.push_back(mem.cell->name);
+ callback(const_path, WitnessHierarchyItem(module, &mem), data);
+ path.pop_back();
+ }
+ }
+ }
+}
+
+template<typename D, typename T>
+void witness_hierarchy(RTLIL::Module *module, D data, T callback)
+{
+ IdPath path;
+ witness_hierarchy_recursion<D, T>(path, 0, module, data, callback);
+}
+
+YOSYS_NAMESPACE_END
+
+#endif
diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc
index 590a7eb1d..7293002f3 100644
--- a/passes/cmds/setundef.cc
+++ b/passes/cmds/setundef.cc
@@ -502,7 +502,15 @@ struct SetundefPass : public Pass {
}
}
- module->rewrite_sigspecs(worker);
+ for (auto &it : module->cells_)
+ if (!it.second->get_bool_attribute(ID::xprop_decoder))
+ it.second->rewrite_sigspecs(worker);
+ for (auto &it : module->processes)
+ it.second->rewrite_sigspecs(worker);
+ for (auto &it : module->connections_) {
+ worker(it.first);
+ worker(it.second);
+ }
if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST)
{
diff --git a/passes/cmds/xprop.cc b/passes/cmds/xprop.cc
index 5dee72e1b..5e78ff9fc 100644
--- a/passes/cmds/xprop.cc
+++ b/passes/cmds/xprop.cc
@@ -252,7 +252,8 @@ struct XpropWorker
}
if (!driven_orig.empty()) {
- module->addBwmux(NEW_ID, driven_enc.is_1, Const(State::Sx, GetSize(driven_orig)), driven_enc.is_x, driven_orig);
+ auto decoder = module->addBwmux(NEW_ID, driven_enc.is_1, Const(State::Sx, GetSize(driven_orig)), driven_enc.is_x, driven_orig);
+ decoder->set_bool_attribute(ID::xprop_decoder);
}
if (!driven_never_x.first.empty()) {
module->connect(driven_never_x);
diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc
index e36379096..099df4be9 100644
--- a/passes/sat/formalff.cc
+++ b/passes/sat/formalff.cc
@@ -317,6 +317,172 @@ struct InitValWorker
}
};
+struct ReplacedPort {
+ IdString name;
+ int offset;
+ bool clk_pol;
+};
+
+struct HierarchyWorker
+{
+ Design *design;
+ pool<Module *> pending;
+
+ dict<Module *, std::vector<ReplacedPort>> replaced_clk_inputs;
+
+ HierarchyWorker(Design *design) :
+ design(design)
+ {
+ for (auto module : design->modules())
+ pending.insert(module);
+ }
+
+ void propagate();
+
+ const std::vector<ReplacedPort> &find_replaced_clk_inputs(IdString cell_type);
+};
+
+// Propagates replaced clock signals
+struct PropagateWorker
+{
+ HierarchyWorker &hierarchy;
+
+ Module *module;
+ SigMap sigmap;
+
+ dict<SigBit, bool> replaced_clk_bits;
+ dict<SigBit, SigBit> not_drivers;
+
+ std::vector<ReplacedPort> replaced_clk_inputs;
+ std::vector<std::pair<SigBit, bool>> pending;
+
+ PropagateWorker(Module *module, HierarchyWorker &hierarchy) :
+ hierarchy(hierarchy), module(module), sigmap(module)
+ {
+ hierarchy.pending.erase(module);
+
+ for (auto wire : module->wires())
+ if (wire->has_attribute(ID::replaced_by_gclk))
+ replace_clk_bit(SigBit(wire), wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1, false);
+
+ for (auto cell : module->cells()) {
+ if (cell->type.in(ID($not), ID($_NOT_))) {
+ auto sig_a = cell->getPort(ID::A);
+ auto &sig_y = cell->getPort(ID::Y);
+ sig_a.extend_u0(GetSize(sig_y), cell->parameters.at(ID::A_SIGNED).as_bool());
+
+ for (int i = 0; i < GetSize(sig_a); i++)
+ if (sig_a[i].is_wire())
+ not_drivers.emplace(sigmap(sig_y[i]), sigmap(sig_a[i]));
+ } else {
+ for (auto &port_bit : hierarchy.find_replaced_clk_inputs(cell->type))
+ replace_clk_bit(cell->getPort(port_bit.name)[port_bit.offset], port_bit.clk_pol, true);
+ }
+ }
+
+ while (!pending.empty()) {
+ auto current = pending.back();
+ pending.pop_back();
+ auto it = not_drivers.find(current.first);
+ if (it == not_drivers.end())
+ continue;
+
+ replace_clk_bit(it->second, !current.second, true);
+ }
+
+ for (auto cell : module->cells()) {
+ if (cell->type.in(ID($not), ID($_NOT_)))
+ continue;
+ for (auto &conn : cell->connections()) {
+ if (!cell->output(conn.first))
+ continue;
+ for (SigBit bit : conn.second) {
+ sigmap.apply(bit);
+ if (replaced_clk_bits.count(bit))
+ log_error("derived signal %s driven by %s (%s) from module %s is used as clock, derived clocks are only supported with clk2fflogic.\n",
+ log_signal(bit), log_id(cell->name), log_id(cell->type), log_id(module));
+ }
+ }
+ }
+
+ for (auto port : module->ports) {
+ auto wire = module->wire(port);
+ if (!wire->port_input)
+ continue;
+ for (int i = 0; i < GetSize(wire); i++) {
+ SigBit bit(wire, i);
+ sigmap.apply(bit);
+ auto it = replaced_clk_bits.find(bit);
+ if (it == replaced_clk_bits.end())
+ continue;
+ replaced_clk_inputs.emplace_back(ReplacedPort {port, i, it->second});
+
+ if (it->second) {
+ bit = module->Not(NEW_ID, bit);
+ }
+ }
+ }
+ }
+
+ void replace_clk_bit(SigBit bit, bool polarity, bool add_attribute)
+ {
+ sigmap.apply(bit);
+ if (!bit.is_wire())
+ log_error("XXX todo\n");
+
+ auto it = replaced_clk_bits.find(bit);
+ if (it != replaced_clk_bits.end()) {
+ if (it->second != polarity)
+ log_error("signal %s from module %s is used as clock with different polarities, run clk2fflogic instead.\n",
+ log_signal(bit), log_id(module));
+ return;
+ }
+
+ replaced_clk_bits.emplace(bit, polarity);
+
+ if (add_attribute) {
+ Wire *clk_wire = bit.wire;
+ if (bit.offset != 0 || GetSize(bit.wire) != 1) {
+ clk_wire = module->addWire(NEW_ID);
+ module->connect(RTLIL::SigBit(clk_wire), bit);
+ }
+ clk_wire->attributes[ID::replaced_by_gclk] = polarity ? State::S1 : State::S0;
+ clk_wire->set_bool_attribute(ID::keep);
+ }
+
+ pending.emplace_back(bit, polarity);
+ }
+};
+
+const std::vector<ReplacedPort> &HierarchyWorker::find_replaced_clk_inputs(IdString cell_type)
+{
+ static const std::vector<ReplacedPort> empty;
+ if (!cell_type.isPublic())
+ return empty;
+
+ Module *module = design->module(cell_type);
+ if (module == nullptr)
+ return empty;
+
+ auto it = replaced_clk_inputs.find(module);
+ if (it != replaced_clk_inputs.end())
+ return it->second;
+
+ if (pending.count(module)) {
+ PropagateWorker worker(module, *this);
+ return replaced_clk_inputs.emplace(module, std::move(worker.replaced_clk_inputs)).first->second;
+ }
+
+ return empty;
+}
+
+
+void HierarchyWorker::propagate()
+{
+ while (!pending.empty())
+ PropagateWorker worker(pending.pop(), *this);
+}
+
struct FormalFfPass : public Pass {
FormalFfPass() : Pass("formalff", "prepare FFs for formal") { }
void help() override
@@ -362,6 +528,15 @@ struct FormalFfPass : public Pass {
log(" them. For -ff2anyinit, this reduces the number of generated $anyinit\n");
log(" cells that drive wires with private names.\n");
log("\n");
+ log(" -hierarchy\n");
+ log(" Propagates the 'replaced_by_gclk' attribute set by clk2ff upwards\n");
+ log(" through the design hierarchy towards the toplevel inputs. This option\n");
+ log(" works on the whole design and ignores the selection.\n");
+ log("\n");
+ log(" -assume\n");
+ log(" Add assumptions that constrain wires with the 'replaced_by_gclk'\n");
+ log(" attribute to the value they would have before an active clock edge.\n");
+ log("\n");
// TODO: An option to check whether all FFs use the same clock before changing it to the global clock
}
@@ -372,6 +547,8 @@ struct FormalFfPass : public Pass {
bool flag_anyinit2ff = false;
bool flag_fine = false;
bool flag_setundef = false;
+ bool flag_hierarchy = false;
+ bool flag_assume = false;
log_header(design, "Executing FORMALFF pass.\n");
@@ -398,12 +575,20 @@ struct FormalFfPass : public Pass {
flag_setundef = true;
continue;
}
+ if (args[argidx] == "-hierarchy") {
+ flag_hierarchy = true;
+ continue;
+ }
+ if (args[argidx] == "-assume") {
+ flag_assume = true;
+ continue;
+ }
break;
}
extra_args(args, argidx, design);
- if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff))
- log_cmd_error("One of the options -clk2ff, -ff2anyinit, or -anyinit2ff must be specified.\n");
+ if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff || flag_hierarchy || flag_assume))
+ log_cmd_error("One of the options -clk2ff, -ff2anyinit, -anyinit2ff, -hierarchy or -assume must be specified.\n");
if (flag_ff2anyinit && flag_anyinit2ff)
log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n");
@@ -548,6 +733,33 @@ struct FormalFfPass : public Pass {
ff.emit();
}
}
+
+ if (flag_hierarchy) {
+ HierarchyWorker worker(design);
+ worker.propagate();
+ }
+
+ if (flag_assume) {
+ for (auto module : design->selected_modules()) {
+ std::vector<pair<SigBit, bool>> found;
+ for (auto wire : module->wires()) {
+ if (!wire->has_attribute(ID::replaced_by_gclk))
+ continue;
+ bool clk_pol = wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1;
+
+ found.emplace_back(SigSpec(wire), clk_pol);
+ }
+ for (auto pair : found) {
+ SigBit clk = pair.first;
+
+ if (pair.second)
+ clk = module->Not(NEW_ID, clk);
+
+ module->addAssume(NEW_ID, clk, State::S1);
+
+ }
+ }
+ }
}
} FormalFfPass;
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc
index 0084a1f28..cfe31968d 100644
--- a/passes/sat/sim.cc
+++ b/passes/sat/sim.cc
@@ -23,6 +23,8 @@
#include "kernel/mem.h"
#include "kernel/fstdata.h"
#include "kernel/ff.h"
+#include "kernel/yw.h"
+#include "kernel/json.h"
#include <ctime>
@@ -74,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;
@@ -93,6 +106,9 @@ struct SimShared
bool ignore_x = false;
bool date = false;
bool multiclock = false;
+ int next_output_id = 0;
+ int step = 0;
+ std::vector<TriggeredAssertion> triggered_assertions;
};
void zinit(State &v)
@@ -152,11 +168,14 @@ struct SimInstance
dict<Cell*, ff_state_t> ff_database;
dict<IdString, mem_state_t> mem_database;
pool<Cell*> formal_database;
+ pool<Cell*> initstate_database;
dict<Cell*, IdString> mem_cells;
std::vector<Mem> memories;
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;
@@ -254,6 +273,8 @@ struct SimInstance
if (cell->type.in(ID($assert), ID($cover), ID($assume))) {
formal_database.insert(cell);
}
+ if (cell->type == ID($initstate))
+ initstate_database.insert(cell);
}
if (shared->zinit)
@@ -300,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;
@@ -325,7 +361,7 @@ struct SimInstance
log_assert(GetSize(sig) <= GetSize(value));
for (int i = 0; i < GetSize(sig); i++)
- if (state_nets.at(sig[i]) != value[i]) {
+ if (value[i] != State::Sa && state_nets.at(sig[i]) != value[i]) {
state_nets.at(sig[i]) = value[i];
dirty_bits.insert(sig[i]);
did_something = true;
@@ -338,12 +374,23 @@ struct SimInstance
void set_memory_state(IdString memid, Const addr, Const data)
{
+ set_memory_state(memid, addr.as_int(), data);
+ }
+
+ void set_memory_state(IdString memid, int addr, Const data)
+ {
auto &state = mem_database[memid];
- int offset = (addr.as_int() - state.mem->start_offset) * state.mem->width;
+ bool dirty = false;
+
+ int offset = (addr - state.mem->start_offset) * state.mem->width;
for (int i = 0; i < GetSize(data); i++)
- if (0 <= i+offset && i+offset < state.mem->size * state.mem->width)
- state.data.bits[i+offset] = data.bits[i];
+ if (0 <= i+offset && i+offset < state.mem->size * state.mem->width && data.bits[i] != State::Sa)
+ if (state.data.bits[i+offset] != data.bits[i])
+ dirty = true, state.data.bits[i+offset] = data.bits[i];
+
+ if (dirty)
+ dirty_memories.insert(memid);
}
void set_memory_state_bit(IdString memid, int offset, State data)
@@ -351,7 +398,10 @@ struct SimInstance
auto &state = mem_database[memid];
if (offset >= state.mem->size * state.mem->width)
log_error("Addressing out of bounds bit %d/%d of memory %s\n", offset, state.mem->size * state.mem->width, log_id(memid));
- state.data.bits[offset] = data;
+ if (state.data.bits[offset] != data) {
+ state.data.bits[offset] = data;
+ dirty_memories.insert(memid);
+ }
}
void update_cell(Cell *cell)
@@ -447,9 +497,14 @@ struct SimInstance
log_error("Memory %s.%s has clocked read ports. Run 'memory' with -nordff.\n", log_id(module), log_id(mem.memid));
if (addr.is_fully_def()) {
- int index = addr.as_int() - mem.start_offset;
+ int addr_int = addr.as_int();
+ int index = addr_int - mem.start_offset;
if (index >= 0 && index < mem.size)
data = mdb.data.extract(index*mem.width, mem.width << port.wide_log2);
+
+ for (int offset = 0; offset < 1 << port.wide_log2; offset++) {
+ register_memory_addr(id, addr_int + offset);
+ }
}
set_state(port.data, data);
@@ -604,7 +659,8 @@ struct SimInstance
if (addr.is_fully_def())
{
- int index = addr.as_int() - mem.start_offset;
+ int addr_int = addr.as_int();
+ int index = addr_int - mem.start_offset;
if (index >= 0 && index < mem.size)
for (int i = 0; i < (mem.width << port.wide_log2); i++)
if (enable[i] == State::S1 && mdb.data.bits.at(index*mem.width+i) != data[i]) {
@@ -612,6 +668,9 @@ struct SimInstance
dirty_memories.insert(mem.memid);
did_something = true;
}
+
+ for (int i = 0; i < 1 << port.wide_log2; i++)
+ register_memory_addr(it.first, addr_int + i);
}
}
}
@@ -625,7 +684,7 @@ struct SimInstance
return did_something;
}
- void update_ph3()
+ void update_ph3(bool check_assertions)
{
for (auto &it : ff_database)
{
@@ -660,27 +719,42 @@ struct SimInstance
}
}
- for (auto cell : formal_database)
+ if (check_assertions)
{
- string label = log_id(cell);
- if (cell->attributes.count(ID::src))
- label = cell->attributes.at(ID::src).decode_string();
+ for (auto cell : formal_database)
+ {
+ string label = log_id(cell);
+ if (cell->attributes.count(ID::src))
+ label = cell->attributes.at(ID::src).decode_string();
+
+ State a = get_state(cell->getPort(ID::A))[0];
+ State en = get_state(cell->getPort(ID::EN))[0];
- State a = get_state(cell->getPort(ID::A))[0];
- State en = get_state(cell->getPort(ID::EN))[0];
+ 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($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)
- log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
+ if (cell->type == ID($assume) && en == State::S1 && a != State::S1)
+ log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
- if (cell->type == ID($assert) && en == State::S1 && a != State::S1)
- log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
+ if (cell->type == ID($assert) && en == State::S1 && a != State::S1)
+ log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str());
+ }
}
for (auto it : children)
- it.second->update_ph3();
+ it.second->update_ph3(check_assertions);
+ }
+
+ void set_initstate_outputs(State state)
+ {
+ for (auto cell : initstate_database)
+ set_state(cell->getPort(ID::Y), state);
+ for (auto child : children)
+ child.second->set_initstate_outputs(state);
}
void writeback(pool<Module*> &wbmods)
@@ -741,7 +815,7 @@ struct SimInstance
child.second->register_signals(id);
}
- void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(const char*, Wire*, int, bool)> register_signal)
+ void write_output_header(std::function<void(IdString)> enter_scope, std::function<void()> exit_scope, std::function<void(const char*, int, Wire*, int, bool)> register_signal)
{
int exit_scopes = 1;
if (shared->hdlname && instance != nullptr && instance->name.isPublic() && instance->has_attribute(ID::hdlname)) {
@@ -774,11 +848,45 @@ struct SimInstance
hdlname.pop_back();
for (auto name : hdlname)
enter_scope("\\" + name);
- register_signal(signal_name.c_str(), signal.first, signal.second.first, registers.count(signal.first)!=0);
+ register_signal(signal_name.c_str(), GetSize(signal.first), signal.first, signal.second.first, registers.count(signal.first)!=0);
for (auto name : hdlname)
exit_scope();
} else
- register_signal(log_id(signal.first->name), signal.first, signal.second.first, registers.count(signal.first)!=0);
+ register_signal(log_id(signal.first->name), GetSize(signal.first), signal.first, signal.second.first, registers.count(signal.first)!=0);
+ }
+
+ for (auto &trace_mem : trace_mem_database)
+ {
+ auto memid = trace_mem.first;
+ auto &mdb = mem_database.at(memid);
+ Cell *cell = mdb.mem->cell;
+
+ std::vector<std::string> hdlname;
+ std::string signal_name;
+ bool has_hdlname = shared->hdlname && cell != nullptr && cell->name.isPublic() && cell->has_attribute(ID::hdlname);
+
+ if (has_hdlname) {
+ hdlname = cell->get_hdlname_attribute();
+ log_assert(!hdlname.empty());
+ signal_name = std::move(hdlname.back());
+ hdlname.pop_back();
+ for (auto name : hdlname)
+ enter_scope("\\" + name);
+ } else {
+ signal_name = log_id(memid);
+ }
+
+ for (auto &trace_index : trace_mem.second) {
+ int output_id = trace_index.second.first;
+ int index = trace_index.first;
+ register_signal(
+ stringf("%s[%d]", signal_name.c_str(), (index + mdb.mem->start_offset)).c_str(),
+ mdb.mem->width, nullptr, output_id, true);
+ }
+
+ if (has_hdlname)
+ for (auto name : hdlname)
+ exit_scope();
}
for (auto child : children)
@@ -788,6 +896,30 @@ struct SimInstance
exit_scope();
}
+ void register_memory_addr(IdString memid, int addr)
+ {
+ auto &mdb = mem_database.at(memid);
+ auto &mem = *mdb.mem;
+ int index = addr - mem.start_offset;
+ if (index < 0 || index >= mem.size)
+ return;
+ auto it = trace_mem_database.find(memid);
+ if (it != trace_mem_database.end() && it->second.count(index))
+ return;
+ 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);
+ }
+ trace_mem_database[memid].emplace(index, make_pair(output_id, data));
+
+ }
+
void register_output_step_values(std::map<int,Const> *data)
{
for (auto &it : signal_database)
@@ -803,6 +935,26 @@ struct SimInstance
data->emplace(id, value);
}
+ for (auto &trace_mem : trace_mem_database)
+ {
+ auto memid = trace_mem.first;
+ auto &mdb = mem_database.at(memid);
+ auto &mem = *mdb.mem;
+ for (auto &trace_index : trace_mem.second)
+ {
+ int output_id = trace_index.second.first;
+ int index = trace_index.first;
+
+ auto value = mdb.data.extract(index * mem.width, mem.width);
+
+ if (trace_index.second.second == value)
+ continue;
+
+ trace_index.second.second = value;
+ data->emplace(output_id, value);
+ }
+ }
+
for (auto child : children)
child.second->register_output_step_values(data);
}
@@ -946,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()
@@ -956,8 +1109,8 @@ struct SimWorker : SimShared
void register_signals()
{
- int id = 1;
- top->register_signals(id);
+ next_output_id = 1;
+ top->register_signals(top->shared->next_output_id);
}
void register_output_step(int t)
@@ -989,6 +1142,9 @@ struct SimWorker : SimShared
void update(bool gclk)
{
+ if (gclk)
+ step += 1;
+
while (1)
{
if (debug)
@@ -1006,7 +1162,7 @@ struct SimWorker : SimShared
if (debug)
log("\n-- ph3 --\n");
- top->update_ph3();
+ top->update_ph3(gclk);
}
void initialize_stable_past()
@@ -1016,7 +1172,7 @@ struct SimWorker : SimShared
top->update_ph1();
if (debug)
log("\n-- ph3 (initialize) --\n");
- top->update_ph3();
+ top->update_ph3(true);
}
void set_inports(pool<IdString> ports, State value)
@@ -1490,6 +1646,242 @@ struct SimWorker : SimShared
write_output_files();
}
+ struct FoundYWPath
+ {
+ SimInstance *instance;
+ Wire *wire;
+ IdString memid;
+ int addr;
+ };
+
+ struct YwHierarchy {
+ dict<IdPath, FoundYWPath> paths;
+ };
+
+ YwHierarchy prepare_yw_hierarchy(const ReadWitness &yw)
+ {
+ YwHierarchy hierarchy;
+ pool<IdPath> paths;
+ dict<IdPath, pool<IdString>> mem_paths;
+
+ for (auto &signal : yw.signals)
+ paths.insert(signal.path);
+
+ for (auto &clock : yw.clocks)
+ paths.insert(clock.path);
+
+ for (auto &path : paths)
+ if (path.has_address())
+ mem_paths[path.prefix()].insert(path.back());
+
+ witness_hierarchy(top->module, top, [&](IdPath const &path, WitnessHierarchyItem item, SimInstance *instance) {
+ if (item.cell != nullptr)
+ return instance->children.at(item.cell);
+ if (item.wire != nullptr) {
+ if (paths.count(path)) {
+ if (debug)
+ log("witness hierarchy: found wire %s\n", path.str().c_str());
+ bool inserted = hierarchy.paths.emplace(path, {instance, item.wire, {}, INT_MIN}).second;
+ if (!inserted)
+ log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str());
+ }
+ } else if (item.mem) {
+ auto it = mem_paths.find(path);
+ if (it != mem_paths.end()) {
+ if (debug)
+ log("witness hierarchy: found mem %s\n", path.str().c_str());
+ IdPath word_path = path;
+ word_path.emplace_back();
+ for (auto addr_part : it->second) {
+ word_path.back() = addr_part;
+ int addr;
+ word_path.get_address(addr);
+ if (addr < item.mem->start_offset || (addr - item.mem->start_offset) >= item.mem->size)
+ continue;
+ bool inserted = hierarchy.paths.emplace(word_path, {instance, nullptr, item.mem->memid, addr}).second;
+ if (!inserted)
+ log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str());
+ }
+ }
+ }
+ return instance;
+ });
+
+ for (auto &path : paths)
+ if (!hierarchy.paths.count(path))
+ log_warning("Yosys witness path `%s` was not found in this design, ignoring\n", path.str().c_str());
+
+ dict<IdPath, dict<int, bool>> clock_inputs;
+
+ for (auto &clock : yw.clocks) {
+ if (clock.is_negedge == clock.is_posedge)
+ continue;
+ clock_inputs[clock.path].emplace(clock.offset, clock.is_posedge);
+ }
+ for (auto &signal : yw.signals) {
+ auto it = clock_inputs.find(signal.path);
+ if (it == clock_inputs.end())
+ continue;
+
+ for (auto &clock_input : it->second) {
+ int offset = clock_input.first;
+ if (offset >= signal.offset && (offset - signal.offset) < signal.width) {
+ int clock_bits_offset = signal.bits_offset + (offset - signal.offset);
+
+ State expected = clock_input.second ? State::S0 : State::S1;
+
+ for (int t = 0; t < GetSize(yw.steps); t++) {
+ if (yw.get_bits(t, clock_bits_offset, 1) != expected)
+ log_warning("Yosys witness trace has an unexpected value for the clock input `%s` in step %d.\n", signal.path.str().c_str(), t);
+ }
+ }
+ }
+ }
+ // TODO add checks and warnings for witness signals (toplevel inputs, $any*) not present in the witness file
+
+ return hierarchy;
+ }
+
+ void set_yw_state(const ReadWitness &yw, const YwHierarchy &hierarchy, int t)
+ {
+ log_assert(t >= 0 && t < GetSize(yw.steps));
+
+ for (auto &signal : yw.signals) {
+ if (signal.init_only && t >= 1)
+ continue;
+ auto found_path_it = hierarchy.paths.find(signal.path);
+ if (found_path_it == hierarchy.paths.end())
+ continue;
+ auto &found_path = found_path_it->second;
+
+ Const value = yw.get_bits(t, signal.bits_offset, signal.width);
+
+ if (debug)
+ log("yw: set %s to %s\n", signal.path.str().c_str(), log_const(value));
+
+ if (found_path.wire != nullptr) {
+ found_path.instance->set_state(
+ 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);
+ }
+ }
+ }
+
+ void set_yw_clocks(const ReadWitness &yw, const YwHierarchy &hierarchy, bool active_edge)
+ {
+ for (auto &clock : yw.clocks) {
+ if (clock.is_negedge == clock.is_posedge)
+ continue;
+ auto found_path_it = hierarchy.paths.find(clock.path);
+ if (found_path_it == hierarchy.paths.end())
+ continue;
+ auto &found_path = found_path_it->second;
+
+ if (found_path.wire != nullptr) {
+ found_path.instance->set_state(
+ SigChunk(found_path.wire, clock.offset, 1),
+ active_edge == clock.is_posedge ? State::S1 : State::S0);
+ }
+ }
+ }
+
+ void run_cosim_yw_witness(Module *topmod, int append)
+ {
+ if (!clock.empty())
+ log_cmd_error("The -clock option is not required nor supported when reading a Yosys witness file.\n");
+ if (!reset.empty())
+ log_cmd_error("The -reset option is not required nor supported when reading a Yosys witness file.\n");
+ if (multiclock)
+ log_warning("The -multiclock option is not required and ignored when reading a Yosys witness file.\n");
+
+ ReadWitness yw(sim_filename);
+
+ top = new SimInstance(this, scope, topmod);
+ register_signals();
+
+ YwHierarchy hierarchy = prepare_yw_hierarchy(yw);
+
+ if (yw.steps.empty()) {
+ log_warning("Yosys witness file `%s` contains no time steps\n", yw.filename.c_str());
+ } else {
+ top->set_initstate_outputs(State::S1);
+ set_yw_state(yw, hierarchy, 0);
+ set_yw_clocks(yw, hierarchy, true);
+ initialize_stable_past();
+ register_output_step(0);
+
+ if (!yw.clocks.empty()) {
+ if (debug)
+ log("Simulating non-active clock edge.\n");
+ set_yw_clocks(yw, hierarchy, false);
+ update(false);
+ register_output_step(5);
+ }
+ top->set_initstate_outputs(State::S0);
+ }
+
+ for (int cycle = 1; cycle < GetSize(yw.steps) + append; cycle++)
+ {
+ if (verbose)
+ log("Simulating cycle %d.\n", cycle);
+ if (cycle < GetSize(yw.steps))
+ set_yw_state(yw, hierarchy, cycle);
+ set_yw_clocks(yw, hierarchy, true);
+ update(true);
+ register_output_step(10 * cycle);
+
+ if (!yw.clocks.empty()) {
+ if (debug)
+ log("Simulating non-active clock edge.\n");
+ set_yw_clocks(yw, hierarchy, false);
+ update(false);
+ register_output_step(5 + 10 * cycle);
+ }
+ }
+
+ register_output_step(10 * (GetSize(yw.steps) + append));
+ 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;
@@ -1734,9 +2126,15 @@ struct VCDWriter : public OutputWriter
worker->top->write_output_header(
[this](IdString name) { vcdfile << stringf("$scope module %s $end\n", log_id(name)); },
[this]() { vcdfile << stringf("$upscope $end\n");},
- [this,use_signal](const char *name, Wire *wire, int id, bool is_reg) {
+ [this,use_signal](const char *name, int size, Wire *, int id, bool is_reg) {
if (use_signal.at(id)) {
- vcdfile << stringf("$var %s %d n%d %s%s $end\n", is_reg ? "reg" : "wire", GetSize(wire), id, name[0] == '$' ? "\\" : "", name);
+ // Works around gtkwave trying to parse everything past the last [ in a signal
+ // name. While the emitted range doesn't necessarily match the wire's range,
+ // this is consistent with the range gtkwave makes up if it doesn't find a
+ // range
+ std::string range = strchr(name, '[') ? stringf("[%d:0]", size - 1) : std::string();
+ vcdfile << stringf("$var %s %d n%d %s%s%s $end\n", is_reg ? "reg" : "wire", size, id, name[0] == '$' ? "\\" : "", name, range.c_str());
+
}
}
);
@@ -1796,9 +2194,9 @@ struct FSTWriter : public OutputWriter
worker->top->write_output_header(
[this](IdString name) { fstWriterSetScope(fstfile, FST_ST_VCD_MODULE, stringf("%s",log_id(name)).c_str(), nullptr); },
[this]() { fstWriterSetUpscope(fstfile); },
- [this,use_signal](const char *name, Wire *wire, int id, bool is_reg) {
+ [this,use_signal](const char *name, int size, Wire *, int id, bool is_reg) {
if (!use_signal.at(id)) return;
- fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, GetSize(wire),
+ fstHandle fst_id = fstWriterCreateVar(fstfile, is_reg ? FST_VT_VCD_REG : FST_VT_VCD_WIRE, FST_VD_IMPLICIT, size,
name, 0);
mapping.emplace(id, fst_id);
}
@@ -1881,7 +2279,7 @@ struct AIWWriter : public OutputWriter
worker->top->write_output_header(
[](IdString) {},
[]() {},
- [this](const char */*name*/, Wire *wire, int id, bool) { mapping[wire] = id; }
+ [this](const char */*name*/, int /*size*/, Wire *wire, int id, bool) { if (wire != nullptr) mapping[wire] = id; }
);
std::map<int, Yosys::RTLIL::Const> current;
@@ -2013,11 +2411,17 @@ struct SimPass : public Pass {
log(" -w\n");
log(" writeback mode: use final simulation state as new init state\n");
log("\n");
- log(" -r\n");
- log(" read simulation results file\n");
- log(" File formats supported: FST, VCD, AIW and WIT\n");
+ log(" -r <filename>\n");
+ log(" read simulation or formal results file\n");
+ log(" File formats supported: FST, VCD, AIW, WIT and .yw\n");
log(" VCD support requires vcd2fst external tool to be present\n");
log("\n");
+ 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");
@@ -2063,6 +2467,7 @@ struct SimPass : public Pass {
{
SimWorker worker;
int numcycles = 20;
+ int append = 0;
bool start_set = false, stop_set = false, at_set = false;
log_header(design, "Executing SIM pass (simulate the circuit).\n");
@@ -2146,12 +2551,22 @@ struct SimPass : public Pass {
worker.sim_filename = sim_filename;
continue;
}
+ if (args[argidx] == "-append" && argidx+1 < args.size()) {
+ append = atoi(args[++argidx].c_str());
+ continue;
+ }
if (args[argidx] == "-map" && argidx+1 < args.size()) {
std::string map_filename = args[++argidx];
rewrite_filename(map_filename);
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;
@@ -2235,10 +2650,14 @@ struct SimPass : public Pass {
worker.run_cosim_aiger_witness(top_mod);
} else if (filename_trim.size() > 4 && filename_trim.compare(filename_trim.size()-4, std::string::npos, ".wit") == 0) {
worker.run_cosim_btor2_witness(top_mod);
+ } else if (filename_trim.size() > 3 && filename_trim.compare(filename_trim.size()-3, std::string::npos, ".yw") == 0) {
+ worker.run_cosim_yw_witness(top_mod, append);
} else {
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-12-26 21:51:44 +0000