mirror of
https://github.com/YosysHQ/yosys
synced 2025-06-06 06:03:23 +00:00
Merge pull request #3624 from jix/sim_yw
Changes to support SBY trace generation with the sim command
This commit is contained in:
Miodrag Milanović
GitHub
commit
8180cc4325
15 changed files with 1722 additions and 113 deletions
|
|
@ -19,6 +19,8 @@
|
|||
|
||||
#include "kernel/yosys.h"
|
||||
#include "kernel/sigtools.h"
|
||||
#include "kernel/json.h"
|
||||
#include "kernel/yw.h"
|
||||
#include "libs/json11/json11.hpp"
|
||||
|
||||
USING_YOSYS_NAMESPACE
|
||||
|
|
@ -709,30 +711,19 @@ struct AigerWriter
|
|||
f << it.second;
|
||||
}
|
||||
|
||||
template<class T> static std::vector<std::string> witness_path(T *obj) {
|
||||
std::vector<std::string> path;
|
||||
if (obj->name.isPublic()) {
|
||||
auto hdlname = obj->get_string_attribute(ID::hdlname);
|
||||
for (auto token : split_tokens(hdlname))
|
||||
path.push_back("\\" + token);
|
||||
}
|
||||
if (path.empty())
|
||||
path.push_back(obj->name.str());
|
||||
return path;
|
||||
}
|
||||
|
||||
void write_ywmap(std::ostream &f)
|
||||
void write_ywmap(PrettyJson &json)
|
||||
{
|
||||
f << "{\n";
|
||||
f << " \"version\": \"Yosys Witness Aiger Map\",\n";
|
||||
f << stringf(" \"generator\": %s,\n", json11::Json(yosys_version_str).dump().c_str());
|
||||
f << stringf(" \"latch_count\": %d,\n", aig_l);
|
||||
f << stringf(" \"input_count\": %d,\n", aig_i);
|
||||
json.begin_object();
|
||||
json.entry("version", "Yosys Witness Aiger map");
|
||||
json.entry("gennerator", yosys_version_str);
|
||||
|
||||
dict<int, string> clock_lines;
|
||||
dict<int, string> input_lines;
|
||||
dict<int, string> init_lines;
|
||||
dict<int, string> seq_lines;
|
||||
json.entry("latch_count", aig_l);
|
||||
json.entry("input_count", aig_i);
|
||||
|
||||
dict<int, Json> clock_lines;
|
||||
dict<int, Json> input_lines;
|
||||
dict<int, Json> init_lines;
|
||||
dict<int, Json> seq_lines;
|
||||
|
||||
for (auto cell : module->cells())
|
||||
{
|
||||
|
|
@ -751,21 +742,21 @@ struct AigerWriter
|
|||
if (init_inputs.count(sig[i])) {
|
||||
int a = init_inputs.at(sig[i]);
|
||||
log_assert((a & 1) == 0);
|
||||
init_lines[a] += json11::Json(json11::Json::object {
|
||||
init_lines[a] = json11::Json(json11::Json::object {
|
||||
{ "path", witness_path(wire) },
|
||||
{ "input", (a >> 1) - 1 },
|
||||
{ "offset", sig_qy[i].offset },
|
||||
}).dump();
|
||||
});
|
||||
}
|
||||
|
||||
if (input_bits.count(sig[i])) {
|
||||
int a = aig_map.at(sig[i]);
|
||||
log_assert((a & 1) == 0);
|
||||
seq_lines[a] += json11::Json(json11::Json::object {
|
||||
seq_lines[a] = json11::Json(json11::Json::object {
|
||||
{ "path", witness_path(wire) },
|
||||
{ "input", (a >> 1) - 1 },
|
||||
{ "offset", sig_qy[i].offset },
|
||||
}).dump();
|
||||
});
|
||||
}
|
||||
}
|
||||
}
|
||||
|
|
@ -783,60 +774,55 @@ struct AigerWriter
|
|||
|
||||
int a = aig_map.at(sig[i]);
|
||||
log_assert((a & 1) == 0);
|
||||
input_lines[a] += json11::Json(json11::Json::object {
|
||||
input_lines[a] = json11::Json(json11::Json::object {
|
||||
{ "path", path },
|
||||
{ "input", (a >> 1) - 1 },
|
||||
{ "offset", i },
|
||||
}).dump();
|
||||
});
|
||||
|
||||
if (ywmap_clocks.count(sig[i])) {
|
||||
int clock_mode = ywmap_clocks[sig[i]];
|
||||
if (clock_mode != 3) {
|
||||
clock_lines[a] += json11::Json(json11::Json::object {
|
||||
clock_lines[a] = json11::Json(json11::Json::object {
|
||||
{ "path", path },
|
||||
{ "input", (a >> 1) - 1 },
|
||||
{ "offset", i },
|
||||
{ "edge", clock_mode == 1 ? "posedge" : "negedge" },
|
||||
}).dump();
|
||||
});
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
f << " \"clocks\": [";
|
||||
json.name("clocks");
|
||||
json.begin_array();
|
||||
clock_lines.sort();
|
||||
const char *sep = "\n ";
|
||||
for (auto &it : clock_lines) {
|
||||
f << sep << it.second;
|
||||
sep = ",\n ";
|
||||
}
|
||||
f << "\n ],\n";
|
||||
for (auto &it : clock_lines)
|
||||
json.value(it.second);
|
||||
json.end_array();
|
||||
|
||||
f << " \"inputs\": [";
|
||||
json.name("inputs");
|
||||
json.begin_array();
|
||||
input_lines.sort();
|
||||
sep = "\n ";
|
||||
for (auto &it : input_lines) {
|
||||
f << sep << it.second;
|
||||
sep = ",\n ";
|
||||
}
|
||||
f << "\n ],\n";
|
||||
for (auto &it : input_lines)
|
||||
json.value(it.second);
|
||||
json.end_array();
|
||||
|
||||
f << " \"seqs\": [";
|
||||
sep = "\n ";
|
||||
for (auto &it : seq_lines) {
|
||||
f << sep << it.second;
|
||||
sep = ",\n ";
|
||||
}
|
||||
f << "\n ],\n";
|
||||
json.name("seqs");
|
||||
json.begin_array();
|
||||
input_lines.sort();
|
||||
for (auto &it : seq_lines)
|
||||
json.value(it.second);
|
||||
json.end_array();
|
||||
|
||||
f << " \"inits\": [";
|
||||
sep = "\n ";
|
||||
for (auto &it : init_lines) {
|
||||
f << sep << it.second;
|
||||
sep = ",\n ";
|
||||
}
|
||||
f << "\n ]\n}\n";
|
||||
json.name("inits");
|
||||
json.begin_array();
|
||||
input_lines.sort();
|
||||
for (auto &it : init_lines)
|
||||
json.value(it.second);
|
||||
json.end_array();
|
||||
json.end_object();
|
||||
}
|
||||
|
||||
};
|
||||
|
|
@ -991,9 +977,12 @@ struct AigerBackend : public Backend {
|
|||
if (!yw_map_filename.empty()) {
|
||||
std::ofstream mapf;
|
||||
mapf.open(yw_map_filename.c_str(), std::ofstream::trunc);
|
||||
if (mapf.fail())
|
||||
log_error("Can't open file `%s' for writing: %s\n", map_filename.c_str(), strerror(errno));
|
||||
writer.write_ywmap(mapf);
|
||||
|
||||
PrettyJson json;
|
||||
|
||||
if (!json.write_to_file(yw_map_filename))
|
||||
log_error("Can't open file `%s' for writing: %s\n", yw_map_filename.c_str(), strerror(errno));
|
||||
writer.write_ywmap(json);
|
||||
}
|
||||
}
|
||||
} AigerBackend;
|
||||
|
|
|
|||
|
|
@ -28,6 +28,8 @@
|
|||
#include "kernel/celltypes.h"
|
||||
#include "kernel/log.h"
|
||||
#include "kernel/mem.h"
|
||||
#include "kernel/json.h"
|
||||
#include "kernel/yw.h"
|
||||
#include <string>
|
||||
|
||||
USING_YOSYS_NAMESPACE
|
||||
|
|
@ -83,6 +85,22 @@ struct BtorWorker
|
|||
vector<string> info_lines;
|
||||
dict<int, int> info_clocks;
|
||||
|
||||
struct ywmap_btor_sig {
|
||||
SigSpec sig;
|
||||
Cell *cell = nullptr;
|
||||
|
||||
ywmap_btor_sig(const SigSpec &sig) : sig(sig) {}
|
||||
ywmap_btor_sig(Cell *cell) : cell(cell) {}
|
||||
};
|
||||
|
||||
vector<ywmap_btor_sig> ywmap_inputs;
|
||||
vector<ywmap_btor_sig> ywmap_states;
|
||||
dict<SigBit, int> ywmap_clock_bits;
|
||||
dict<SigBit, int> ywmap_clock_inputs;
|
||||
|
||||
|
||||
PrettyJson ywmap_json;
|
||||
|
||||
void btorf(const char *fmt, ...) YS_ATTRIBUTE(format(printf, 2, 3))
|
||||
{
|
||||
va_list ap;
|
||||
|
|
@ -126,6 +144,50 @@ struct BtorWorker
|
|||
return " " + infostr;
|
||||
}
|
||||
|
||||
void ywmap_state(const SigSpec &sig) {
|
||||
if (ywmap_json.active())
|
||||
ywmap_states.emplace_back(sig);
|
||||
}
|
||||
|
||||
void ywmap_state(Cell *cell) {
|
||||
if (ywmap_json.active())
|
||||
ywmap_states.emplace_back(cell);
|
||||
}
|
||||
|
||||
void ywmap_input(const SigSpec &sig) {
|
||||
if (ywmap_json.active())
|
||||
ywmap_inputs.emplace_back(sig);
|
||||
}
|
||||
|
||||
void emit_ywmap_btor_sig(const ywmap_btor_sig &btor_sig) {
|
||||
if (btor_sig.cell == nullptr) {
|
||||
if (btor_sig.sig.empty()) {
|
||||
ywmap_json.value(nullptr);
|
||||
return;
|
||||
}
|
||||
ywmap_json.begin_array();
|
||||
ywmap_json.compact();
|
||||
for (auto &chunk : btor_sig.sig.chunks()) {
|
||||
log_assert(chunk.is_wire());
|
||||
|
||||
ywmap_json.begin_object();
|
||||
ywmap_json.entry("path", witness_path(chunk.wire));
|
||||
ywmap_json.entry("width", chunk.width);
|
||||
ywmap_json.entry("offset", chunk.offset);
|
||||
ywmap_json.end_object();
|
||||
}
|
||||
ywmap_json.end_array();
|
||||
} else {
|
||||
ywmap_json.begin_object();
|
||||
ywmap_json.compact();
|
||||
ywmap_json.entry("path", witness_path(btor_sig.cell));
|
||||
Mem *mem = mem_cells[btor_sig.cell];
|
||||
ywmap_json.entry("width", mem->width);
|
||||
ywmap_json.entry("size", mem->size);
|
||||
ywmap_json.end_object();
|
||||
}
|
||||
}
|
||||
|
||||
void btorf_push(const string &id)
|
||||
{
|
||||
if (verbose) {
|
||||
|
|
@ -617,7 +679,7 @@ struct BtorWorker
|
|||
SigSpec sig_d = sigmap(cell->getPort(ID::D));
|
||||
SigSpec sig_q = sigmap(cell->getPort(ID::Q));
|
||||
|
||||
if (!info_filename.empty() && cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)))
|
||||
if ((!info_filename.empty() || ywmap_json.active()) && cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)))
|
||||
{
|
||||
SigSpec sig_c = sigmap(cell->getPort(cell->type == ID($dff) ? ID::CLK : ID::C));
|
||||
int nid = get_sig_nid(sig_c);
|
||||
|
|
@ -629,7 +691,11 @@ struct BtorWorker
|
|||
if (cell->type == ID($dff) && !cell->getParam(ID::CLK_POLARITY).as_bool())
|
||||
negedge = true;
|
||||
|
||||
info_clocks[nid] |= negedge ? 2 : 1;
|
||||
if (!info_filename.empty())
|
||||
info_clocks[nid] |= negedge ? 2 : 1;
|
||||
|
||||
if (ywmap_json.active())
|
||||
ywmap_clock_bits[sig_c] |= negedge ? 2 : 1;
|
||||
}
|
||||
|
||||
IdString symbol;
|
||||
|
|
@ -662,6 +728,8 @@ struct BtorWorker
|
|||
else
|
||||
btorf("%d state %d %s\n", nid, sid, log_id(symbol));
|
||||
|
||||
ywmap_state(sig_q);
|
||||
|
||||
if (nid_init_val >= 0) {
|
||||
int nid_init = next_nid++;
|
||||
if (verbose)
|
||||
|
|
@ -683,6 +751,8 @@ struct BtorWorker
|
|||
|
||||
btorf("%d state %d%s\n", nid, sid, getinfo(cell).c_str());
|
||||
|
||||
ywmap_state(sig_y);
|
||||
|
||||
if (cell->type == ID($anyconst)) {
|
||||
int nid2 = next_nid++;
|
||||
btorf("%d next %d %d %d\n", nid2, sid, nid, nid);
|
||||
|
|
@ -705,6 +775,8 @@ struct BtorWorker
|
|||
btorf("%d state %d%s\n", initstate_nid, sid, getinfo(cell).c_str());
|
||||
btorf("%d init %d %d %d\n", next_nid++, sid, initstate_nid, one_nid);
|
||||
btorf("%d next %d %d %d\n", next_nid++, sid, initstate_nid, zero_nid);
|
||||
|
||||
ywmap_state(sig_y);
|
||||
}
|
||||
|
||||
add_nid_sig(initstate_nid, sig_y);
|
||||
|
|
@ -768,6 +840,8 @@ struct BtorWorker
|
|||
nid_init_val = next_nid++;
|
||||
btorf("%d state %d\n", nid_init_val, sid);
|
||||
|
||||
ywmap_state(nullptr);
|
||||
|
||||
for (int i = 0; i < mem->size; i++) {
|
||||
Const thisword = initdata.extract(i*mem->width, mem->width);
|
||||
if (thisword.is_fully_undef())
|
||||
|
|
@ -793,6 +867,8 @@ struct BtorWorker
|
|||
else
|
||||
btorf("%d state %d %s\n", nid, sid, log_id(mem->memid));
|
||||
|
||||
ywmap_state(cell);
|
||||
|
||||
if (nid_init_val >= 0)
|
||||
{
|
||||
int nid_init = next_nid++;
|
||||
|
|
@ -915,10 +991,13 @@ struct BtorWorker
|
|||
int sid = get_bv_sid(GetSize(sig));
|
||||
|
||||
int nid_input = next_nid++;
|
||||
if (is_init)
|
||||
if (is_init) {
|
||||
btorf("%d state %d\n", nid_input, sid);
|
||||
else
|
||||
ywmap_state(sig);
|
||||
} else {
|
||||
btorf("%d input %d\n", nid_input, sid);
|
||||
ywmap_input(sig);
|
||||
}
|
||||
|
||||
int nid_masked_input;
|
||||
if (sig_mask_undef.is_fully_ones()) {
|
||||
|
|
@ -993,6 +1072,7 @@ struct BtorWorker
|
|||
int sid = get_bv_sid(GetSize(s));
|
||||
int nid = next_nid++;
|
||||
btorf("%d input %d\n", nid, sid);
|
||||
ywmap_input(s);
|
||||
nid_width[nid] = GetSize(s);
|
||||
|
||||
for (int j = 0; j < GetSize(s); j++)
|
||||
|
|
@ -1075,12 +1155,15 @@ struct BtorWorker
|
|||
return nid;
|
||||
}
|
||||
|
||||
BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad, bool cover_mode, bool print_internal_names, string info_filename) :
|
||||
BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose, bool single_bad, bool cover_mode, bool print_internal_names, string info_filename, string ywmap_filename) :
|
||||
f(f), sigmap(module), module(module), verbose(verbose), single_bad(single_bad), cover_mode(cover_mode), print_internal_names(print_internal_names), info_filename(info_filename)
|
||||
{
|
||||
if (!info_filename.empty())
|
||||
infof("name %s\n", log_id(module));
|
||||
|
||||
if (!ywmap_filename.empty())
|
||||
ywmap_json.write_to_file(ywmap_filename);
|
||||
|
||||
memories = Mem::get_all_memories(module);
|
||||
|
||||
dict<IdString, Mem*> mem_dict;
|
||||
|
|
@ -1094,6 +1177,20 @@ struct BtorWorker
|
|||
|
||||
btorf_push("inputs");
|
||||
|
||||
if (ywmap_json.active()) {
|
||||
for (auto wire : module->wires())
|
||||
{
|
||||
auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
|
||||
if (gclk_attr == wire->attributes.end())
|
||||
continue;
|
||||
SigSpec sig = sigmap(wire);
|
||||
if (gclk_attr->second == State::S1)
|
||||
ywmap_clock_bits[sig] |= 1;
|
||||
else if (gclk_attr->second == State::S0)
|
||||
ywmap_clock_bits[sig] |= 2;
|
||||
}
|
||||
}
|
||||
|
||||
for (auto wire : module->wires())
|
||||
{
|
||||
if (wire->attributes.count(ID::init)) {
|
||||
|
|
@ -1111,6 +1208,7 @@ struct BtorWorker
|
|||
int nid = next_nid++;
|
||||
|
||||
btorf("%d input %d%s\n", nid, sid, getinfo(wire).c_str());
|
||||
ywmap_input(wire);
|
||||
add_nid_sig(nid, sig);
|
||||
|
||||
if (!info_filename.empty()) {
|
||||
|
|
@ -1122,6 +1220,16 @@ struct BtorWorker
|
|||
info_clocks[nid] |= 2;
|
||||
}
|
||||
}
|
||||
|
||||
if (ywmap_json.active()) {
|
||||
for (int i = 0; i < GetSize(sig); i++) {
|
||||
auto input_bit = SigBit(wire, i);
|
||||
auto bit = sigmap(input_bit);
|
||||
if (!ywmap_clock_bits.count(bit))
|
||||
continue;
|
||||
ywmap_clock_inputs[input_bit] = ywmap_clock_bits[bit];
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
btorf_pop("inputs");
|
||||
|
|
@ -1378,6 +1486,42 @@ struct BtorWorker
|
|||
f << it;
|
||||
f.close();
|
||||
}
|
||||
|
||||
if (ywmap_json.active())
|
||||
{
|
||||
ywmap_json.begin_object();
|
||||
ywmap_json.entry("version", "Yosys Witness BTOR map");
|
||||
ywmap_json.entry("generator", yosys_version_str);
|
||||
|
||||
ywmap_json.name("clocks");
|
||||
ywmap_json.begin_array();
|
||||
for (auto &entry : ywmap_clock_inputs) {
|
||||
if (entry.second != 1 && entry.second != 2)
|
||||
continue;
|
||||
log_assert(entry.first.is_wire());
|
||||
ywmap_json.begin_object();
|
||||
ywmap_json.compact();
|
||||
ywmap_json.entry("path", witness_path(entry.first.wire));
|
||||
ywmap_json.entry("offset", entry.first.offset);
|
||||
ywmap_json.entry("edge", entry.second == 1 ? "posedge" : "negedge");
|
||||
ywmap_json.end_object();
|
||||
}
|
||||
ywmap_json.end_array();
|
||||
|
||||
ywmap_json.name("inputs");
|
||||
ywmap_json.begin_array();
|
||||
for (auto &entry : ywmap_inputs)
|
||||
emit_ywmap_btor_sig(entry);
|
||||
ywmap_json.end_array();
|
||||
|
||||
ywmap_json.name("states");
|
||||
ywmap_json.begin_array();
|
||||
for (auto &entry : ywmap_states)
|
||||
emit_ywmap_btor_sig(entry);
|
||||
ywmap_json.end_array();
|
||||
|
||||
ywmap_json.end_object();
|
||||
}
|
||||
}
|
||||
};
|
||||
|
||||
|
|
@ -1406,11 +1550,15 @@ struct BtorBackend : public Backend {
|
|||
log(" -x\n");
|
||||
log(" Output symbols for internal netnames (starting with '$')\n");
|
||||
log("\n");
|
||||
log(" -ywmap <filename>\n");
|
||||
log(" Create a map file for conversion to and from Yosys witness traces\n");
|
||||
log("\n");
|
||||
}
|
||||
void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design) override
|
||||
{
|
||||
bool verbose = false, single_bad = false, cover_mode = false, print_internal_names = false;
|
||||
string info_filename;
|
||||
string ywmap_filename;
|
||||
|
||||
log_header(design, "Executing BTOR backend.\n");
|
||||
|
||||
|
|
@ -1443,6 +1591,10 @@ struct BtorBackend : public Backend {
|
|||
print_internal_names = true;
|
||||
continue;
|
||||
}
|
||||
if (args[argidx] == "-ywmap" && argidx+1 < args.size()) {
|
||||
ywmap_filename = args[++argidx];
|
||||
continue;
|
||||
}
|
||||
break;
|
||||
}
|
||||
extra_args(f, filename, args, argidx);
|
||||
|
|
@ -1455,7 +1607,7 @@ struct BtorBackend : public Backend {
|
|||
*f << stringf("; BTOR description generated by %s for module %s.\n",
|
||||
yosys_version_str, log_id(topmod));
|
||||
|
||||
BtorWorker(*f, topmod, verbose, single_bad, cover_mode, print_internal_names, info_filename);
|
||||
BtorWorker(*f, topmod, verbose, single_bad, cover_mode, print_internal_names, info_filename, ywmap_filename);
|
||||
|
||||
*f << stringf("; end of yosys output\n");
|
||||
}
|
||||
|
|
|
|||
|
|
@ -458,7 +458,7 @@ struct Smt2Worker
|
|||
{
|
||||
RTLIL::SigSpec sig_a, sig_b;
|
||||
RTLIL::SigSpec sig_y = sigmap(cell->getPort(ID::Y));
|
||||
bool is_signed = cell->getParam(ID::A_SIGNED).as_bool();
|
||||
bool is_signed = type == 'U' ? false : cell->getParam(ID::A_SIGNED).as_bool();
|
||||
int width = GetSize(sig_y);
|
||||
|
||||
if (type == 's' || type == 'S' || type == 'd' || type == 'b') {
|
||||
|
|
@ -483,6 +483,7 @@ struct Smt2Worker
|
|||
if (ch == 'A') processed_expr += get_bv(sig_a);
|
||||
else if (ch == 'B') processed_expr += get_bv(sig_b);
|
||||
else if (ch == 'P') processed_expr += get_bv(cell->getPort(ID::B));
|
||||
else if (ch == 'S') processed_expr += get_bv(cell->getPort(ID::S));
|
||||
else if (ch == 'L') processed_expr += is_signed ? "a" : "l";
|
||||
else if (ch == 'U') processed_expr += is_signed ? "s" : "u";
|
||||
else processed_expr += ch;
|
||||
|
|
@ -639,6 +640,9 @@ struct Smt2Worker
|
|||
if (cell->type == ID($xor)) return export_bvop(cell, "(bvxor A B)");
|
||||
if (cell->type == ID($xnor)) return export_bvop(cell, "(bvxnor A B)");
|
||||
|
||||
if (cell->type == ID($bweqx)) return export_bvop(cell, "(bvxnor A B)", 'U');
|
||||
if (cell->type == ID($bwmux)) return export_bvop(cell, "(bvor (bvand A (bvnot S)) (bvand B S))", 'U');
|
||||
|
||||
if (cell->type == ID($shl)) return export_bvop(cell, "(bvshl A B)", 's');
|
||||
if (cell->type == ID($shr)) return export_bvop(cell, "(bvlshr A B)", 's');
|
||||
if (cell->type == ID($sshl)) return export_bvop(cell, "(bvshl A B)", 's');
|
||||
|
|
@ -994,7 +998,7 @@ struct Smt2Worker
|
|||
if (contains_clock && GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
|
||||
comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
|
||||
clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
|
||||
if (contains_clock) {
|
||||
if (wire->port_input && contains_clock) {
|
||||
for (int i = 0; i < GetSize(sig); i++) {
|
||||
bool is_posedge = clock_posedge.count(sig[i]);
|
||||
bool is_negedge = clock_negedge.count(sig[i]);
|
||||
|
|
@ -1744,7 +1748,6 @@ struct Smt2Backend : public Backend {
|
|||
log_push();
|
||||
Pass::call(design, "bmuxmap");
|
||||
Pass::call(design, "demuxmap");
|
||||
Pass::call(design, "bwmuxmap");
|
||||
log_pop();
|
||||
|
||||
size_t argidx;
|
||||
|
|
|
|||
|
|
@ -110,6 +110,10 @@ class AigerMap:
|
|||
def __init__(self, mapfile):
|
||||
data = json.load(mapfile)
|
||||
|
||||
version = data.get("version") if isinstance(data, dict) else {}
|
||||
if version != "Yosys Witness Aiger map":
|
||||
raise click.ClickException(f"{mapfile.name}: unexpected file format version {version!r}")
|
||||
|
||||
self.latch_count = data["latch_count"]
|
||||
self.input_count = data["input_count"]
|
||||
|
||||
|
|
@ -250,5 +254,157 @@ def yw2aiw(input, mapfile, output):
|
|||
|
||||
click.echo(f"Converted {len(inyw)} time steps.")
|
||||
|
||||
class BtorMap:
|
||||
def __init__(self, mapfile):
|
||||
self.data = data = json.load(mapfile)
|
||||
|
||||
version = data.get("version") if isinstance(data, dict) else {}
|
||||
if version != "Yosys Witness BTOR map":
|
||||
raise click.ClickException(f"{mapfile.name}: unexpected file format version {version!r}")
|
||||
|
||||
self.sigmap = WitnessSigMap()
|
||||
|
||||
for mode in ("states", "inputs"):
|
||||
for btor_signal_def in data[mode]:
|
||||
if btor_signal_def is None:
|
||||
continue
|
||||
if isinstance(btor_signal_def, dict):
|
||||
btor_signal_def["path"] = tuple(btor_signal_def["path"])
|
||||
else:
|
||||
for chunk in btor_signal_def:
|
||||
chunk["path"] = tuple(chunk["path"])
|
||||
|
||||
|
||||
@cli.command(help="""
|
||||
Convert a BTOR witness trace into a Yosys witness trace.
|
||||
|
||||
This requires a Yosys witness BTOR map file as generated by 'write_btor -ywmap'.
|
||||
""")
|
||||
@click.argument("input", type=click.File("r"))
|
||||
@click.argument("mapfile", type=click.File("r"))
|
||||
@click.argument("output", type=click.File("w"))
|
||||
def wit2yw(input, mapfile, output):
|
||||
input_name = input.name
|
||||
click.echo(f"Converting BTOR witness trace {input_name!r} to Yosys witness trace {output.name!r}...")
|
||||
click.echo(f"Using Yosys witness BTOR map file {mapfile.name!r}")
|
||||
btor_map = BtorMap(mapfile)
|
||||
|
||||
input = filter(None, (line.split(';', 1)[0].strip() for line in input))
|
||||
|
||||
sat = next(input, None)
|
||||
if sat != "sat":
|
||||
raise click.ClickException(f"{input_name}: not a BTOR witness file")
|
||||
|
||||
props = next(input, None)
|
||||
|
||||
t = -1
|
||||
|
||||
line = next(input, None)
|
||||
|
||||
frames = []
|
||||
bits = {}
|
||||
|
||||
while line and not line.startswith('.'):
|
||||
current_t = int(line[1:].strip())
|
||||
if line[0] == '#':
|
||||
mode = "states"
|
||||
elif line[0] == '@':
|
||||
mode = "inputs"
|
||||
else:
|
||||
raise click.ClickException(f"{input_name}: unexpected data in BTOR witness file")
|
||||
|
||||
if current_t > t:
|
||||
t = current_t
|
||||
values = WitnessValues()
|
||||
array_inits = set()
|
||||
frames.append(values)
|
||||
|
||||
line = next(input, None)
|
||||
while line and line[0] not in "#@.":
|
||||
if current_t > 0 and mode == "states":
|
||||
line = next(input, None)
|
||||
continue
|
||||
tokens = line.split()
|
||||
line = next(input, None)
|
||||
|
||||
btor_sig = btor_map.data[mode][int(tokens[0])]
|
||||
btor_sigs = [btor_sig]
|
||||
|
||||
if btor_sig is None:
|
||||
continue
|
||||
|
||||
if isinstance(btor_sig, dict):
|
||||
addr = tokens[1]
|
||||
if not addr.startswith('['):
|
||||
addr = '[*]'
|
||||
value = tokens[1]
|
||||
else:
|
||||
value = tokens[2]
|
||||
if not addr.endswith(']'):
|
||||
raise click.ClickException(f"{input_name}: expected address in BTOR witness file")
|
||||
path = btor_sig["path"]
|
||||
width = btor_sig["width"]
|
||||
size = btor_sig["size"]
|
||||
if addr == '[*]':
|
||||
btor_sigs = [
|
||||
[{
|
||||
"path": (*path, f"\\[{addr}]"),
|
||||
"width": width,
|
||||
"offset": 0,
|
||||
}]
|
||||
for addr in range(size)
|
||||
if (path, addr) not in array_inits
|
||||
]
|
||||
array_inits.update((path, addr) for addr in range(size))
|
||||
else:
|
||||
addr = int(addr[1:-1], 2)
|
||||
|
||||
if addr < 0 or addr >= size:
|
||||
raise click.ClickException(f"{input_name}: out of bounds address in BTOR witness file")
|
||||
|
||||
array_inits.add((path, addr))
|
||||
btor_sig = [{
|
||||
"path": (*path, f"\\[{addr}]"),
|
||||
"width": width,
|
||||
"offset": 0,
|
||||
}]
|
||||
btor_sigs = [btor_sig]
|
||||
else:
|
||||
value = tokens[1]
|
||||
|
||||
for btor_sig in btor_sigs:
|
||||
value_bits = iter(reversed(value))
|
||||
|
||||
for chunk in btor_sig:
|
||||
offset = chunk["offset"]
|
||||
path = chunk["path"]
|
||||
for i in range(offset, offset + chunk["width"]):
|
||||
key = (path, i)
|
||||
bits[key] = mode == "inputs"
|
||||
values[key] = next(value_bits)
|
||||
|
||||
if next(value_bits, None) is not None:
|
||||
raise click.ClickException(f"{input_name}: excess bits in BTOR witness file")
|
||||
|
||||
|
||||
if line is None:
|
||||
raise click.ClickException(f"{input_name}: unexpected end of BTOR witness file")
|
||||
if line.strip() != '.':
|
||||
raise click.ClickException(f"{input_name}: unexpected data in BTOR witness file")
|
||||
if next(input, None) is not None:
|
||||
raise click.ClickException(f"{input_name}: unexpected trailing data in BTOR witness file")
|
||||
|
||||
outyw = WriteWitness(output, 'yosys-witness wit2yw')
|
||||
|
||||
outyw.signals = coalesce_signals((), bits)
|
||||
for clock in btor_map.data["clocks"]:
|
||||
outyw.add_clock(clock["path"], clock["offset"], clock["edge"])
|
||||
|
||||
for values in frames:
|
||||
outyw.step(values)
|
||||
|
||||
outyw.end_trace()
|
||||
click.echo(f"Converted {outyw.t} time steps.")
|
||||
|
||||
if __name__ == "__main__":
|
||||
cli()
|
||||
|
|
|
|||
|
|
@ -175,8 +175,9 @@ class WitnessSig:
|
|||
return self.sort_key < other.sort_key
|
||||
|
||||
|
||||
def coalesce_signals(signals):
|
||||
bits = {}
|
||||
def coalesce_signals(signals, bits=None):
|
||||
if bits is None:
|
||||
bits = {}
|
||||
for sig in signals:
|
||||
for bit in sig.bits():
|
||||
if sig.init_only:
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue