aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
Diffstat (limited to 'backends')
-rw-r--r--backends/aiger/aiger.cc169
-rw-r--r--backends/blif/blif.cc4
-rw-r--r--backends/btor/btor.cc197
-rw-r--r--backends/cxxrtl/cxxrtl.h21
-rw-r--r--backends/cxxrtl/cxxrtl_backend.cc2
-rw-r--r--backends/edif/edif.cc4
-rw-r--r--backends/firrtl/firrtl.cc10
-rw-r--r--backends/jny/jny.cc48
-rw-r--r--backends/json/json.cc13
-rw-r--r--backends/protobuf/.gitignore2
-rw-r--r--backends/protobuf/Makefile.inc10
-rw-r--r--backends/protobuf/protobuf.cc371
-rw-r--r--backends/rtlil/rtlil_backend.cc9
-rw-r--r--backends/smt2/Makefile.inc16
-rw-r--r--backends/smt2/smt2.cc179
-rw-r--r--backends/smt2/smtbmc.py476
-rw-r--r--backends/smt2/smtio.py97
-rw-r--r--backends/smt2/witness.py410
-rw-r--r--backends/smt2/ywio.py393
-rw-r--r--backends/smv/smv.cc1
-rw-r--r--backends/verilog/verilog_backend.cc51
21 files changed, 1896 insertions, 587 deletions
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 547d131ee..4ef28be9f 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -19,6 +19,9 @@
#include "kernel/yosys.h"
#include "kernel/sigtools.h"
+#include "kernel/json.h"
+#include "kernel/yw.h"
+#include "libs/json11/json11.hpp"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
@@ -61,6 +64,8 @@ struct AigerWriter
dict<SigBit, int> init_inputs;
int initstate_ff = 0;
+ dict<SigBit, int> ywmap_clocks;
+
int mkgate(int a0, int a1)
{
aig_m++, aig_a++;
@@ -159,6 +164,17 @@ struct AigerWriter
output_bits.insert(wirebit);
}
}
+
+ if (wire->width == 1) {
+ auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
+ if (gclk_attr != wire->attributes.end()) {
+ SigBit bit = sigmap(wire);
+ if (gclk_attr->second == State::S1)
+ ywmap_clocks[bit] |= 1;
+ else if (gclk_attr->second == State::S0)
+ ywmap_clocks[bit] |= 2;
+ }
+ }
}
for (auto bit : input_bits)
@@ -186,6 +202,22 @@ struct AigerWriter
unused_bits.erase(D);
undriven_bits.erase(Q);
ff_map[Q] = D;
+
+ if (cell->type != ID($_FF_)) {
+ auto sig_clk = sigmap(cell->getPort(ID::C).as_bit());
+ ywmap_clocks[sig_clk] |= cell->type == ID($_DFF_N_) ? 2 : 1;
+ }
+ continue;
+ }
+
+ if (cell->type == ID($anyinit))
+ {
+ auto sig_d = sigmap(cell->getPort(ID::D));
+ auto sig_q = sigmap(cell->getPort(ID::Q));
+ for (int i = 0; i < sig_d.size(); i++) {
+ undriven_bits.erase(sig_q[i]);
+ ff_map[sig_q[i]] = sig_d[i];
+ }
continue;
}
@@ -678,6 +710,121 @@ struct AigerWriter
for (auto &it : wire_lines)
f << it.second;
}
+
+ void write_ywmap(PrettyJson &json)
+ {
+ json.begin_object();
+ json.entry("version", "Yosys Witness Aiger map");
+ json.entry("gennerator", yosys_version_str);
+
+ 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())
+ {
+ if (cell->type.in(ID($_FF_), ID($_DFF_N_), ID($_DFF_P_), ID($anyinit), ID($anyconst), ID($anyseq)))
+ {
+ // Use sig_q to get the FF output name, but sig to lookup aiger bits
+ auto sig_qy = cell->getPort(cell->type.in(ID($anyconst), ID($anyseq)) ? ID::Y : ID::Q);
+ SigSpec sig = sigmap(sig_qy);
+
+ for (int i = 0; i < GetSize(sig_qy); i++) {
+ if (sig_qy[i].wire == nullptr || sig[i].wire == nullptr)
+ continue;
+
+ auto wire = sig_qy[i].wire;
+
+ 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 {
+ { "path", witness_path(wire) },
+ { "input", (a >> 1) - 1 },
+ { "offset", sig_qy[i].offset },
+ });
+ }
+
+ 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 {
+ { "path", witness_path(wire) },
+ { "input", (a >> 1) - 1 },
+ { "offset", sig_qy[i].offset },
+ });
+ }
+ }
+ }
+ }
+
+ for (auto wire : module->wires())
+ {
+ SigSpec sig = sigmap(wire);
+ if (wire->port_input)
+ {
+ auto path = witness_path(wire);
+ for (int i = 0; i < GetSize(wire); i++) {
+ if (aig_map.count(sig[i]) == 0 || sig[i].wire == nullptr)
+ continue;
+
+ int a = aig_map.at(sig[i]);
+ log_assert((a & 1) == 0);
+ input_lines[a] = json11::Json(json11::Json::object {
+ { "path", path },
+ { "input", (a >> 1) - 1 },
+ { "offset", i },
+ });
+
+ 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 {
+ { "path", path },
+ { "input", (a >> 1) - 1 },
+ { "offset", i },
+ { "edge", clock_mode == 1 ? "posedge" : "negedge" },
+ });
+ }
+ }
+ }
+ }
+ }
+
+ json.name("clocks");
+ json.begin_array();
+ clock_lines.sort();
+ for (auto &it : clock_lines)
+ json.value(it.second);
+ json.end_array();
+
+ json.name("inputs");
+ json.begin_array();
+ input_lines.sort();
+ for (auto &it : input_lines)
+ json.value(it.second);
+ json.end_array();
+
+ json.name("seqs");
+ json.begin_array();
+ input_lines.sort();
+ for (auto &it : seq_lines)
+ json.value(it.second);
+ json.end_array();
+
+ json.name("inits");
+ json.begin_array();
+ input_lines.sort();
+ for (auto &it : init_lines)
+ json.value(it.second);
+ json.end_array();
+ json.end_object();
+ }
+
};
struct AigerBackend : public Backend {
@@ -717,6 +864,9 @@ struct AigerBackend : public Backend {
log(" -no-startoffset\n");
log(" make indexes zero based, enable using map files with smt solvers.\n");
log("\n");
+ log(" -ywmap <filename>\n");
+ log(" write a map file for conversion to and from yosys witness traces.\n");
+ log("\n");
log(" -I, -O, -B, -L\n");
log(" If the design contains no input/output/assert/flip-flop then create one\n");
log(" dummy input/output/bad_state-pin or latch to make the tools reading the\n");
@@ -736,6 +886,7 @@ struct AigerBackend : public Backend {
bool lmode = false;
bool no_startoffset = false;
std::string map_filename;
+ std::string yw_map_filename;
log_header(design, "Executing AIGER backend.\n");
@@ -767,6 +918,10 @@ struct AigerBackend : public Backend {
verbose_map = true;
continue;
}
+ if (yw_map_filename.empty() && args[argidx] == "-ywmap" && argidx+1 < args.size()) {
+ yw_map_filename = args[++argidx];
+ continue;
+ }
if (args[argidx] == "-no-startoffset") {
no_startoffset = true;
continue;
@@ -791,6 +946,9 @@ struct AigerBackend : public Backend {
}
extra_args(f, filename, args, argidx, !ascii_mode);
+ if (!yw_map_filename.empty() && !zinit_mode)
+ log_error("Currently -ywmap requires -zinit.\n");
+
Module *top_module = design->top_module();
if (top_module == nullptr)
@@ -815,6 +973,17 @@ struct AigerBackend : public Backend {
log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
writer.write_map(mapf, verbose_map, no_startoffset);
}
+
+ if (!yw_map_filename.empty()) {
+ std::ofstream mapf;
+ mapf.open(yw_map_filename.c_str(), std::ofstream::trunc);
+
+ 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/blif/blif.cc b/backends/blif/blif.cc
index ba29d9090..23d1d58fc 100644
--- a/backends/blif/blif.cc
+++ b/backends/blif/blif.cc
@@ -512,8 +512,8 @@ struct BlifBackend : public Backend {
log(" suppresses the generation of this nets without fanout.\n");
log("\n");
log("The following options can be useful when the generated file is not going to be\n");
- log("read by a BLIF parser but a custom tool. It is recommended to not name the output\n");
- log("file *.blif when any of this options is used.\n");
+ log("read by a BLIF parser but a custom tool. It is recommended to not name the\n");
+ log("output file *.blif when any of this options is used.\n");
log("\n");
log(" -icells\n");
log(" do not translate Yosys's internal gates to generic BLIF logic\n");
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 5be9bf324..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) {
@@ -446,25 +508,28 @@ struct BtorWorker
goto okay;
}
- if (cell->type.in(ID($not), ID($neg), ID($_NOT_)))
+ if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos)))
{
string btor_op;
if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not";
if (cell->type == ID($neg)) btor_op = "neg";
- log_assert(!btor_op.empty());
int width = std::max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::Y)));
bool a_signed = cell->hasParam(ID::A_SIGNED) ? cell->getParam(ID::A_SIGNED).as_bool() : false;
-
- int sid = get_bv_sid(width);
int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
-
- int nid = next_nid++;
- btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
-
SigSpec sig = sigmap(cell->getPort(ID::Y));
+ // the $pos cell just passes through, all other cells need an actual operation applied
+ int nid = nid_a;
+ if (cell->type != ID($pos))
+ {
+ log_assert(!btor_op.empty());
+ int sid = get_bv_sid(width);
+ nid = next_nid++;
+ btorf("%d %s %d %d%s\n", nid, btor_op.c_str(), sid, nid_a, getinfo(cell).c_str());
+ }
+
if (GetSize(sig) < width) {
int sid = get_bv_sid(GetSize(sig));
int nid2 = next_nid++;
@@ -609,12 +674,12 @@ struct BtorWorker
goto okay;
}
- if (cell->type.in(ID($dff), ID($ff), ID($_DFF_P_), ID($_DFF_N), ID($_FF_)))
+ if (cell->type.in(ID($dff), ID($ff), ID($anyinit), ID($_DFF_P_), ID($_DFF_N), ID($_FF_)))
{
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);
@@ -626,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;
@@ -659,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)
@@ -680,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);
@@ -702,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);
@@ -765,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())
@@ -790,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++;
@@ -912,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()) {
@@ -990,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++)
@@ -1072,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;
@@ -1091,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)) {
@@ -1108,7 +1208,28 @@ 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()) {
+ auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
+ if (gclk_attr != wire->attributes.end()) {
+ if (gclk_attr->second == State::S1)
+ info_clocks[nid] |= 1;
+ else if (gclk_attr->second == State::S0)
+ 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");
@@ -1365,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();
+ }
}
};
@@ -1393,18 +1550,22 @@ 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");
log_push();
- Pass::call(design, "memory_map -rom-only");
Pass::call(design, "bmuxmap");
Pass::call(design, "demuxmap");
+ Pass::call(design, "bwmuxmap");
log_pop();
size_t argidx;
@@ -1430,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);
@@ -1442,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/cxxrtl/cxxrtl.h b/backends/cxxrtl/cxxrtl.h
index b4ffa87cd..073921cc4 100644
--- a/backends/cxxrtl/cxxrtl.h
+++ b/backends/cxxrtl/cxxrtl.h
@@ -1575,6 +1575,27 @@ value<BitsY> mod_ss(const value<BitsA> &a, const value<BitsB> &b) {
return divmod_ss<BitsY>(a, b).second;
}
+template<size_t BitsY, size_t BitsA, size_t BitsB>
+CXXRTL_ALWAYS_INLINE
+value<BitsY> modfloor_uu(const value<BitsA> &a, const value<BitsB> &b) {
+ return divmod_uu<BitsY>(a, b).second;
+}
+
+// GHDL Modfloor operator. Returns r=a mod b, such that r has the same sign as b and
+// a=b*N+r where N is some integer
+// In practical terms, when a and b have different signs and the remainder returned by divmod_ss is not 0
+// then return the remainder + b
+template<size_t BitsY, size_t BitsA, size_t BitsB>
+CXXRTL_ALWAYS_INLINE
+value<BitsY> modfloor_ss(const value<BitsA> &a, const value<BitsB> &b) {
+ value<BitsY> r;
+ r = divmod_ss<BitsY>(a, b).second;
+ if((b.is_neg() != a.is_neg()) && !r.is_zero())
+ return add_ss<BitsY>(b, r);
+ return r;
+}
+
+
// Memory helper
struct memory_index {
bool valid;
diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc
index 404755b1e..62768bd33 100644
--- a/backends/cxxrtl/cxxrtl_backend.cc
+++ b/backends/cxxrtl/cxxrtl_backend.cc
@@ -185,7 +185,7 @@ bool is_binary_cell(RTLIL::IdString type)
ID($and), ID($or), ID($xor), ID($xnor), ID($logic_and), ID($logic_or),
ID($shl), ID($sshl), ID($shr), ID($sshr), ID($shift), ID($shiftx),
ID($eq), ID($ne), ID($eqx), ID($nex), ID($gt), ID($ge), ID($lt), ID($le),
- ID($add), ID($sub), ID($mul), ID($div), ID($mod));
+ ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($modfloor));
}
bool is_extending_cell(RTLIL::IdString type)
diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc
index 370108444..7722d0c33 100644
--- a/backends/edif/edif.cc
+++ b/backends/edif/edif.cc
@@ -107,8 +107,8 @@ struct EdifBackend : public Backend {
log(" constant drivers first)\n");
log("\n");
log(" -gndvccy\n");
- log(" create \"GND\" and \"VCC\" cells with \"Y\" outputs. (the default is \"G\"\n");
- log(" for \"GND\" and \"P\" for \"VCC\".)\n");
+ log(" create \"GND\" and \"VCC\" cells with \"Y\" outputs. (the default is\n");
+ log(" \"G\" for \"GND\" and \"P\" for \"VCC\".)\n");
log("\n");
log(" -attrprop\n");
log(" create EDIF properties for cell attributes\n");
diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc
index 76ba77abb..eb30ab4b9 100644
--- a/backends/firrtl/firrtl.cc
+++ b/backends/firrtl/firrtl.cc
@@ -346,6 +346,12 @@ void emit_elaborated_extmodules(RTLIL::Design *design, std::ostream &f)
{
// Find the module corresponding to this instance.
auto modInstance = design->module(cell->type);
+ // Ensure that we actually have a module instance
+ if (modInstance == nullptr) {
+ log_error("Unknown cell type %s\n", cell->type.c_str());
+ return;
+ }
+
bool modIsBlackbox = modInstance->get_blackbox_attribute();
if (modIsBlackbox)
@@ -1215,6 +1221,7 @@ struct FirrtlBackend : public Backend {
Pass::call(design, "pmuxtree");
Pass::call(design, "bmuxmap");
Pass::call(design, "demuxmap");
+ Pass::call(design, "bwmuxmap");
namecache.clear();
autoid_counter = 0;
@@ -1237,6 +1244,9 @@ struct FirrtlBackend : public Backend {
if (top == nullptr)
top = last;
+ if (!top)
+ log_cmd_error("There is no top module in this design!\n");
+
std::string circuitFileinfo = getFileinfo(top);
*f << stringf("circuit %s: %s\n", make_id(top->name), circuitFileinfo.c_str());
diff --git a/backends/jny/jny.cc b/backends/jny/jny.cc
index d801b144c..0be11a52c 100644
--- a/backends/jny/jny.cc
+++ b/backends/jny/jny.cc
@@ -27,6 +27,8 @@
#include <algorithm>
#include <unordered_map>
#include <vector>
+#include <sstream>
+#include <iterator>
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
@@ -116,17 +118,17 @@ struct JnyWriter
_include_connections(connections), _include_attributes(attributes), _include_properties(properties)
{ }
- void write_metadata(Design *design, uint16_t indent_level = 0)
+ void write_metadata(Design *design, uint16_t indent_level = 0, std::string invk = "")
{
log_assert(design != nullptr);
design->sort();
f << "{\n";
+ f << " \"$schema\": \"https://raw.githubusercontent.com/YosysHQ/yosys/master/misc/jny.schema.json\",\n";
f << stringf(" \"generator\": \"%s\",\n", escape_string(yosys_version_str).c_str());
- // XXX(aki): Replace this with a proper version info eventually:tm:
- f << " \"version\": \"0.0.0\",\n";
-
+ f << " \"version\": \"0.0.1\",\n";
+ f << " \"invocation\": \"" << escape_string(invk) << "\",\n";
f << " \"features\": [";
size_t fnum{0};
@@ -409,11 +411,12 @@ struct JnyWriter
struct JnyBackend : public Backend {
JnyBackend() : Backend("jny", "generate design metadata") { }
void help() override {
- // XXX(aki): TODO: explicitly document the JSON schema
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log(" jny [options] [selection]\n");
log("\n");
+ log("Write JSON netlist metadata for the current design\n");
+ log("\n");
log(" -no-connections\n");
log(" Don't include connection information in the netlist output.\n");
log("\n");
@@ -423,8 +426,8 @@ struct JnyBackend : public Backend {
log(" -no-properties\n");
log(" Don't include property information in the netlist output.\n");
log("\n");
- log("Write a JSON metadata for the current design\n");
- log("\n");
+ log("The JSON schema for JNY output files is located in the \"jny.schema.json\" file\n");
+ log("which is located at \"https://raw.githubusercontent.com/YosysHQ/yosys/master/misc/jny.schema.json\"\n");
log("\n");
}
@@ -453,12 +456,22 @@ struct JnyBackend : public Backend {
break;
}
+
+ // Compose invocation line
+ std::ostringstream invk;
+ if (!args.empty()) {
+ std::copy(args.begin(), args.end(),
+ std::ostream_iterator<std::string>(invk, " ")
+ );
+ }
+ invk << filename;
+
extra_args(f, filename, args, argidx);
log_header(design, "Executing jny backend.\n");
JnyWriter jny_writer(*f, false, connections, attributes, properties);
- jny_writer.write_metadata(design);
+ jny_writer.write_metadata(design, 0, invk.str());
}
} JnyBackend;
@@ -472,7 +485,7 @@ struct JnyPass : public Pass {
log("\n");
log(" jny [options] [selection]\n");
log("\n");
- log("Write a JSON netlist metadata for the current design\n");
+ log("Write JSON netlist metadata for the current design\n");
log("\n");
log(" -o <filename>\n");
log(" write to the specified file.\n");
@@ -520,12 +533,22 @@ struct JnyPass : public Pass {
break;
}
+
+ // Compose invocation line
+ std::ostringstream invk;
+ if (!args.empty()) {
+ std::copy(args.begin(), args.end(),
+ std::ostream_iterator<std::string>(invk, " ")
+ );
+ }
+
extra_args(args, argidx, design);
std::ostream *f;
std::stringstream buf;
+ bool empty = filename.empty();
- if (!filename.empty()) {
+ if (!empty) {
rewrite_filename(filename);
std::ofstream *ff = new std::ofstream;
ff->open(filename.c_str(), std::ofstream::trunc);
@@ -534,15 +557,16 @@ struct JnyPass : public Pass {
log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
}
f = ff;
+ invk << filename;
} else {
f = &buf;
}
JnyWriter jny_writer(*f, false, connections, attributes, properties);
- jny_writer.write_metadata(design);
+ jny_writer.write_metadata(design, 0, invk.str());
- if (!filename.empty()) {
+ if (!empty) {
delete f;
} else {
log("%s", buf.str().c_str());
diff --git a/backends/json/json.cc b/backends/json/json.cc
index 270d762ee..fd2c922fd 100644
--- a/backends/json/json.cc
+++ b/backends/json/json.cc
@@ -397,8 +397,8 @@ struct JsonBackend : public Backend {
log(" \"signed\": <1 if the port is signed>\n");
log(" }\n");
log("\n");
- log("The \"offset\" and \"upto\" fields are skipped if their value would be 0.");
- log("They don't affect connection semantics, and are only used to preserve original");
+ log("The \"offset\" and \"upto\" fields are skipped if their value would be 0.\n");
+ log("They don't affect connection semantics, and are only used to preserve original\n");
log("HDL bit indexing.");
log("And <cell_details> is:\n");
log("\n");
@@ -459,8 +459,8 @@ struct JsonBackend : public Backend {
log("connected to a constant driver are denoted as string \"0\", \"1\", \"x\", or\n");
log("\"z\" instead of a number.\n");
log("\n");
- log("Bit vectors (including integers) are written as string holding the binary");
- log("representation of the value. Strings are written as strings, with an appended");
+ log("Bit vectors (including integers) are written as string holding the binary\n");
+ log("representation of the value. Strings are written as strings, with an appended\n");
log("blank in cases of strings of the form /[01xz]* */.\n");
log("\n");
log("For example the following Verilog code:\n");
@@ -666,8 +666,9 @@ struct JsonPass : public Pass {
std::ostream *f;
std::stringstream buf;
+ bool empty = filename.empty();
- if (!filename.empty()) {
+ if (!empty) {
rewrite_filename(filename);
std::ofstream *ff = new std::ofstream;
ff->open(filename.c_str(), std::ofstream::trunc);
@@ -683,7 +684,7 @@ struct JsonPass : public Pass {
JsonWriter json_writer(*f, true, aig_mode, compat_int_mode);
json_writer.write_design(design);
- if (!filename.empty()) {
+ if (!empty) {
delete f;
} else {
log("%s", buf.str().c_str());
diff --git a/backends/protobuf/.gitignore b/backends/protobuf/.gitignore
deleted file mode 100644
index 849b38d45..000000000
--- a/backends/protobuf/.gitignore
+++ /dev/null
@@ -1,2 +0,0 @@
-yosys.pb.cc
-yosys.pb.h
diff --git a/backends/protobuf/Makefile.inc b/backends/protobuf/Makefile.inc
deleted file mode 100644
index 9cac9dcaa..000000000
--- a/backends/protobuf/Makefile.inc
+++ /dev/null
@@ -1,10 +0,0 @@
-ifeq ($(ENABLE_PROTOBUF),1)
-
-backends/protobuf/yosys.pb.cc backends/protobuf/yosys.pb.h: misc/yosys.proto
- $(Q) cd misc && protoc --cpp_out "../backends/protobuf" yosys.proto
-
-backends/protobuf/protobuf.cc: backends/protobuf/yosys.pb.h
-
-OBJS += backends/protobuf/protobuf.o backends/protobuf/yosys.pb.o
-
-endif
diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc
deleted file mode 100644
index 384ce2e8e..000000000
--- a/backends/protobuf/protobuf.cc
+++ /dev/null
@@ -1,371 +0,0 @@
-/*
- * yosys -- Yosys Open SYnthesis Suite
- *
- * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
- * Copyright (C) 2018 Serge Bazanski <q3k@symbioticeda.com>
- *
- * 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 <google/protobuf/text_format.h>
-
-#include "kernel/rtlil.h"
-#include "kernel/register.h"
-#include "kernel/sigtools.h"
-#include "kernel/celltypes.h"
-#include "kernel/cellaigs.h"
-#include "kernel/log.h"
-#include "yosys.pb.h"
-
-USING_YOSYS_NAMESPACE
-PRIVATE_NAMESPACE_BEGIN
-
-struct ProtobufDesignSerializer
-{
- bool aig_mode_;
- bool use_selection_;
- yosys::pb::Design *pb_;
-
- Design *design_;
- Module *module_;
-
- SigMap sigmap_;
- int sigidcounter_;
- dict<SigBit, uint64_t> sigids_;
- pool<Aig> aig_models_;
-
-
- ProtobufDesignSerializer(bool use_selection, bool aig_mode) :
- aig_mode_(aig_mode), use_selection_(use_selection) { }
-
- string get_name(IdString name)
- {
- return RTLIL::unescape_id(name);
- }
-
-
- void serialize_parameters(google::protobuf::Map<std::string, yosys::pb::Parameter> *out,
- const dict<IdString, Const> &parameters)
- {
- for (auto &param : parameters) {
- std::string key = get_name(param.first);
-
-
- yosys::pb::Parameter pb_param;
-
- if ((param.second.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0) {
- pb_param.set_str(param.second.decode_string());
- } else if (GetSize(param.second.bits) > 64) {
- pb_param.set_str(param.second.as_string());
- } else {
- pb_param.set_int_(param.second.as_int());
- }
-
- (*out)[key] = pb_param;
- }
- }
-
- void get_bits(yosys::pb::BitVector *out, SigSpec sig)
- {
- for (auto bit : sigmap_(sig)) {
- auto sig = out->add_signal();
-
- // Constant driver.
- if (bit.wire == nullptr) {
- if (bit == State::S0) sig->set_constant(sig->CONSTANT_DRIVER_LOW);
- else if (bit == State::S1) sig->set_constant(sig->CONSTANT_DRIVER_HIGH);
- else if (bit == State::Sz) sig->set_constant(sig->CONSTANT_DRIVER_Z);
- else sig->set_constant(sig->CONSTANT_DRIVER_X);
- continue;
- }
-
- // Signal - give it a unique identifier.
- if (sigids_.count(bit) == 0) {
- sigids_[bit] = sigidcounter_++;
- }
- sig->set_id(sigids_[bit]);
- }
- }
-
- void serialize_module(yosys::pb::Module* out, Module *module)
- {
- module_ = module;
- log_assert(module_->design == design_);
- sigmap_.set(module_);
- sigids_.clear();
- sigidcounter_ = 0;
-
- serialize_parameters(out->mutable_attribute(), module_->attributes);
-
- for (auto n : module_->ports) {
- Wire *w = module->wire(n);
- if (use_selection_ && !module_->selected(w))
- continue;
-
- yosys::pb::Module::Port pb_port;
- pb_port.set_direction(w->port_input ? w->port_output ?
- yosys::pb::DIRECTION_INOUT : yosys::pb::DIRECTION_INPUT : yosys::pb::DIRECTION_OUTPUT);
- get_bits(pb_port.mutable_bits(), w);
- (*out->mutable_port())[get_name(n)] = pb_port;
- }
-
- for (auto c : module_->cells()) {
- if (use_selection_ && !module_->selected(c))
- continue;
-
- yosys::pb::Module::Cell pb_cell;
- pb_cell.set_hide_name(c->name[0] == '$');
- pb_cell.set_type(get_name(c->type));
-
- if (aig_mode_) {
- Aig aig(c);
- if (aig.name.empty())
- continue;
- pb_cell.set_model(aig.name);
- aig_models_.insert(aig);
- }
- serialize_parameters(pb_cell.mutable_parameter(), c->parameters);
- serialize_parameters(pb_cell.mutable_attribute(), c->attributes);
-
- if (c->known()) {
- for (auto &conn : c->connections()) {
- yosys::pb::Direction direction = yosys::pb::DIRECTION_OUTPUT;
- if (c->input(conn.first))
- direction = c->output(conn.first) ? yosys::pb::DIRECTION_INOUT : yosys::pb::DIRECTION_INPUT;
- (*pb_cell.mutable_port_direction())[get_name(conn.first)] = direction;
- }
- }
- for (auto &conn : c->connections()) {
- yosys::pb::BitVector vec;
- get_bits(&vec, conn.second);
- (*pb_cell.mutable_connection())[get_name(conn.first)] = vec;
- }
-
- (*out->mutable_cell())[get_name(c->name)] = pb_cell;
- }
-
- for (auto w : module_->wires()) {
- if (use_selection_ && !module_->selected(w))
- continue;
-
- auto netname = out->add_netname();
- netname->set_hide_name(w->name[0] == '$');
- get_bits(netname->mutable_bits(), w);
- serialize_parameters(netname->mutable_attributes(), w->attributes);
- }
- }
-
-
- void serialize_models(google::protobuf::Map<string, yosys::pb::Model> *models)
- {
- for (auto &aig : aig_models_) {
- yosys::pb::Model pb_model;
- for (auto &node : aig.nodes) {
- auto pb_node = pb_model.add_node();
- if (node.portbit >= 0) {
- if (node.inverter) {
- pb_node->set_type(pb_node->TYPE_NPORT);
- } else {
- pb_node->set_type(pb_node->TYPE_PORT);
- }
- auto port = pb_node->mutable_port();
- port->set_portname(log_id(node.portname));
- port->set_bitindex(node.portbit);
- } else if (node.left_parent < 0 && node.right_parent < 0) {
- if (node.inverter) {
- pb_node->set_type(pb_node->TYPE_TRUE);
- } else {
- pb_node->set_type(pb_node->TYPE_FALSE);
- }
- } else {
- if (node.inverter) {
- pb_node->set_type(pb_node->TYPE_NAND);
- } else {
- pb_node->set_type(pb_node->TYPE_AND);
- }
- auto gate = pb_node->mutable_gate();
- gate->set_left(node.left_parent);
- gate->set_right(node.right_parent);
- }
- for (auto &op : node.outports) {
- auto pb_op = pb_node->add_out_port();
- pb_op->set_name(log_id(op.first));
- pb_op->set_bit_index(op.second);
- }
- }
- (*models)[aig.name] = pb_model;
- }
- }
-
- void serialize_design(yosys::pb::Design *pb, Design *design)
- {
- GOOGLE_PROTOBUF_VERIFY_VERSION;
- pb_ = pb;
- pb_->Clear();
- pb_->set_creator(yosys_version_str);
-
- design_ = design;
- design_->sort();
-
- auto modules = use_selection_ ? design_->selected_modules() : design_->modules();
- for (auto mod : modules) {
- yosys::pb::Module pb_mod;
- serialize_module(&pb_mod, mod);
- (*pb->mutable_modules())[mod->name.str()] = pb_mod;
- }
-
- serialize_models(pb_->mutable_models());
- }
-};
-
-struct ProtobufBackend : public Backend {
- ProtobufBackend(): Backend("protobuf", "write design to a Protocol Buffer file") { }
- void help() override
- {
- // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
- log("\n");
- log(" write_protobuf [options] [filename]\n");
- log("\n");
- log("Write a JSON netlist of the current design.\n");
- log("\n");
- log(" -aig\n");
- log(" include AIG models for the different gate types\n");
- log("\n");
- log(" -text\n");
- log(" output protobuf in Text/ASCII representation\n");
- log("\n");
- log("The schema of the output Protocol Buffer is defined in misc/yosys.pb in the\n");
- log("Yosys source code distribution.\n");
- log("\n");
- }
- void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
- {
- bool aig_mode = false;
- bool text_mode = false;
-
- size_t argidx;
- for (argidx = 1; argidx < args.size(); argidx++) {
- if (args[argidx] == "-aig") {
- aig_mode = true;
- continue;
- }
- if (args[argidx] == "-text") {
- text_mode = true;
- continue;
- }
- break;
- }
- extra_args(f, filename, args, argidx, !text_mode);
-
- log_header(design, "Executing Protobuf backend.\n");
-
- yosys::pb::Design pb;
- ProtobufDesignSerializer serializer(false, aig_mode);
- serializer.serialize_design(&pb, design);
-
- if (text_mode) {
- string out;
- google::protobuf::TextFormat::PrintToString(pb, &out);
- *f << out;
- } else {
- pb.SerializeToOstream(f);
- }
- }
-} ProtobufBackend;
-
-struct ProtobufPass : public Pass {
- ProtobufPass() : Pass("protobuf", "write design in Protobuf format") { }
- void help() override
- {
- // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
- log("\n");
- log(" protobuf [options] [selection]\n");
- log("\n");
- log("Write a JSON netlist of all selected objects.\n");
- log("\n");
- log(" -o <filename>\n");
- log(" write to the specified file.\n");
- log("\n");
- log(" -aig\n");
- log(" include AIG models for the different gate types\n");
- log("\n");
- log(" -text\n");
- log(" output protobuf in Text/ASCII representation\n");
- log("\n");
- log("The schema of the output Protocol Buffer is defined in misc/yosys.pb in the\n");
- log("Yosys source code distribution.\n");
- log("\n");
- }
- void execute(std::vector<std::string> args, RTLIL::Design *design) override
- {
- std::string filename;
- bool aig_mode = false;
- bool text_mode = false;
-
- size_t argidx;
- for (argidx = 1; argidx < args.size(); argidx++)
- {
- if (args[argidx] == "-o" && argidx+1 < args.size()) {
- filename = args[++argidx];
- continue;
- }
- if (args[argidx] == "-aig") {
- aig_mode = true;
- continue;
- }
- if (args[argidx] == "-text") {
- text_mode = true;
- continue;
- }
- break;
- }
- extra_args(args, argidx, design);
-
- std::ostream *f;
- std::stringstream buf;
-
- if (!filename.empty()) {
- rewrite_filename(filename);
- std::ofstream *ff = new std::ofstream;
- ff->open(filename.c_str(), text_mode ? std::ofstream::trunc : (std::ofstream::trunc | std::ofstream::binary));
- if (ff->fail()) {
- delete ff;
- log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
- }
- f = ff;
- } else {
- f = &buf;
- }
-
- yosys::pb::Design pb;
- ProtobufDesignSerializer serializer(true, aig_mode);
- serializer.serialize_design(&pb, design);
-
- if (text_mode) {
- string out;
- google::protobuf::TextFormat::PrintToString(pb, &out);
- *f << out;
- } else {
- pb.SerializeToOstream(f);
- }
-
- if (!filename.empty()) {
- delete f;
- } else {
- log("%s", buf.str().c_str());
- }
- }
-} ProtobufPass;
-
-PRIVATE_NAMESPACE_END;
diff --git a/backends/rtlil/rtlil_backend.cc b/backends/rtlil/rtlil_backend.cc
index 1b11de5ec..574eb3aaa 100644
--- a/backends/rtlil/rtlil_backend.cc
+++ b/backends/rtlil/rtlil_backend.cc
@@ -51,7 +51,7 @@ void RTLIL_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int wi
}
}
f << stringf("%d'", width);
- if (data.is_fully_undef()) {
+ if (data.is_fully_undef_x_only()) {
f << "x";
} else {
for (int i = offset+width-1; i >= offset; i--) {
@@ -75,7 +75,7 @@ void RTLIL_BACKEND::dump_const(std::ostream &f, const RTLIL::Const &data, int wi
else if (str[i] == '\t')
f << stringf("\\t");
else if (str[i] < 32)
- f << stringf("\\%03o", str[i]);
+ f << stringf("\\%03o", (unsigned char)str[i]);
else if (str[i] == '"')
f << stringf("\\\"");
else if (str[i] == '\\')
@@ -530,8 +530,9 @@ struct DumpPass : public Pass {
std::ostream *f;
std::stringstream buf;
+ bool empty = filename.empty();
- if (!filename.empty()) {
+ if (!empty) {
rewrite_filename(filename);
std::ofstream *ff = new std::ofstream;
ff->open(filename.c_str(), append ? std::ofstream::app : std::ofstream::trunc);
@@ -546,7 +547,7 @@ struct DumpPass : public Pass {
RTLIL_BACKEND::dump_design(*f, design, true, flag_m, flag_n);
- if (!filename.empty()) {
+ if (!empty) {
delete f;
} else {
log("%s", buf.str().c_str());
diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc
index fb01308bd..3afe990e7 100644
--- a/backends/smt2/Makefile.inc
+++ b/backends/smt2/Makefile.inc
@@ -7,6 +7,7 @@ ifneq ($(CONFIG),emcc)
# MSYS targets support yosys-smtbmc, but require a launcher script
ifeq ($(CONFIG),$(filter $(CONFIG),msys2 msys2-64))
TARGETS += $(PROGRAM_PREFIX)yosys-smtbmc.exe $(PROGRAM_PREFIX)yosys-smtbmc-script.py
+TARGETS += $(PROGRAM_PREFIX)yosys-witness.exe $(PROGRAM_PREFIX)yosys-witness-script.py
# Needed to find the Python interpreter for yosys-smtbmc scripts.
# Override if necessary, it is only used for msys2 targets.
PYTHON := $(shell cygpath -w -m $(PREFIX)/bin/python3)
@@ -15,18 +16,31 @@ $(PROGRAM_PREFIX)yosys-smtbmc-script.py: backends/smt2/smtbmc.py
$(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' \
-e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
+$(PROGRAM_PREFIX)yosys-witness-script.py: backends/smt2/witness.py
+ $(P) sed -e 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' \
+ -e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
+
$(PROGRAM_PREFIX)yosys-smtbmc.exe: misc/launcher.c $(PROGRAM_PREFIX)yosys-smtbmc-script.py
$(P) $(CXX) -DGUI=0 -O -s -o $@ $<
+
+$(PROGRAM_PREFIX)yosys-witness.exe: misc/launcher.c $(PROGRAM_PREFIX)yosys-witness-script.py
+ $(P) $(CXX) -DGUI=0 -O -s -o $@ $<
# Other targets
else
-TARGETS += $(PROGRAM_PREFIX)yosys-smtbmc
+TARGETS += $(PROGRAM_PREFIX)yosys-smtbmc $(PROGRAM_PREFIX)yosys-witness
$(PROGRAM_PREFIX)yosys-smtbmc: backends/smt2/smtbmc.py
$(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' < $< > $@.new
$(Q) chmod +x $@.new
$(Q) mv $@.new $@
+
+$(PROGRAM_PREFIX)yosys-witness: backends/smt2/witness.py
+ $(P) sed 's|##yosys-sys-path##|sys.path += [os.path.dirname(os.path.realpath(__file__)) + p for p in ["/share/python3", "/../share/$(PROGRAM_PREFIX)yosys/python3"]]|;' < $< > $@.new
+ $(Q) chmod +x $@.new
+ $(Q) mv $@.new $@
endif
$(eval $(call add_share_file,share/python3,backends/smt2/smtio.py))
+$(eval $(call add_share_file,share/python3,backends/smt2/ywio.py))
endif
endif
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 6e70f9043..48da3f4be 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -23,6 +23,7 @@
#include "kernel/celltypes.h"
#include "kernel/log.h"
#include "kernel/mem.h"
+#include "libs/json11/json11.hpp"
#include <string>
USING_YOSYS_NAMESPACE
@@ -241,6 +242,17 @@ struct Smt2Worker
for (auto wire : module->wires())
{
+ auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
+ if (gclk_attr != wire->attributes.end()) {
+ if (gclk_attr->second == State::S1)
+ clock_posedge.insert(sigmap(wire));
+ else if (gclk_attr->second == State::S0)
+ clock_negedge.insert(sigmap(wire));
+ }
+ }
+
+ for (auto wire : module->wires())
+ {
if (!wire->port_input || GetSize(wire) != 1)
continue;
SigBit bit = sigmap(wire);
@@ -446,11 +458,14 @@ 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 == 'd' || type == 'b') {
- width = max(width, GetSize(cell->getPort(ID::A)));
+ if (type == 's' || type == 'S' || type == 'd' || type == 'b') {
+ if (type == 'b')
+ width = GetSize(cell->getPort(ID::A));
+ else
+ width = max(width, GetSize(cell->getPort(ID::A)));
if (cell->hasPort(ID::B))
width = max(width, GetSize(cell->getPort(ID::B)));
}
@@ -462,7 +477,7 @@ struct Smt2Worker
if (cell->hasPort(ID::B)) {
sig_b = cell->getPort(ID::B);
- sig_b.extend_u0(width, is_signed && !(type == 's'));
+ sig_b.extend_u0(width, (type == 'S') || (is_signed && !(type == 's')));
}
std::string processed_expr;
@@ -471,6 +486,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;
@@ -547,6 +563,9 @@ struct Smt2Worker
if (cell->type.in(ID($_FF_), ID($_DFF_P_), ID($_DFF_N_)))
{
registers.insert(cell);
+ SigBit q_bit = cell->getPort(ID::Q);
+ if (q_bit.is_wire())
+ decls.push_back(witness_signal("reg", 1, 0, "", idcounter, q_bit.wire));
makebits(stringf("%s#%d", get_id(module), idcounter), 0, log_signal(cell->getPort(ID::Q)));
register_bool(cell->getPort(ID::Q), idcounter++);
recursive_cells.erase(cell);
@@ -577,31 +596,44 @@ struct Smt2Worker
if (cell->type.in(ID($ff), ID($dff)))
{
registers.insert(cell);
+ int smtoffset = 0;
+ for (auto chunk : cell->getPort(ID::Q).chunks()) {
+ if (chunk.is_wire())
+ decls.push_back(witness_signal("reg", chunk.width, chunk.offset, "", idcounter, chunk.wire, smtoffset));
+ smtoffset += chunk.width;
+ }
makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Q)), log_signal(cell->getPort(ID::Q)));
register_bv(cell->getPort(ID::Q), idcounter++);
recursive_cells.erase(cell);
return;
}
- if (cell->type.in(ID($anyconst), ID($anyseq), ID($allconst), ID($allseq)))
+ if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq)))
{
+ auto QY = cell->type == ID($anyinit) ? ID::Q : ID::Y;
registers.insert(cell);
string infostr = cell->attributes.count(ID::src) ? cell->attributes.at(ID::src).decode_string().c_str() : get_id(cell);
if (cell->attributes.count(ID::reg))
infostr += " " + cell->attributes.at(ID::reg).decode_string();
- decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort(ID::Y)), infostr.c_str()));
- if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::maximize)){
+ decls.push_back(stringf("; yosys-smt2-%s %s#%d %d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, GetSize(cell->getPort(QY)), infostr.c_str()));
+ if (cell->getPort(QY).is_wire() && cell->getPort(QY).as_wire()->get_bool_attribute(ID::maximize)){
decls.push_back(stringf("; yosys-smt2-maximize %s#%d\n", get_id(module), idcounter));
- log("Wire %s is maximized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str());
+ log("Wire %s is maximized\n", cell->getPort(QY).as_wire()->name.str().c_str());
}
- else if (cell->getPort(ID::Y).is_wire() && cell->getPort(ID::Y).as_wire()->get_bool_attribute(ID::minimize)){
+ else if (cell->getPort(QY).is_wire() && cell->getPort(QY).as_wire()->get_bool_attribute(ID::minimize)){
decls.push_back(stringf("; yosys-smt2-minimize %s#%d\n", get_id(module), idcounter));
- log("Wire %s is minimized\n", cell->getPort(ID::Y).as_wire()->name.str().c_str());
+ log("Wire %s is minimized\n", cell->getPort(QY).as_wire()->name.str().c_str());
}
- makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(ID::Y)), log_signal(cell->getPort(ID::Y)));
+
+ bool init_only = cell->type.in(ID($anyconst), ID($anyinit), ID($allconst));
+ for (auto chunk : cell->getPort(QY).chunks())
+ if (chunk.is_wire())
+ decls.push_back(witness_signal(init_only ? "init" : "seq", chunk.width, chunk.offset, "", idcounter, chunk.wire));
+
+ makebits(stringf("%s#%d", get_id(module), idcounter), GetSize(cell->getPort(QY)), log_signal(cell->getPort(QY)));
if (cell->type == ID($anyseq))
ex_input_eq.push_back(stringf(" (= (|%s#%d| state) (|%s#%d| other_state))", get_id(module), idcounter, get_id(module), idcounter));
- register_bv(cell->getPort(ID::Y), idcounter++);
+ register_bv(cell->getPort(QY), idcounter++);
recursive_cells.erase(cell);
return;
}
@@ -611,6 +643,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');
@@ -619,8 +654,8 @@ struct Smt2Worker
if (cell->type.in(ID($shift), ID($shiftx))) {
if (cell->getParam(ID::B_SIGNED).as_bool()) {
return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) "
- "(bvlshr A B) (bvlshr A (bvneg B)))",
- GetSize(cell->getPort(ID::B)), 0), 's');
+ "(bvlshr A B) (bvshl A (bvneg B)))",
+ GetSize(cell->getPort(ID::B)), 0), 'S'); // type 'S' sign extends B
} else {
return export_bvop(cell, "(bvlshr A B)", 's');
}
@@ -748,6 +783,7 @@ struct Smt2Worker
log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module));
decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(mem->memid), abits, mem->width, GetSize(mem->rd_ports), GetSize(mem->wr_ports), has_async_wr ? "async" : "sync"));
+ decls.push_back(witness_memory(get_id(mem->memid), cell, mem));
string memstate;
if (has_async_wr) {
@@ -840,6 +876,7 @@ struct Smt2Worker
if (m != nullptr)
{
decls.push_back(stringf("; yosys-smt2-cell %s %s\n", get_id(cell->type), get_id(cell->name)));
+ decls.push_back(witness_cell(get_id(cell->name), cell));
string cell_state = stringf("(|%s_h %s| state)", get_id(module), get_id(cell->name));
for (auto &conn : cell->connections())
@@ -920,7 +957,7 @@ struct Smt2Worker
pool<SigBit> reg_bits;
for (auto cell : module->cells())
- if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_))) {
+ if (cell->type.in(ID($ff), ID($dff), ID($_FF_), ID($_DFF_P_), ID($_DFF_N_), ID($anyinit))) {
// not using sigmap -- we want the net directly at the dff output
for (auto bit : cell->getPort(ID::Q))
reg_bits.insert(bit);
@@ -938,14 +975,19 @@ struct Smt2Worker
for (auto wire : module->wires()) {
bool is_register = false;
- for (auto bit : SigSpec(wire))
+ bool contains_clock = false;
+ for (auto bit : SigSpec(wire)) {
if (reg_bits.count(bit))
is_register = true;
+ auto sig_bit = sigmap(bit);
+ if (clock_posedge.count(sig_bit) || clock_negedge.count(sig_bit))
+ contains_clock = true;
+ }
bool is_smtlib2_comb_expr = wire->has_attribute(ID::smtlib2_comb_expr);
if (is_smtlib2_comb_expr && !is_smtlib2_module)
log_error("smtlib2_comb_expr is only valid in a module with the smtlib2_module attribute: wire %s.%s", log_id(module),
log_id(wire));
- if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) {
+ if (wire->port_id || is_register || contains_clock || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) {
RTLIL::SigSpec sig = sigmap(wire);
std::vector<std::string> comments;
if (wire->port_input)
@@ -956,9 +998,20 @@ struct Smt2Worker
comments.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic()))
comments.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
- if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
+ 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 (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]);
+ if (is_posedge != is_negedge)
+ comments.push_back(witness_signal(
+ is_posedge ? "posedge" : "negedge", 1, i, get_id(wire), -1, wire));
+ }
+ }
+ if (wire->port_input)
+ comments.push_back(witness_signal("input", wire->width, 0, get_id(wire), -1, wire));
std::string smtlib2_comb_expr;
if (is_smtlib2_comb_expr) {
smtlib2_comb_expr =
@@ -968,6 +1021,8 @@ struct Smt2Worker
if (!bvmode && GetSize(sig) > 1)
log_error("smtlib2_comb_expr is unsupported on multi-bit wires when -nobv is specified: wire %s.%s",
log_id(module), log_id(wire));
+
+ comments.push_back(witness_signal("blackbox", wire->width, 0, get_id(wire), -1, wire));
}
auto &out_decls = is_smtlib2_comb_expr ? smtlib2_decls : decls;
if (bvmode && GetSize(sig) > 1) {
@@ -1136,7 +1191,7 @@ struct Smt2Worker
ex_state_eq.push_back(stringf("(= %s %s)", get_bool(cell->getPort(ID::Q)).c_str(), get_bool(cell->getPort(ID::Q), "other_state").c_str()));
}
- if (cell->type.in(ID($ff), ID($dff)))
+ if (cell->type.in(ID($ff), ID($dff), ID($anyinit)))
{
std::string expr_d = get_bv(cell->getPort(ID::D));
std::string expr_q = get_bv(cell->getPort(ID::Q), "next_state");
@@ -1435,6 +1490,91 @@ struct Smt2Worker
f << "true)";
f << stringf(" ; end of module %s\n", get_id(module));
}
+
+ 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;
+ }
+
+ std::string witness_signal(const char *type, int width, int offset, const std::string &smtname, int smtid, RTLIL::Wire *wire, int smtoffset = 0)
+ {
+ std::vector<std::string> hiername;
+ const char *wire_name = wire->name.c_str();
+ if (wire_name[0] == '\\') {
+ auto hdlname = wire->get_string_attribute(ID::hdlname);
+ for (auto token : split_tokens(hdlname))
+ hiername.push_back("\\" + token);
+ }
+ if (hiername.empty())
+ hiername.push_back(wire->name.str());
+
+ std::string line = "; yosys-smt2-witness ";
+ (json11::Json { json11::Json::object {
+ { "type", type },
+ { "offset", offset },
+ { "width", width },
+ { "smtname", smtname.empty() ? json11::Json(smtid) : json11::Json(smtname) },
+ { "smtoffset", smtoffset },
+ { "path", witness_path(wire) },
+ }}).dump(line);
+ line += "\n";
+ return line;
+ }
+
+ std::string witness_cell(const char *smtname, RTLIL::Cell *cell)
+ {
+ std::string line = "; yosys-smt2-witness ";
+ (json11::Json {json11::Json::object {
+ { "type", "cell" },
+ { "smtname", smtname },
+ { "path", witness_path(cell) },
+ }}).dump(line);
+ line += "\n";
+ return line;
+ }
+
+ std::string witness_memory(const char *smtname, RTLIL::Cell *cell, Mem *mem)
+ {
+ json11::Json::array uninitialized;
+ auto init_data = mem->get_init_data();
+
+ int cursor = 0;
+
+ while (cursor < init_data.size()) {
+ while (cursor < init_data.size() && init_data[cursor] != State::Sx)
+ cursor++;
+ int offset = cursor;
+ while (cursor < init_data.size() && init_data[cursor] == State::Sx)
+ cursor++;
+ int width = cursor - offset;
+ if (width)
+ uninitialized.push_back(json11::Json::object {
+ {"width", width},
+ {"offset", offset},
+ });
+ }
+
+ std::string line = "; yosys-smt2-witness ";
+ (json11::Json { json11::Json::object {
+ { "type", "mem" },
+ { "width", mem->width },
+ { "size", mem->size },
+ { "rom", mem->wr_ports.empty() },
+ { "statebv", statebv },
+ { "smtname", smtname },
+ { "uninitialized", uninitialized },
+ { "path", witness_path(cell) },
+ }}).dump(line);
+ line += "\n";
+ return line;
+ }
};
struct Smt2Backend : public Backend {
@@ -1609,7 +1749,6 @@ struct Smt2Backend : public Backend {
log_header(design, "Executing SMT2 backend.\n");
log_push();
- Pass::call(design, "memory_map -rom-only");
Pass::call(design, "bmuxmap");
Pass::call(design, "demuxmap");
log_pop();
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 137182f33..cb21eb3aa 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -17,9 +17,10 @@
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
#
-import os, sys, getopt, re
+import os, sys, getopt, re, bisect
##yosys-sys-path##
from smtio import SmtIo, SmtOpts, MkVcd
+from ywio import ReadWitness, WriteWitness, WitnessValues
from collections import defaultdict
got_topt = False
@@ -28,6 +29,8 @@ step_size = 1
num_steps = 20
append_steps = 0
vcdfile = None
+inywfile = None
+outywfile = None
cexfile = None
aimfile = None
aiwfile = None
@@ -51,6 +54,8 @@ smtctop = None
noinit = False
binarymode = False
keep_going = False
+check_witness = False
+detect_loops = False
so = SmtOpts()
@@ -94,6 +99,9 @@ def usage():
the AIGER witness file does not include the status and
properties lines.
+ --yw <yosys_witness_filename>
+ read a Yosys witness.
+
--btorwit <btor_witness_filename>
read a BTOR witness.
@@ -121,6 +129,9 @@ def usage():
(hint: use 'write_smt2 -wires' for maximum
coverage of signals in generated VCD file)
+ --dump-yw <yw_filename>
+ write trace as a Yosys witness trace
+
--dump-vlogtb <verilog_filename>
write trace as Verilog test bench
@@ -161,15 +172,23 @@ def usage():
covering all found failed assertions, the character '%' is
replaced in all dump filenames with an increasing number.
+ --check-witness
+ check that the used witness file contains sufficient
+ constraints to force an assertion failure.
+
+ --detect-loops
+ check if states are unique in temporal induction counter examples
+ (this feature is experimental and incomplete)
+
""" + so.helpmsg())
sys.exit(1)
try:
opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
- ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
- "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
- "smtc-init", "smtc-top=", "noinit", "binary", "keep-going"])
+ ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "yw=", "btorwit=", "presat",
+ "dump-vcd=", "dump-yw=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
+ "smtc-init", "smtc-top=", "noinit", "binary", "keep-going", "check-witness", "detect-loops"])
except:
usage()
@@ -204,10 +223,14 @@ for o, a in opts:
aiwfile = a + ".aiw"
elif o == "--aig-noheader":
aigheader = False
+ elif o == "--yw":
+ inywfile = a
elif o == "--btorwit":
btorwitfile = a
elif o == "--dump-vcd":
vcdfile = a
+ elif o == "--dump-yw":
+ outywfile = a
elif o == "--dump-vlogtb":
vlogtbfile = a
elif o == "--vlogtb-top":
@@ -244,6 +267,10 @@ for o, a in opts:
binarymode = True
elif o == "--keep-going":
keep_going = True
+ elif o == "--check-witness":
+ check_witness = True
+ elif o == "--detect-loops":
+ detect_loops = True
elif so.handle(o, a):
pass
else:
@@ -426,7 +453,6 @@ assert topmod in smt.modinfo
if cexfile is not None:
if not got_topt:
- assume_skipped = 0
skip_steps = 0
num_steps = 0
@@ -462,7 +488,8 @@ if cexfile is not None:
constr_assumes[step].append((cexfile, smtexpr))
if not got_topt:
- skip_steps = max(skip_steps, step)
+ if not check_witness:
+ skip_steps = max(skip_steps, step)
num_steps = max(num_steps, step+1)
if aimfile is not None:
@@ -471,7 +498,6 @@ if aimfile is not None:
latch_map = dict()
if not got_topt:
- assume_skipped = 0
skip_steps = 0
num_steps = 0
@@ -595,13 +621,118 @@ if aimfile is not None:
constr_assumes[step].append((cexfile, smtexpr))
if not got_topt:
- skip_steps = max(skip_steps, step)
+ if not check_witness:
+ skip_steps = max(skip_steps, step)
# some solvers optimize the properties so that they fail one cycle early,
# thus we check the properties in the cycle the aiger witness ends, and
# if that doesn't work, we check the cycle after that as well.
num_steps = max(num_steps, step+2)
step += 1
+if inywfile is not None:
+ if not got_topt:
+ skip_steps = 0
+ num_steps = 0
+
+ with open(inywfile, "r") as f:
+ inyw = ReadWitness(f)
+
+ inits, seqs, clocks, mems = smt.hierwitness(topmod, allregs=True, blackbox=True)
+
+ smt_wires = defaultdict(list)
+ smt_mems = defaultdict(list)
+
+ for wire in inits + seqs:
+ smt_wires[wire["path"]].append(wire)
+
+ for mem in mems:
+ smt_mems[mem["path"]].append(mem)
+
+ addr_re = re.compile(r'\\\[[0-9]+\]$')
+ bits_re = re.compile(r'[01?]*$')
+
+ for t, step in inyw.steps():
+ present_signals, missing = step.present_signals(inyw.sigmap)
+ for sig in present_signals:
+ bits = step[sig]
+ if not bits_re.match(bits):
+ raise ValueError("unsupported bit value in Yosys witness file")
+
+ sig_end = sig.offset + len(bits)
+ if sig.path in smt_wires:
+ for wire in smt_wires[sig.path]:
+ width, offset = wire["width"], wire["offset"]
+
+ smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1
+
+ offset = max(offset, 0)
+
+ end = width + offset
+ common_offset = max(sig.offset, offset)
+ common_end = min(sig_end, end)
+ if common_end <= common_offset:
+ continue
+
+ smt_expr = smt.witness_net_expr(topmod, f"s{t}", wire)
+
+ if not smt_bool:
+ slice_high = common_end - offset - 1
+ slice_low = common_offset - offset
+ smt_expr = "((_ extract %d %d) %s)" % (slice_high, slice_low, smt_expr)
+
+ bit_slice = bits[len(bits) - (common_end - sig.offset):len(bits) - (common_offset - sig.offset)]
+
+ if bit_slice.count("?") == len(bit_slice):
+ continue
+
+ if smt_bool:
+ assert width == 1
+ smt_constr = "(= %s %s)" % (smt_expr, "true" if bit_slice == "1" else "false")
+ else:
+ if "?" in bit_slice:
+ mask = bit_slice.replace("0", "1").replace("?", "0")
+ bit_slice = bit_slice.replace("?", "0")
+ smt_expr = "(bvand %s #b%s)" % (smt_expr, mask)
+
+ smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice)
+
+ constr_assumes[t].append((inywfile, smt_constr))
+
+ if sig.memory_path:
+ if sig.memory_path in smt_mems:
+ for mem in smt_mems[sig.memory_path]:
+ width, size, bv = mem["width"], mem["size"], mem["statebv"]
+
+ smt_expr = smt.net_expr(topmod, f"s{t}", mem["smtpath"])
+
+ if bv:
+ word_low = sig.memory_addr * width
+ word_high = word_low + width - 1
+ smt_expr = "((_ extract %d %d) %s)" % (word_high, word_low, smt_expr)
+ else:
+ addr_width = (size - 1).bit_length()
+ addr_bits = f"{sig.memory_addr:0{addr_width}b}"
+ smt_expr = "(select %s #b%s )" % (smt_expr, addr_bits)
+
+ if len(bits) < width:
+ slice_high = sig.offset + len(bits) - 1
+ smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr)
+
+ bit_slice = bits
+
+ if "?" in bit_slice:
+ mask = bit_slice.replace("0", "1").replace("?", "0")
+ bit_slice = bit_slice.replace("?", "0")
+ smt_expr = "(bvand %s #b%s)" % (smt_expr, mask)
+
+ smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice)
+ constr_assumes[t].append((inywfile, smt_constr))
+
+ if not got_topt:
+ if not check_witness:
+ skip_steps = max(skip_steps, t)
+ num_steps = max(num_steps, t+1)
+
if btorwitfile is not None:
with open(btorwitfile, "r") as f:
step = None
@@ -699,128 +830,137 @@ if btorwitfile is not None:
skip_steps = step
num_steps = step+1
-def write_vcd_trace(steps_start, steps_stop, index):
- filename = vcdfile.replace("%", index)
- print_msg("Writing trace to VCD file: %s" % (filename))
+def collect_mem_trace_data(steps_start, steps_stop, vcd=None):
+ mem_trace_data = dict()
- with open(filename, "w") as vcd_file:
- vcd = MkVcd(vcd_file)
- path_list = list()
+ for mempath in sorted(smt.hiermems(topmod)):
+ abits, width, rports, wports, asyncwr = smt.mem_info(topmod, mempath)
- for netpath in sorted(smt.hiernets(topmod)):
- hidden_net = False
- for n in netpath:
- if n.startswith("$"):
- hidden_net = True
- if not hidden_net:
- edge = smt.net_clock(topmod, netpath)
- if edge is None:
- vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath))
- else:
- vcd.add_clock([topmod] + netpath, edge)
- path_list.append(netpath)
+ expr_id = list()
+ expr_list = list()
+ for i in range(steps_start, steps_stop):
+ for j in range(rports):
+ expr_id.append(('R', i-steps_start, j, 'A'))
+ expr_id.append(('R', i-steps_start, j, 'D'))
+ expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j))
+ expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j))
+ for j in range(wports):
+ expr_id.append(('W', i-steps_start, j, 'A'))
+ expr_id.append(('W', i-steps_start, j, 'D'))
+ expr_id.append(('W', i-steps_start, j, 'M'))
+ expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dA" % j))
+ expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dD" % j))
+ expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dM" % j))
+
+ rdata = list()
+ wdata = list()
+ addrs = set()
+
+ for eid, edat in zip(expr_id, smt.get_list(expr_list)):
+ t, i, j, f = eid
+
+ if t == 'R':
+ c = rdata
+ elif t == 'W':
+ c = wdata
+ else:
+ assert False
- mem_trace_data = dict()
- for mempath in sorted(smt.hiermems(topmod)):
- abits, width, rports, wports, asyncwr = smt.mem_info(topmod, mempath)
+ while len(c) <= i:
+ c.append(list())
+ c = c[i]
- expr_id = list()
- expr_list = list()
- for i in range(steps_start, steps_stop):
- for j in range(rports):
- expr_id.append(('R', i-steps_start, j, 'A'))
- expr_id.append(('R', i-steps_start, j, 'D'))
- expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j))
- expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j))
- for j in range(wports):
- expr_id.append(('W', i-steps_start, j, 'A'))
- expr_id.append(('W', i-steps_start, j, 'D'))
- expr_id.append(('W', i-steps_start, j, 'M'))
- expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dA" % j))
- expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dD" % j))
- expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dM" % j))
-
- rdata = list()
- wdata = list()
- addrs = set()
-
- for eid, edat in zip(expr_id, smt.get_list(expr_list)):
- t, i, j, f = eid
-
- if t == 'R':
- c = rdata
- elif t == 'W':
- c = wdata
- else:
- assert False
+ while len(c) <= j:
+ c.append(dict())
+ c = c[j]
- while len(c) <= i:
- c.append(list())
- c = c[i]
+ c[f] = smt.bv2bin(edat)
- while len(c) <= j:
- c.append(dict())
- c = c[j]
+ if f == 'A':
+ addrs.add(c[f])
- c[f] = smt.bv2bin(edat)
+ for addr in addrs:
+ tdata = list()
+ data = ["x"] * width
+ gotread = False
- if f == 'A':
- addrs.add(c[f])
+ if len(wdata) == 0 and len(rdata) != 0:
+ wdata = [[]] * len(rdata)
- for addr in addrs:
- tdata = list()
- data = ["x"] * width
- gotread = False
+ assert len(rdata) == len(wdata)
- if len(wdata) == 0 and len(rdata) != 0:
- wdata = [[]] * len(rdata)
+ for i in range(len(wdata)):
+ if not gotread:
+ for j_data in rdata[i]:
+ if j_data["A"] == addr:
+ data = list(j_data["D"])
+ gotread = True
+ break
- assert len(rdata) == len(wdata)
+ if gotread:
+ buf = data[:]
+ for ii in reversed(range(len(tdata))):
+ for k in range(width):
+ if tdata[ii][k] == "x":
+ tdata[ii][k] = buf[k]
+ else:
+ buf[k] = tdata[ii][k]
- for i in range(len(wdata)):
- if not gotread:
- for j_data in rdata[i]:
- if j_data["A"] == addr:
- data = list(j_data["D"])
- gotread = True
- break
-
- if gotread:
- buf = data[:]
- for ii in reversed(range(len(tdata))):
- for k in range(width):
- if tdata[ii][k] == "x":
- tdata[ii][k] = buf[k]
- else:
- buf[k] = tdata[ii][k]
+ if not asyncwr:
+ tdata.append(data[:])
- if not asyncwr:
- tdata.append(data[:])
+ for j_data in wdata[i]:
+ if j_data["A"] != addr:
+ continue
- for j_data in wdata[i]:
- if j_data["A"] != addr:
- continue
+ D = j_data["D"]
+ M = j_data["M"]
- D = j_data["D"]
- M = j_data["M"]
+ for k in range(width):
+ if M[k] == "1":
+ data[k] = D[k]
- for k in range(width):
- if M[k] == "1":
- data[k] = D[k]
+ if asyncwr:
+ tdata.append(data[:])
- if asyncwr:
- tdata.append(data[:])
+ assert len(tdata) == len(rdata)
- assert len(tdata) == len(rdata)
+ int_addr = int(addr, 2)
- netpath = mempath[:]
- netpath[-1] += "<%0*x>" % ((len(addr)+3) // 4, int(addr, 2))
+ netpath = mempath[:]
+ if vcd:
+ netpath[-1] += "<%0*x>" % ((len(addr)+3) // 4, int_addr)
vcd.add_net([topmod] + netpath, width)
- for i in range(steps_start, steps_stop):
- if i not in mem_trace_data:
- mem_trace_data[i] = list()
- mem_trace_data[i].append((netpath, "".join(tdata[i-steps_start])))
+ for i in range(steps_start, steps_stop):
+ if i not in mem_trace_data:
+ mem_trace_data[i] = list()
+ mem_trace_data[i].append((netpath, int_addr, "".join(tdata[i-steps_start])))
+
+ return mem_trace_data
+
+def write_vcd_trace(steps_start, steps_stop, index):
+ filename = vcdfile.replace("%", index)
+ print_msg("Writing trace to VCD file: %s" % (filename))
+
+ with open(filename, "w") as vcd_file:
+ vcd = MkVcd(vcd_file)
+ path_list = list()
+
+ for netpath in sorted(smt.hiernets(topmod)):
+ hidden_net = False
+ for n in netpath:
+ if n.startswith("$"):
+ hidden_net = True
+ if not hidden_net:
+ edge = smt.net_clock(topmod, netpath)
+ if edge is None:
+ vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath))
+ else:
+ vcd.add_clock([topmod] + netpath, edge)
+ path_list.append(netpath)
+
+ mem_trace_data = collect_mem_trace_data(steps_start, steps_stop, vcd)
for i in range(steps_start, steps_stop):
vcd.set_time(i)
@@ -828,11 +968,35 @@ def write_vcd_trace(steps_start, steps_stop, index):
for path, value in zip(path_list, value_list):
vcd.set_net([topmod] + path, value)
if i in mem_trace_data:
- for path, value in mem_trace_data[i]:
+ for path, addr, value in mem_trace_data[i]:
vcd.set_net([topmod] + path, value)
vcd.set_time(steps_stop)
+def detect_state_loop(steps_start, steps_stop):
+ print_msg(f"Checking for loops in found induction counter example")
+ print_msg(f"This feature is experimental and incomplete")
+
+ path_list = sorted(smt.hiernets(topmod, regs_only=True))
+
+ mem_trace_data = collect_mem_trace_data(steps_start, steps_stop)
+
+ # Map state to index of step when it occurred
+ states = dict()
+
+ for i in range(steps_start, steps_stop):
+ value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i)
+ mem_state = sorted(
+ [(tuple(path), addr, data)
+ for path, addr, data in mem_trace_data.get(i, [])])
+ state = tuple(value_list), tuple(mem_state)
+ if state in states:
+ return (i, states[state])
+ else:
+ states[state] = i
+
+ return None
+
def char_ok_in_verilog(c,i):
if ('A' <= c <= 'Z'): return True
if ('a' <= c <= 'z'): return True
@@ -1072,8 +1236,73 @@ def write_constr_trace(steps_start, steps_stop, index):
for name, val in zip(pi_names, pi_values):
print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)
+def write_yw_trace(steps_start, steps_stop, index, allregs=False):
+ filename = outywfile.replace("%", index)
+ print_msg("Writing trace to Yosys witness file: %s" % (filename))
+
+ mem_trace_data = collect_mem_trace_data(steps_start, steps_stop)
+
+ with open(filename, "w") as f:
+ inits, seqs, clocks, mems = smt.hierwitness(topmod, allregs)
+
+ yw = WriteWitness(f, "smtbmc")
+
+ for clock in clocks:
+ yw.add_clock(clock["path"], clock["offset"], clock["type"])
+
+ for seq in seqs:
+ seq["sig"] = yw.add_sig(seq["path"], seq["offset"], seq["width"])
+
+ for init in inits:
+ init["sig"] = yw.add_sig(init["path"], init["offset"], init["width"], True)
+
+ inits = seqs + inits
+
+ mem_dict = {tuple(mem["smtpath"]): mem for mem in mems}
+ mem_init_values = []
+
+ for path, addr, value in mem_trace_data.get(0, ()):
+ json_mem = mem_dict.get(tuple(path))
+ if not json_mem:
+ continue
+
+ bit_addr = addr * json_mem["width"]
+ uninit_chunks = [(chunk["width"] + chunk["offset"], chunk["offset"]) for chunk in json_mem["uninitialized"]]
+ first_chunk_nr = bisect.bisect_left(uninit_chunks, (bit_addr + 1,))
-def write_trace(steps_start, steps_stop, index):
+ for uninit_end, uninit_offset in uninit_chunks[first_chunk_nr:]:
+ assert uninit_end > bit_addr
+ if uninit_offset > bit_addr + json_mem["width"]:
+ break
+
+ word_path = (*json_mem["path"], f"\\[{addr}]")
+
+ overlap_start = max(uninit_offset - bit_addr, 0)
+ overlap_end = min(uninit_end - bit_addr, json_mem["width"])
+ overlap_bits = value[len(value)-overlap_end:len(value)-overlap_start]
+
+ sig = yw.add_sig(word_path, overlap_start, overlap_end - overlap_start, True)
+ mem_init_values.append((sig, overlap_bits.replace("x", "?")))
+
+ for k in range(steps_start, steps_stop):
+ step_values = WitnessValues()
+
+ if k == steps_start:
+ for sig, value in mem_init_values:
+ step_values[sig] = value
+ sigs = inits + seqs
+ else:
+ sigs = seqs
+
+ for sig in sigs:
+ value = smt.bv2bin(smt.get(smt.witness_net_expr(topmod, f"s{k}", sig)))
+ step_values[sig["sig"]] = value
+ yw.step(step_values)
+
+ yw.end_trace()
+
+
+def write_trace(steps_start, steps_stop, index, allregs=False):
if vcdfile is not None:
write_vcd_trace(steps_start, steps_stop, index)
@@ -1083,6 +1312,9 @@ def write_trace(steps_start, steps_stop, index):
if outconstr is not None:
write_constr_trace(steps_start, steps_stop, index)
+ if outywfile is not None:
+ write_yw_trace(steps_start, steps_stop, index, allregs)
+
def print_failed_asserts_worker(mod, state, path, extrainfo, infomap, infokey=()):
assert mod in smt.modinfo
@@ -1392,12 +1624,16 @@ if tempind:
print_msg("Temporal induction failed!")
print_anyconsts(num_steps)
print_failed_asserts(num_steps)
- write_trace(step, num_steps+1, '%')
+ write_trace(step, num_steps+1, '%', allregs=True)
+ if detect_loops:
+ loop = detect_state_loop(step, num_steps+1)
+ if loop:
+ print_msg(f"Loop detected, increasing induction depth will not help. Step {loop[0]} = step {loop[1]}")
elif dumpall:
print_anyconsts(num_steps)
print_failed_asserts(num_steps)
- write_trace(step, num_steps+1, "%d" % step)
+ write_trace(step, num_steps+1, "%d" % step, allregs=True)
else:
print_msg("Temporal induction successful.")
@@ -1590,6 +1826,7 @@ else: # not tempind, covermode
smt_assert("(not %s)" % active_assert_expr)
else:
+ active_assert_expr = "true"
smt_assert("false")
@@ -1597,6 +1834,17 @@ else: # not tempind, covermode
if retstatus != "FAILED":
print("%s BMC failed!" % smt.timestamp())
+ if check_witness:
+ print_msg("Checking witness constraints...")
+ smt_pop()
+ smt_push()
+ smt_assert(active_assert_expr)
+ if smt_check_sat() != "sat":
+ retstatus = "PASSED"
+ check_witness = False
+ num_steps = -1
+ break
+
if append_steps > 0:
for i in range(last_check_step+1, last_check_step+1+append_steps):
print_msg("Appending additional step %d." % i)
@@ -1689,6 +1937,8 @@ else: # not tempind, covermode
print_anyconsts(0)
write_trace(0, num_steps, '%')
+ if check_witness:
+ retstatus = "FAILED"
smt.write("(exit)")
smt.wait()
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 91efc13a3..a73745896 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -16,7 +16,7 @@
# OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
#
-import sys, re, os, signal
+import sys, re, os, signal, json
import subprocess
if os.name == "posix":
import resource
@@ -108,6 +108,7 @@ class SmtModInfo:
self.allconsts = dict()
self.allseqs = dict()
self.asize = dict()
+ self.witness = []
class SmtIo:
@@ -337,7 +338,7 @@ class SmtIo:
def p_thread_main(self):
while True:
- data = self.p.stdout.readline().decode("ascii")
+ data = self.p.stdout.readline().decode("utf-8")
if data == "": break
self.p_queue.put(data)
self.p_queue.put("")
@@ -359,7 +360,7 @@ class SmtIo:
def p_write(self, data, flush):
assert self.p is not None
- self.p.stdin.write(bytes(data, "ascii"))
+ self.p.stdin.write(bytes(data, "utf-8"))
if flush: self.p.stdin.flush()
def p_read(self):
@@ -587,6 +588,11 @@ class SmtIo:
self.modinfo[self.curmod].allseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
+ if fields[1] == "yosys-smt2-witness":
+ data = json.loads(stmt.split(None, 2)[2])
+ if data.get("type") in ["cell", "mem", "posedge", "negedge", "input", "reg", "init", "seq", "blackbox"]:
+ self.modinfo[self.curmod].witness.append(data)
+
def hiernets(self, top, regs_only=False):
def hiernets_worker(nets, mod, cursor):
for netname in sorted(self.modinfo[mod].wsize.keys()):
@@ -658,6 +664,57 @@ class SmtIo:
hiermems_worker(mems, top, [])
return mems
+ def hierwitness(self, top, allregs=False, blackbox=True):
+ init_witnesses = []
+ seq_witnesses = []
+ clk_witnesses = []
+ mem_witnesses = []
+
+ def absolute(path, cursor, witness):
+ return {
+ **witness,
+ "path": path + tuple(witness["path"]),
+ "smtpath": cursor + [witness["smtname"]],
+ }
+
+ for witness in self.modinfo[top].witness:
+ if witness["type"] == "input":
+ seq_witnesses.append(absolute((), [], witness))
+ if witness["type"] in ("posedge", "negedge"):
+ clk_witnesses.append(absolute((), [], witness))
+
+ init_types = ["init"]
+ if allregs:
+ init_types.append("reg")
+
+ seq_types = ["seq"]
+ if blackbox:
+ seq_types.append("blackbox")
+
+ def worker(mod, path, cursor):
+ cell_paths = {}
+ for witness in self.modinfo[mod].witness:
+ if witness["type"] in init_types:
+ init_witnesses.append(absolute(path, cursor, witness))
+ if witness["type"] in seq_types:
+ seq_witnesses.append(absolute(path, cursor, witness))
+ if witness["type"] == "mem":
+ if allregs and not witness["rom"]:
+ width, size = witness["width"], witness["size"]
+ witness = {**witness, "uninitialized": [{"width": width * size, "offset": 0}]}
+ if not witness["uninitialized"]:
+ continue
+
+ mem_witnesses.append(absolute(path, cursor, witness))
+ if witness["type"] == "cell":
+ cell_paths[witness["smtname"]] = tuple(witness["path"])
+
+ for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
+ worker(celltype, path + cell_paths.get(cellname, ("?" + cellname,)), cursor + [cellname])
+
+ worker(top, (), [])
+ return init_witnesses, seq_witnesses, clk_witnesses, mem_witnesses
+
def read(self):
stmt = []
count_brackets = 0
@@ -790,31 +847,28 @@ class SmtIo:
return result
def parse(self, stmt):
- def worker(stmt):
- if stmt[0] == '(':
+ def worker(stmt, cursor=0):
+ while stmt[cursor] in [" ", "\t", "\r", "\n"]:
+ cursor += 1
+
+ if stmt[cursor] == '(':
expr = []
- cursor = 1
+ cursor += 1
while stmt[cursor] != ')':
- el, le = worker(stmt[cursor:])
+ el, cursor = worker(stmt, cursor)
expr.append(el)
- cursor += le
return expr, cursor+1
- if stmt[0] == '|':
+ if stmt[cursor] == '|':
expr = "|"
- cursor = 1
+ cursor += 1
while stmt[cursor] != '|':
expr += stmt[cursor]
cursor += 1
expr += "|"
return expr, cursor+1
- if stmt[0] in [" ", "\t", "\r", "\n"]:
- el, le = worker(stmt[1:])
- return el, le+1
-
expr = ""
- cursor = 0
while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
expr += stmt[cursor]
cursor += 1
@@ -887,6 +941,8 @@ class SmtIo:
assert mod in self.modinfo
if path[0] == "":
return base
+ if isinstance(path[0], int):
+ return "(|%s#%d| %s)" % (mod, path[0], base)
if path[0] in self.modinfo[mod].cells:
return "(|%s_h %s| %s)" % (mod, path[0], base)
if path[0] in self.modinfo[mod].wsize:
@@ -902,6 +958,15 @@ class SmtIo:
nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
return self.net_expr(nextmod, nextbase, path[1:])
+ def witness_net_expr(self, mod, base, witness):
+ net = self.net_expr(mod, base, witness["smtpath"])
+ is_bool = self.net_width(mod, witness["smtpath"]) == 1
+ if is_bool:
+ assert witness["width"] == 1
+ assert witness["smtoffset"] == 0
+ return net
+ return "((_ extract %d %d) %s)" % (witness["smtoffset"] + witness["width"] - 1, witness["smtoffset"], net)
+
def net_width(self, mod, net_path):
for i in range(len(net_path)-1):
assert mod in self.modinfo
@@ -909,6 +974,8 @@ class SmtIo:
mod = self.modinfo[mod].cells[net_path[i]]
assert mod in self.modinfo
+ if isinstance(net_path[-1], int):
+ return None
assert net_path[-1] in self.modinfo[mod].wsize
return self.modinfo[mod].wsize[net_path[-1]]
diff --git a/backends/smt2/witness.py b/backends/smt2/witness.py
new file mode 100644
index 000000000..8d0cc8112
--- /dev/null
+++ b/backends/smt2/witness.py
@@ -0,0 +1,410 @@
+#!/usr/bin/env python3
+#
+# 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.
+#
+
+import os, sys, itertools, re
+##yosys-sys-path##
+import json
+import click
+
+from ywio import ReadWitness, WriteWitness, WitnessSig, WitnessSigMap, WitnessValues, coalesce_signals
+
+@click.group()
+def cli():
+ pass
+
+
+@cli.command(help="""
+Display a Yosys witness trace in a human readable format.
+""")
+@click.argument("input", type=click.File("r"))
+def display(input):
+ click.echo(f"Reading Yosys witness trace {input.name!r}...")
+ inyw = ReadWitness(input)
+
+ def output():
+
+ yield click.style("*** RTLIL bit-order below may differ from source level declarations ***", fg="red")
+ if inyw.clocks:
+ yield click.style("=== Clock Signals ===", fg="blue")
+ for clock in inyw.clocks:
+ yield f" {clock['edge']} {WitnessSig(clock['path'], clock['offset']).pretty()}"
+
+ for t, values in inyw.steps():
+ if t:
+ yield click.style(f"=== Step {t} ===", fg="blue")
+ else:
+ yield click.style("=== Initial State ===", fg="blue")
+
+ step_prefix = click.style(f"#{t}", fg="bright_black")
+
+ signals, missing = values.present_signals(inyw.sigmap)
+
+ assert not missing
+
+ for sig in signals:
+ display_bits = values[sig].replace("?", click.style("?", fg="bright_black"))
+ yield f" {step_prefix} {sig.pretty()} = {display_bits}"
+ click.echo_via_pager([line + "\n" for line in output()])
+
+
+@cli.command(help="""
+Display statistics of a Yosys witness trace.
+""")
+@click.argument("input", type=click.File("r"))
+def stats(input):
+ click.echo(f"Reading Yosys witness trace {input.name!r}...")
+ inyw = ReadWitness(input)
+
+ total = 0
+
+ for t, values in inyw.steps():
+ click.echo(f"{t:5}: {len(values.values):8} bits")
+ total += len(values.values)
+
+ click.echo(f"total: {total:8} bits")
+
+
+@cli.command(help="""
+Transform a Yosys witness trace.
+
+Currently no transformations are implemented, so it is only useful for testing.
+""")
+@click.argument("input", type=click.File("r"))
+@click.argument("output", type=click.File("w"))
+def yw2yw(input, output):
+ click.echo(f"Copying yosys witness trace from {input.name!r} to {output.name!r}...")
+ inyw = ReadWitness(input)
+ outyw = WriteWitness(output, "yosys-witness yw2yw")
+
+ for clock in inyw.clocks:
+ outyw.add_clock(clock["path"], clock["offset"], clock["edge"])
+
+ for sig in inyw.signals:
+ outyw.add_sig(sig.path, sig.offset, sig.width, sig.init_only)
+
+ for t, values in inyw.steps():
+ outyw.step(values)
+
+ outyw.end_trace()
+
+ click.echo(f"Copied {outyw.t + 1} time steps.")
+
+
+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"]
+
+ self.clocks = data["clocks"]
+
+ self.sigmap = WitnessSigMap()
+ self.init_inputs = set(init["input"] for init in data["inits"])
+
+ for bit in data["inputs"] + data["seqs"] + data["inits"]:
+ self.sigmap.add_bit((tuple(bit["path"]), bit["offset"]), bit["input"])
+
+
+
+@cli.command(help="""
+Convert an AIGER witness trace into a Yosys witness trace.
+
+This requires a Yosys witness AIGER map file as generated by 'write_aiger -ywmap'.
+""")
+@click.argument("input", type=click.File("r"))
+@click.argument("mapfile", type=click.File("r"))
+@click.argument("output", type=click.File("w"))
+def aiw2yw(input, mapfile, output):
+ input_name = input.name
+ click.echo(f"Converting AIGER witness trace {input_name!r} to Yosys witness trace {output.name!r}...")
+ click.echo(f"Using Yosys witness AIGER map file {mapfile.name!r}")
+ aiger_map = AigerMap(mapfile)
+
+ header_lines = list(itertools.islice(input, 0, 2))
+
+ if len(header_lines) == 2 and header_lines[1][0] in ".bcjf":
+ status = header_lines[0].strip()
+ if status == "0":
+ raise click.ClickException(f"{input_name}: file contains no trace, the AIGER status is unsat")
+ elif status == "2":
+ raise click.ClickException(f"{input_name}: file contains no trace, the AIGER status is sat")
+ elif status != "1":
+ raise click.ClickException(f"{input_name}: unexpected data in AIGER witness file")
+ else:
+ input = itertools.chain(header_lines, input)
+
+ ffline = next(input, None)
+ if ffline is None:
+ raise click.ClickException(f"{input_name}: unexpected end of file")
+ ffline = ffline.strip()
+ if not re.match(r'[01x]*$', ffline):
+ raise click.ClickException(f"{input_name}: unexpected data in AIGER witness file")
+ if not re.match(r'[0]*$', ffline):
+ raise click.ClickException(f"{input_name}: non-default initial state not supported")
+
+ outyw = WriteWitness(output, 'yosys-witness aiw2yw')
+
+ for clock in aiger_map.clocks:
+ outyw.add_clock(clock["path"], clock["offset"], clock["edge"])
+
+ for (path, offset), id in aiger_map.sigmap.bit_to_id.items():
+ outyw.add_sig(path, offset, init_only=id in aiger_map.init_inputs)
+
+ missing = set()
+
+ while True:
+ inline = next(input, None)
+ if inline is None:
+ click.echo(f"Warning: {input_name}: file may be incomplete")
+ break
+ inline = inline.strip()
+ if inline in [".", "# DONE"]:
+ break
+ if inline.startswith("#"):
+ continue
+
+ if not re.match(r'[01x]*$', ffline):
+ raise click.ClickException(f"{input_name}: unexpected data in AIGER witness file")
+
+ if len(inline) != aiger_map.input_count:
+ raise click.ClickException(
+ f"{input_name}: {mapfile.name}: number of inputs does not match, "
+ f"{len(inline)} in witness, {aiger_map.input_count} in map file")
+
+ values = WitnessValues()
+ for i, v in enumerate(inline):
+ if v == "x" or outyw.t > 0 and i in aiger_map.init_inputs:
+ continue
+
+ try:
+ bit = aiger_map.sigmap.id_to_bit[i]
+ except IndexError:
+ bit = None
+ if bit is None:
+ missing.insert(i)
+
+ values[bit] = v
+
+ outyw.step(values)
+
+ outyw.end_trace()
+
+ if missing:
+ click.echo("The following AIGER inputs belong to unknown signals:")
+ click.echo(" " + " ".join(str(id) for id in sorted(missing)))
+
+ click.echo(f"Converted {outyw.t} time steps.")
+
+@cli.command(help="""
+Convert a Yosys witness trace into an AIGER witness trace.
+
+This requires a Yosys witness AIGER map file as generated by 'write_aiger -ywmap'.
+""")
+@click.argument("input", type=click.File("r"))
+@click.argument("mapfile", type=click.File("r"))
+@click.argument("output", type=click.File("w"))
+def yw2aiw(input, mapfile, output):
+ click.echo(f"Converting Yosys witness trace {input.name!r} to AIGER witness trace {output.name!r}...")
+ click.echo(f"Using Yosys witness AIGER map file {mapfile.name!r}")
+ aiger_map = AigerMap(mapfile)
+ inyw = ReadWitness(input)
+
+ print("1", file=output)
+ print("b0", file=output)
+ # TODO the b0 status isn't really accurate, but we don't have any better info here
+ print("0" * aiger_map.latch_count, file=output)
+
+ all_missing = set()
+
+ for t, step in inyw.steps():
+ bits, missing = step.pack_present(aiger_map.sigmap)
+ bits = bits[::-1].replace('?', 'x')
+ all_missing.update(missing)
+ bits += 'x' * (aiger_map.input_count - len(bits))
+ print(bits, file=output)
+
+ print(".", file=output)
+
+ if all_missing:
+ click.echo("The following signals are missing in the AIGER map file and will be dropped:")
+ for sig in coalesce_signals(WitnessSig(*bit) for bit in all_missing):
+ click.echo(" " + sig.pretty())
+
+
+ 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
new file mode 100644
index 000000000..39cfac41e
--- /dev/null
+++ b/backends/smt2/ywio.py
@@ -0,0 +1,393 @@
+#
+# 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.
+#
+
+import json, re
+
+from functools import total_ordering
+
+
+class PrettyJson:
+ def __init__(self, f):
+ self.f = f
+ self.indent = 0
+ self.state = ["value"]
+
+ def line(self):
+ indent = len(self.state) - bool(self.state and self.state[-1] == "value")
+ print("\n", end=" " * (2 * indent), file=self.f)
+
+ def raw(self, str):
+ print(end=str, file=self.f)
+
+ def begin_object(self):
+ self.begin_value()
+ self.raw("{")
+ self.state.append("object_first")
+
+ def begin_array(self):
+ self.begin_value()
+ self.raw("[")
+ self.state.append("array_first")
+
+ def end_object(self):
+ state = self.state.pop()
+ if state == "object":
+ self.line()
+ else:
+ assert state == "object_first"
+ self.raw("}")
+ self.end_value()
+
+ def end_array(self):
+ state = self.state.pop()
+ if state == "array":
+ self.line()
+ else:
+ assert state == "array_first"
+ self.raw("]")
+ self.end_value()
+
+ def name(self, name):
+ if self.state[-1] == "object_first":
+ self.state[-1] = "object"
+ else:
+ self.raw(",")
+ self.line()
+ json.dump(str(name), self.f)
+ self.raw(": ")
+ self.state.append("value")
+
+ def begin_value(self):
+ if self.state[-1] == "array_first":
+ self.line()
+ self.state[-1] = "array"
+ elif self.state[-1] == "array":
+ self.raw(",")
+ self.line()
+ else:
+ assert self.state.pop() == "value"
+
+ def end_value(self):
+ if not self.state:
+ print(file=self.f, flush=True)
+
+ def value(self, value):
+ self.begin_value()
+ json.dump(value, self.f)
+ self.end_value()
+
+ def entry(self, name, value):
+ self.name(name)
+ self.value(value)
+
+ def object(self, entries=None):
+ if isinstance(entries, dict):
+ entries = dict.items()
+ self.begin_object()
+ for name, value in entries:
+ self.entry(name, value)
+ self.end_object()
+
+ def array(self, values=None):
+ self.begin_array()
+ for value in values:
+ self.value(value)
+ self.end_array()
+
+
+addr_re = re.compile(r'\\\[[0-9]+\]$')
+public_name_re = re.compile(r"\\([a-zA-Z_][a-zA-Z0-9_]*(\[[0-9]+\])?|\[[0-9]+\])$")
+
+def pretty_name(id):
+ if public_name_re.match(id):
+ return id.lstrip("\\")
+ else:
+ return id
+
+def pretty_path(path):
+ out = ""
+ for name in path:
+ name = pretty_name(name)
+ if name.startswith("["):
+ out += name
+ continue
+ if out:
+ out += "."
+ if name.startswith("\\") or name.startswith("$"):
+ out += name + " "
+ else:
+ out += name
+
+ return out
+
+@total_ordering
+class WitnessSig:
+ def __init__(self, path, offset, width=1, init_only=False):
+ path = tuple(path)
+ self.path, self.width, self.offset, self.init_only = path, width, offset, init_only
+
+ self.memory_path = None
+ self.memory_addr = None
+
+ sort_path = path
+ sort_id = -1
+ if path and addr_re.match(path[-1]):
+ self.memory_path = sort_path = path[:-1]
+ self.memory_addr = sort_id = int(path[-1][2:-1])
+
+ self.sort_key = (init_only, sort_path, sort_id, offset, width)
+
+ def bits(self):
+ return ((self.path, i) for i in range(self.offset, self.offset + self.width))
+
+ def rev_bits(self):
+ return ((self.path, i) for i in reversed(range(self.offset, self.offset + self.width)))
+
+ def pretty(self):
+ if self.width > 1:
+ last_offset = self.offset + self.width - 1
+ return f"{pretty_path(self.path)}[{last_offset}:{self.offset}]"
+ else:
+ return f"{pretty_path(self.path)}[{self.offset}]"
+
+ def __eq__(self):
+ return self.sort_key
+
+ def __hash__(self):
+ return hash(self.sort_key)
+
+ def __lt__(self, other):
+ return self.sort_key < other.sort_key
+
+
+def coalesce_signals(signals, bits=None):
+ if bits is None:
+ bits = {}
+ for sig in signals:
+ for bit in sig.bits():
+ if sig.init_only:
+ bits.setdefault(bit, False)
+ else:
+ bits[bit] = True
+
+ active = None
+
+ out = []
+
+ for bit, not_init in sorted(bits.items()):
+ if active:
+ if active[0] == bit[0] and active[2] == bit[1] and active[3] == not_init:
+ active[2] += 1
+ else:
+ out.append(WitnessSig(active[0], active[1], active[2] - active[1], not active[3]))
+ active = None
+
+ if active is None:
+ active = [bit[0], bit[1], bit[1] + 1, not_init]
+
+ if active:
+ out.append(WitnessSig(active[0], active[1], active[2] - active[1], not active[3]))
+
+ return sorted(out)
+
+
+class WitnessSigMap:
+ def __init__(self, signals=[]):
+ self.signals = []
+
+ self.id_to_bit = []
+ self.bit_to_id = {}
+ self.bit_to_sig = {}
+
+ for sig in signals:
+ self.add_signal(sig)
+
+ def add_signal(self, sig):
+ self.signals.append(sig)
+ for bit in sig.bits():
+ self.add_bit(bit)
+ self.bit_to_sig[bit] = sig
+
+ def add_bit(self, bit, id=None):
+ if id is None:
+ id = len(self.id_to_bit)
+ self.id_to_bit.append(bit)
+ else:
+ if len(self.id_to_bit) <= id:
+ self.id_to_bit += [None] * (id - len(self.id_to_bit) + 1)
+ self.id_to_bit[id] = bit
+ self.bit_to_id[bit] = id
+
+
+class WitnessValues:
+ def __init__(self):
+ self.values = {}
+
+ def __setitem__(self, key, value):
+ if isinstance(key, tuple) and len(key) == 2:
+ if value != "?":
+ assert isinstance(value, str)
+ assert len(value) == 1
+ self.values[key] = value
+ else:
+ assert isinstance(key, WitnessSig)
+ assert key.width == len(value)
+ if isinstance(value, str):
+ value = reversed(value)
+ for bit, bit_value in zip(key.bits(), value):
+ if bit_value != "?":
+ self.values[bit] = bit_value
+
+ def __getitem__(self, key):
+ if isinstance(key, tuple) and len(key) == 2:
+ return self.values.get(key, "?")
+ else:
+ assert isinstance(key, WitnessSig)
+ return "".join([self.values.get(bit, "?") for bit in key.rev_bits()])
+
+ def pack_present(self, sigmap):
+ missing = []
+
+ max_id = max((sigmap.bit_to_id.get(bit, -1) for bit in self.values), default=-1)
+
+ vector = ["?"] * (max_id + 1)
+ for bit, bit_value in self.values.items():
+ id = sigmap.bit_to_id.get(bit, - 1)
+ if id < 0:
+ missing.append(bit)
+ else:
+ vector[max_id - sigmap.bit_to_id[bit]] = bit_value
+
+ return "".join(vector), missing
+
+ def pack(self, sigmap):
+ packed, missing = self.pack_present(sigmap)
+ if missing:
+ raise RuntimeError(f"Cannot pack bits {missing!r}")
+ return packed
+
+ def unpack(self, sigmap, bits):
+ for i, bit_value in enumerate(reversed(bits)):
+ if bit_value != "?":
+ self.values[sigmap.id_to_bit[i]] = bit_value
+
+ def present_signals(self, sigmap):
+ signals = set(sigmap.bit_to_sig.get(bit) for bit in self.values)
+ missing_signals = None in signals
+ if missing_signals:
+ signals.discard(None)
+
+ return sorted(signals), missing_signals
+
+
+class WriteWitness:
+ def __init__(self, f, generator):
+ self.out = PrettyJson(f)
+ self.t = 0
+ self.header_written = False
+ self.clocks = []
+ self.signals = []
+
+ self.out.begin_object()
+ self.out.entry("format", "Yosys Witness Trace")
+ self.out.entry("generator", generator)
+
+ def add_clock(self, path, offset, edge):
+ assert not self.header_written
+ self.clocks.append({
+ "path": path,
+ "edge": edge,
+ "offset": offset,
+ })
+
+ def add_sig(self, path, offset, width=1, init_only=False):
+ assert not self.header_written
+ sig = WitnessSig(path, offset, width, init_only)
+ self.signals.append(sig)
+ return sig
+
+ def write_header(self):
+ assert not self.header_written
+ self.header_written = True
+ self.out.name("clocks")
+ self.out.array(self.clocks)
+
+ self.signals = coalesce_signals(self.signals)
+ self.sigmap = WitnessSigMap(self.signals)
+
+ self.out.name("signals")
+ self.out.array({
+ "path": sig.path,
+ "width": sig.width,
+ "offset": sig.offset,
+ "init_only": sig.init_only,
+ } for sig in self.signals)
+
+ self.out.name("steps")
+ self.out.begin_array()
+
+ def step(self, values):
+ if not self.header_written:
+ self.write_header()
+
+ self.out.value({"bits": values.pack(self.sigmap)})
+
+ self.t += 1
+
+ def end_trace(self):
+ if not self.header_written:
+ self.write_header()
+ self.out.end_array()
+ self.out.end_object()
+
+
+class ReadWitness:
+ def __init__(self, f):
+ data = json.load(f)
+ if not isinstance(data, dict):
+ data = {}
+
+ data_format = data.get("format", "Unknown Format")
+
+ if data_format != "Yosys Witness Trace":
+ raise ValueError(f"unsupported format {data_format!r}")
+
+ self.clocks = data["clocks"]
+ for clock in self.clocks:
+ clock["path"] = tuple(clock["path"])
+
+ self.signals = [
+ WitnessSig(sig["path"], sig["offset"], sig["width"], sig["init_only"])
+ for sig in data["signals"]
+ ]
+
+ self.sigmap = WitnessSigMap(self.signals)
+
+ self.bits = [step["bits"] for step in data["steps"]]
+
+ def step(self, t):
+ values = WitnessValues()
+ values.unpack(self.sigmap, self.bits[t])
+ return values
+
+ def steps(self):
+ for i in range(len(self.bits)):
+ yield i, self.step(i)
+
+ def __len__(self):
+ return len(self.bits)
diff --git a/backends/smv/smv.cc b/backends/smv/smv.cc
index 7d4f94adc..49c2cc7a6 100644
--- a/backends/smv/smv.cc
+++ b/backends/smv/smv.cc
@@ -744,6 +744,7 @@ struct SmvBackend : 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/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index aa1d4558c..3da168960 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -35,7 +35,7 @@
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
-bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs;
+bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs, noparallelcase;
int auto_name_counter, auto_name_offset, auto_name_digits, extmem_counter;
std::map<RTLIL::IdString, int> auto_name_map;
std::set<RTLIL::IdString> reg_wires;
@@ -1209,7 +1209,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
if (cell->type == ID($modfloor))
{
// wire truncated = $signed(A) % $signed(B);
- // assign Y = (A[-1] == B[-1]) || truncated == 0 ? truncated : $signed(B) + $signed(truncated);
+ // assign Y = (A[-1] == B[-1]) || truncated == 0 ? $signed(truncated) : $signed(B) + $signed(truncated);
if (cell->getParam(ID::A_SIGNED).as_bool() && cell->getParam(ID::B_SIGNED).as_bool()) {
SigSpec sig_a = cell->getPort(ID::A);
@@ -1229,7 +1229,7 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
dump_sigspec(f, sig_a.extract(sig_a.size()-1));
f << stringf(" == ");
dump_sigspec(f, sig_b.extract(sig_b.size()-1));
- f << stringf(") || %s == 0 ? %s : ", temp_id.c_str(), temp_id.c_str());
+ f << stringf(") || %s == 0 ? $signed(%s) : ", temp_id.c_str(), temp_id.c_str());
dump_cell_expr_port(f, cell, "B", true);
f << stringf(" + $signed(%s);\n", temp_id.c_str());
return true;
@@ -1314,24 +1314,38 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
f << stringf("%s" " input [%d:0] s;\n", indent.c_str(), s_width-1);
dump_attributes(f, indent + " ", cell->attributes);
- if (!noattr)
- f << stringf("%s" " (* parallel_case *)\n", indent.c_str());
- f << stringf("%s" " casez (s)", indent.c_str());
- f << stringf(noattr ? " // synopsys parallel_case\n" : "\n");
+ if (noparallelcase)
+ f << stringf("%s" " case (s)\n", indent.c_str());
+ else {
+ if (!noattr)
+ f << stringf("%s" " (* parallel_case *)\n", indent.c_str());
+ f << stringf("%s" " casez (s)", indent.c_str());
+ f << stringf(noattr ? " // synopsys parallel_case\n" : "\n");
+ }
for (int i = 0; i < s_width; i++)
{
f << stringf("%s" " %d'b", indent.c_str(), s_width);
for (int j = s_width-1; j >= 0; j--)
- f << stringf("%c", j == i ? '1' : '?');
+ f << stringf("%c", j == i ? '1' : noparallelcase ? '0' : '?');
f << stringf(":\n");
f << stringf("%s" " %s = b[%d:%d];\n", indent.c_str(), func_name.c_str(), (i+1)*width-1, i*width);
}
- f << stringf("%s" " default:\n", indent.c_str());
+ if (noparallelcase) {
+ f << stringf("%s" " %d'b", indent.c_str(), s_width);
+ for (int j = s_width-1; j >= 0; j--)
+ f << '0';
+ f << stringf(":\n");
+ } else
+ f << stringf("%s" " default:\n", indent.c_str());
f << stringf("%s" " %s = a;\n", indent.c_str(), func_name.c_str());
+ if (noparallelcase) {
+ f << stringf("%s" " default:\n", indent.c_str());
+ f << stringf("%s" " %s = %d'bx;\n", indent.c_str(), func_name.c_str(), width);
+ }
f << stringf("%s" " endcase\n", indent.c_str());
f << stringf("%s" "endfunction\n", indent.c_str());
@@ -2136,6 +2150,11 @@ struct VerilogBackend : public Backend {
log(" without this option all internal cells are converted to Verilog\n");
log(" expressions.\n");
log("\n");
+ log(" -noparallelcase\n");
+ log(" With this option no parallel_case attributes are used. Instead, a case\n");
+ log(" statement that assigns don't-care values for priority dependent inputs\n");
+ log(" is generated.\n");
+ log("\n");
log(" -siminit\n");
log(" add initial statements with hierarchical refs to initialize FFs when\n");
log(" in -noexpr mode.\n");
@@ -2160,7 +2179,8 @@ struct VerilogBackend : public Backend {
log(" as binary numbers.\n");
log("\n");
log(" -simple-lhs\n");
- log(" Connection assignments with simple left hand side without concatenations.\n");
+ log(" Connection assignments with simple left hand side without\n");
+ log(" concatenations.\n");
log("\n");
log(" -extmem\n");
log(" instead of initializing memories using assignments to individual\n");
@@ -2210,6 +2230,7 @@ struct VerilogBackend : public Backend {
decimal = false;
siminit = false;
simple_lhs = false;
+ noparallelcase = false;
auto_prefix = "";
bool blackboxes = false;
@@ -2245,6 +2266,10 @@ struct VerilogBackend : public Backend {
noexpr = true;
continue;
}
+ if (arg == "-noparallelcase") {
+ noparallelcase = true;
+ continue;
+ }
if (arg == "-nodec") {
nodec = true;
continue;
@@ -2301,8 +2326,10 @@ struct VerilogBackend : public Backend {
}
log_push();
- Pass::call(design, "bmuxmap");
- Pass::call(design, "demuxmap");
+ if (!noexpr) {
+ Pass::call(design, "bmuxmap");
+ Pass::call(design, "demuxmap");
+ }
Pass::call(design, "clean_zerowidth");
log_pop();
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-06 11:56:42 +0000