aiger: Use new JSON code for writing aiger witness map files

This commit is contained in:
Jannis Harder 2022-12-23 17:22:24 +01:00
parent 29461ade17
commit 3e25e61778
3 changed files with 96 additions and 55 deletions

View File

@ -19,6 +19,7 @@
#include "kernel/yosys.h" #include "kernel/yosys.h"
#include "kernel/sigtools.h" #include "kernel/sigtools.h"
#include "kernel/json.h"
#include "libs/json11/json11.hpp" #include "libs/json11/json11.hpp"
USING_YOSYS_NAMESPACE USING_YOSYS_NAMESPACE
@ -721,18 +722,19 @@ struct AigerWriter
return path; return path;
} }
void write_ywmap(std::ostream &f) void write_ywmap(PrettyJson &json)
{ {
f << "{\n"; json.begin_object();
f << " \"version\": \"Yosys Witness Aiger Map\",\n"; json.entry("version", "Yosys Witness Aiger map");
f << stringf(" \"generator\": %s,\n", json11::Json(yosys_version_str).dump().c_str()); json.entry("gennerator", yosys_version_str);
f << stringf(" \"latch_count\": %d,\n", aig_l);
f << stringf(" \"input_count\": %d,\n", aig_i);
dict<int, string> clock_lines; json.entry("latch_count", aig_l);
dict<int, string> input_lines; json.entry("input_count", aig_i);
dict<int, string> init_lines;
dict<int, string> seq_lines; 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()) for (auto cell : module->cells())
{ {
@ -751,21 +753,21 @@ struct AigerWriter
if (init_inputs.count(sig[i])) { if (init_inputs.count(sig[i])) {
int a = init_inputs.at(sig[i]); int a = init_inputs.at(sig[i]);
log_assert((a & 1) == 0); 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) }, { "path", witness_path(wire) },
{ "input", (a >> 1) - 1 }, { "input", (a >> 1) - 1 },
{ "offset", sig_qy[i].offset }, { "offset", sig_qy[i].offset },
}).dump(); });
} }
if (input_bits.count(sig[i])) { if (input_bits.count(sig[i])) {
int a = aig_map.at(sig[i]); int a = aig_map.at(sig[i]);
log_assert((a & 1) == 0); 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) }, { "path", witness_path(wire) },
{ "input", (a >> 1) - 1 }, { "input", (a >> 1) - 1 },
{ "offset", sig_qy[i].offset }, { "offset", sig_qy[i].offset },
}).dump(); });
} }
} }
} }
@ -783,60 +785,55 @@ struct AigerWriter
int a = aig_map.at(sig[i]); int a = aig_map.at(sig[i]);
log_assert((a & 1) == 0); log_assert((a & 1) == 0);
input_lines[a] += json11::Json(json11::Json::object { input_lines[a] = json11::Json(json11::Json::object {
{ "path", path }, { "path", path },
{ "input", (a >> 1) - 1 }, { "input", (a >> 1) - 1 },
{ "offset", i }, { "offset", i },
}).dump(); });
if (ywmap_clocks.count(sig[i])) { if (ywmap_clocks.count(sig[i])) {
int clock_mode = ywmap_clocks[sig[i]]; int clock_mode = ywmap_clocks[sig[i]];
if (clock_mode != 3) { if (clock_mode != 3) {
clock_lines[a] += json11::Json(json11::Json::object { clock_lines[a] = json11::Json(json11::Json::object {
{ "path", path }, { "path", path },
{ "input", (a >> 1) - 1 }, { "input", (a >> 1) - 1 },
{ "offset", i }, { "offset", i },
{ "edge", clock_mode == 1 ? "posedge" : "negedge" }, { "edge", clock_mode == 1 ? "posedge" : "negedge" },
}).dump(); });
} }
} }
} }
} }
} }
f << " \"clocks\": ["; json.name("clocks");
json.begin_array();
clock_lines.sort(); clock_lines.sort();
const char *sep = "\n "; for (auto &it : clock_lines)
for (auto &it : clock_lines) { json.value(it.second);
f << sep << it.second; json.end_array();
sep = ",\n ";
}
f << "\n ],\n";
f << " \"inputs\": ["; json.name("inputs");
json.begin_array();
input_lines.sort(); input_lines.sort();
sep = "\n "; for (auto &it : input_lines)
for (auto &it : input_lines) { json.value(it.second);
f << sep << it.second; json.end_array();
sep = ",\n ";
}
f << "\n ],\n";
f << " \"seqs\": ["; json.name("seqs");
sep = "\n "; json.begin_array();
for (auto &it : seq_lines) { input_lines.sort();
f << sep << it.second; for (auto &it : seq_lines)
sep = ",\n "; json.value(it.second);
} json.end_array();
f << "\n ],\n";
f << " \"inits\": ["; json.name("inits");
sep = "\n "; json.begin_array();
for (auto &it : init_lines) { input_lines.sort();
f << sep << it.second; for (auto &it : init_lines)
sep = ",\n "; json.value(it.second);
} json.end_array();
f << "\n ]\n}\n"; json.end_object();
} }
}; };
@ -991,9 +988,12 @@ struct AigerBackend : public Backend {
if (!yw_map_filename.empty()) { if (!yw_map_filename.empty()) {
std::ofstream mapf; std::ofstream mapf;
mapf.open(yw_map_filename.c_str(), std::ofstream::trunc); 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)); PrettyJson json;
writer.write_ywmap(mapf);
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; } AigerBackend;

View File

@ -23,13 +23,38 @@ USING_YOSYS_NAMESPACE
void PrettyJson::emit_to_log() void PrettyJson::emit_to_log()
{ {
targets.push_back([](const char *raw_json) { log("%s", raw_json); }); struct LogTarget : public Target {
void emit(const char *data) override { log("%s", data); }
};
targets.push_back(std::unique_ptr<Target>(new LogTarget));
} }
void PrettyJson::append_to_string(std::string &target) void PrettyJson::append_to_string(std::string &target)
{ {
std::string *target_p = &target; struct AppendStringTarget : public Target {
targets.push_back([=](const char *raw_json) { *target_p += raw_json; }); std::string &target;
AppendStringTarget(std::string &target) : target(target) {}
void emit(const char *data) override { target += data; }
};
targets.push_back(std::unique_ptr<Target>(new AppendStringTarget(target)));
}
bool PrettyJson::write_to_file(const std::string &path)
{
struct WriteFileTarget : public Target {
std::ofstream target;
void emit(const char *data) override { target << data; }
void flush() override { target.flush(); }
};
auto target = std::unique_ptr<WriteFileTarget>(new WriteFileTarget);
target->target.open(path);
if (target->target.fail())
return false;
targets.push_back(std::unique_ptr<Target>(target.release()));
return true;
} }
void PrettyJson::line() void PrettyJson::line()
@ -42,7 +67,13 @@ void PrettyJson::line()
void PrettyJson::raw(const char *raw_json) void PrettyJson::raw(const char *raw_json)
{ {
for (auto &target : targets) for (auto &target : targets)
target(raw_json); target->emit(raw_json);
}
void PrettyJson::flush()
{
for (auto &target : targets)
target->flush();
} }
void PrettyJson::begin_object() void PrettyJson::begin_object()
@ -110,8 +141,10 @@ void PrettyJson::begin_value()
void PrettyJson::end_value() void PrettyJson::end_value()
{ {
if (state.empty()) if (state.empty()) {
raw("\n"); raw("\n");
flush();
}
} }
void PrettyJson::value_json(const Json &value) void PrettyJson::value_json(const Json &value)

View File

@ -38,18 +38,26 @@ class PrettyJson
ARRAY, ARRAY,
}; };
struct Target {
virtual void emit(const char *data) = 0;
virtual void flush() {};
virtual ~Target() {};
};
std::string newline_indent = "\n"; std::string newline_indent = "\n";
std::vector<std::function<void(const char *)>> targets; std::vector<std::unique_ptr<Target>> targets;
std::vector<Scope> state = {VALUE}; std::vector<Scope> state = {VALUE};
public: public:
void emit_to_log(); void emit_to_log();
void append_to_string(std::string &target); void append_to_string(std::string &target);
bool write_to_file(const std::string &path);
bool active() { return !targets.empty(); } bool active() { return !targets.empty(); }
void line(); void line();
void raw(const char *raw_json); void raw(const char *raw_json);
void flush();
void begin_object(); void begin_object();
void begin_array(); void begin_array();
void end_object(); void end_object();