aboutsummaryrefslogtreecommitdiffstats
path: root/backends/btor
diff options
context:
space:
mode:
authorJannis Harder <me@jix.one>2023-01-03 14:45:41 +0100
committerJannis Harder <me@jix.one>2023-01-11 18:07:16 +0100
commit636b9f27052ef67192ee55a862c31e57a1ccad79 (patch)
tree3d9177af1c3360c28a348a982245966b6aa1af00 /backends/btor
parent3e25e61778cc9fe427bf68f45de43f26985b12c3 (diff)
downloadyosys-636b9f27052ef67192ee55a862c31e57a1ccad79.tar.gz
yosys-636b9f27052ef67192ee55a862c31e57a1ccad79.tar.bz2
yosys-636b9f27052ef67192ee55a862c31e57a1ccad79.zip
Support for BTOR witness to Yosys witness conversion
Diffstat (limited to 'backends/btor')
-rw-r--r--backends/btor/btor.cc159
1 files changed, 153 insertions, 6 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 8368ab82d..4315f6f67 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -28,6 +28,7 @@
#include "kernel/celltypes.h"
#include "kernel/log.h"
#include "kernel/mem.h"
+#include "kernel/json.h"
#include <string>
USING_YOSYS_NAMESPACE
@@ -83,6 +84,20 @@ 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_clocks;
+
+ PrettyJson ywmap_json;
+
void btorf(const char *fmt, ...) YS_ATTRIBUTE(format(printf, 2, 3))
{
va_list ap;
@@ -126,6 +141,62 @@ struct BtorWorker
return " " + infostr;
}
+ template<class T> static std::vector<std::string> witness_path(T *obj) {
+ std::vector<std::string> path;
+ if (obj->name.isPublic()) {
+ auto hdlname = obj->get_string_attribute(ID::hdlname);
+ for (auto token : split_tokens(hdlname))
+ path.push_back("\\" + token);
+ }
+ if (path.empty())
+ path.push_back(obj->name.str());
+ return path;
+ }
+
+ void ywmap_state(const SigSpec &sig) {
+ if (ywmap_json.active())
+ ywmap_states.emplace_back(sig);
+ }
+
+ void ywmap_state(Cell *cell) {
+ if (ywmap_json.active())
+ ywmap_states.emplace_back(cell);
+ }
+
+ void ywmap_input(const SigSpec &sig) {
+ if (ywmap_json.active())
+ ywmap_inputs.emplace_back(sig);
+ }
+
+ void emit_ywmap_btor_sig(const ywmap_btor_sig &btor_sig) {
+ if (btor_sig.cell == nullptr) {
+ if (btor_sig.sig.empty()) {
+ ywmap_json.value(nullptr);
+ return;
+ }
+ ywmap_json.begin_array();
+ ywmap_json.compact();
+ for (auto &chunk : btor_sig.sig.chunks()) {
+ log_assert(chunk.is_wire());
+
+ ywmap_json.begin_object();
+ ywmap_json.entry("path", witness_path(chunk.wire));
+ ywmap_json.entry("width", chunk.width);
+ ywmap_json.entry("offset", chunk.offset);
+ ywmap_json.end_object();
+ }
+ ywmap_json.end_array();
+ } else {
+ ywmap_json.begin_object();
+ ywmap_json.compact();
+ ywmap_json.entry("path", witness_path(btor_sig.cell));
+ Mem *mem = mem_cells[btor_sig.cell];
+ ywmap_json.entry("width", mem->width);
+ ywmap_json.entry("size", mem->size);
+ ywmap_json.end_object();
+ }
+ }
+
void btorf_push(const string &id)
{
if (verbose) {
@@ -617,7 +688,7 @@ struct BtorWorker
SigSpec sig_d = sigmap(cell->getPort(ID::D));
SigSpec sig_q = sigmap(cell->getPort(ID::Q));
- if (!info_filename.empty() && cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)))
+ if ((!info_filename.empty() || ywmap_json.active()) && cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)))
{
SigSpec sig_c = sigmap(cell->getPort(cell->type == ID($dff) ? ID::CLK : ID::C));
int nid = get_sig_nid(sig_c);
@@ -629,7 +700,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_clocks[sig_c] |= negedge ? 2 : 1;
}
IdString symbol;
@@ -662,6 +737,8 @@ struct BtorWorker
else
btorf("%d state %d %s\n", nid, sid, log_id(symbol));
+ ywmap_state(sig_q);
+
if (nid_init_val >= 0) {
int nid_init = next_nid++;
if (verbose)
@@ -683,6 +760,8 @@ struct BtorWorker
btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str());
+ ywmap_state(sig_y);
+
if (cell->type == ID($anyconst)) {
int nid2 = next_nid++;
btorf("%d next %d %d %d\n", nid2, sid, nid, nid);
@@ -705,6 +784,8 @@ struct BtorWorker
btorf("%d state %d%s\n", initstate_nid, sid, getinfo(cell).c_str());
btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid);
+
+ ywmap_state(sig_y);
}
add_nid_sig(initstate_nid, sig_y);
@@ -768,6 +849,8 @@ struct BtorWorker
nid_init_val = next_nid++;
btorf("%d state %d\n", nid_init_val, sid);
+ ywmap_state(nullptr);
+
for (int i = 0; i < mem->size; i++) {
Const thisword = initdata.extract(i*mem->width, mem->width);
if (thisword.is_fully_undef())
@@ -793,6 +876,8 @@ struct BtorWorker
else
btorf("%d state %d %s\n", nid, sid, log_id(mem->memid));
+ ywmap_state(cell);
+
if (nid_init_val >= 0)
{
int nid_init = next_nid++;
@@ -915,10 +1000,13 @@ struct BtorWorker
int sid = get_bv_sid(GetSize(sig));
int nid_input = next_nid++;
- if (is_init)
+ if (is_init) {
btorf("%d state %d\n", nid_input, sid);
- else
+ ywmap_state(sig);
+ } else {
btorf("%d input %d\n", nid_input, sid);
+ ywmap_input(sig);
+ }
int nid_masked_input;
if (sig_mask_undef.is_fully_ones()) {
@@ -993,6 +1081,7 @@ struct BtorWorker
int sid = get_bv_sid(GetSize(s));
int nid = next_nid++;
btorf("%d input %d\n", nid, sid);
+ ywmap_input(s);
nid_width[nid] = GetSize(s);
for (int j = 0; j < GetSize(s); j++)
@@ -1075,12 +1164,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;
@@ -1111,6 +1203,7 @@ struct BtorWorker
int nid = next_nid++;
btorf("%d input %d%s\n", nid, sid, getinfo(wire).c_str());
+ ywmap_input(wire);
add_nid_sig(nid, sig);
if (!info_filename.empty()) {
@@ -1122,6 +1215,16 @@ struct BtorWorker
info_clocks[nid] |= 2;
}
}
+
+ if (ywmap_json.active()) {
+ auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
+ if (gclk_attr != wire->attributes.end()) {
+ if (gclk_attr->second == State::S1)
+ ywmap_clocks[sig] |= 1;
+ else if (gclk_attr->second == State::S0)
+ ywmap_clocks[sig] |= 2;
+ }
+ }
}
btorf_pop("inputs");
@@ -1378,6 +1481,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_clocks) {
+ if (entry.second != 1 && entry.second != 2)
+ continue;
+ log_assert(entry.first.is_wire());
+ ywmap_json.begin_object();
+ ywmap_json.compact();
+ ywmap_json.entry("path", witness_path(entry.first.wire));
+ ywmap_json.entry("offset", entry.first.offset);
+ ywmap_json.entry("edge", entry.second == 1 ? "posedge" : "negedge");
+ ywmap_json.end_object();
+ }
+ ywmap_json.end_array();
+
+ ywmap_json.name("inputs");
+ ywmap_json.begin_array();
+ for (auto &entry : ywmap_inputs)
+ emit_ywmap_btor_sig(entry);
+ ywmap_json.end_array();
+
+ ywmap_json.name("states");
+ ywmap_json.begin_array();
+ for (auto &entry : ywmap_states)
+ emit_ywmap_btor_sig(entry);
+ ywmap_json.end_array();
+
+ ywmap_json.end_object();
+ }
}
};
@@ -1406,11 +1545,15 @@ struct BtorBackend : public Backend {
log(" -x\n");
log(" Output symbols for internal netnames (starting with '$')\n");
log("\n");
+ log(" -ywmap <filename>\n");
+ log(" Create a map file for conversion to and from Yosys witness traces\n");
+ log("\n");
}
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
{
bool verbose = false, single_bad = false, cover_mode = false, print_internal_names = false;
string info_filename;
+ string ywmap_filename;
log_header(design, "Executing BTOR backend.\n");
@@ -1443,6 +1586,10 @@ struct BtorBackend : public Backend {
print_internal_names = true;
continue;
}
+ if (args[argidx] == "-ywmap" && argidx+1 < args.size()) {
+ ywmap_filename = args[++argidx];
+ continue;
+ }
break;
}
extra_args(f, filename, args, argidx);
@@ -1455,7 +1602,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");
}