From 5fa1fa1e6f0dd731267f5e93d05f0223949d5c5c Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 1 Dec 2016 11:04:36 +0100 Subject: [PATCH] Added "write_aiger -zinit -symbols -vmap" --- backends/aiger/aiger.cc | 169 +++++++++++++++++++++++++++++++++------- 1 file changed, 139 insertions(+), 30 deletions(-) diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 93aa0ebc0..9dd3a94c7 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -58,6 +58,13 @@ struct AigerWriter dict init_inputs; int initstate_ff = 0; + int mkgate(int a0, int a1) + { + aig_m++, aig_a++; + aig_gates.push_back(a0 > a1 ? make_pair(a0, a1) : make_pair(a1, a0)); + return 2*aig_m; + } + int bit2aig(SigBit bit) { if (aig_map.count(bit) == 0) @@ -76,9 +83,7 @@ struct AigerWriter auto args = and_map.at(bit); int a0 = bit2aig(args.first); int a1 = bit2aig(args.second); - aig_m++, aig_a++; - aig_map[bit] = 2*aig_m; - aig_gates.push_back(a0 > a1 ? make_pair(a0, a1) : make_pair(a1, a0)); + aig_map[bit] = mkgate(a0, a1); } } @@ -94,7 +99,8 @@ struct AigerWriter SigSpec initsig = sigmap(wire); Const initval = wire->attributes.at("\\init"); for (int i = 0; i < GetSize(wire) && i < GetSize(initval); i++) - init_map[initsig[i]] = initval[i]; + if (initval[i] == State::S0 || initval[i] == State::S1) + init_map[initsig[i]] = initval[i] == State::S1; } if (wire->port_input) @@ -171,7 +177,7 @@ struct AigerWriter for (auto it : ff_map) { aig_m++, aig_l++; aig_map[it.first] = 2*aig_m; - ordered_latches[it.first] = aig_l; + ordered_latches[it.first] = aig_l-1; if (init_map.count(it.first) == 0) aig_latchinit.push_back(2); else @@ -184,20 +190,44 @@ struct AigerWriter aig_latchinit.push_back(0); } - for (auto it : ff_map) - aig_latchin.push_back(bit2aig(it.second)); + if (zinit_mode) + { + for (auto it : ff_map) + { + int l = ordered_latches[it.first]; + + if (aig_latchinit.at(l) == 1) + aig_map[it.first] ^= 1; + + if (aig_latchinit.at(l) == 2) + { + int gated_ffout = mkgate(aig_map[it.first], initstate_ff^1); + int gated_initin = mkgate(init_inputs[it.first], initstate_ff); + aig_map[it.first] = mkgate(gated_ffout^1, gated_initin^1)^1; + } + } + } + + for (auto it : ff_map) { + int a = bit2aig(it.second); + int l = ordered_latches[it.first]; + if (zinit_mode && aig_latchinit.at(l) == 1) + aig_latchin.push_back(a ^ 1); + else + aig_latchin.push_back(a); + } if (!initstate_bits.empty() || !init_inputs.empty()) aig_latchin.push_back(1); for (auto bit : output_bits) { aig_o++; - ordered_outputs[bit] = aig_o; + ordered_outputs[bit] = aig_o-1; aig_outputs.push_back(bit2aig(bit)); } } - void write_aiger(std::ostream &f, bool ascii_mode, bool miter_mode) + void write_aiger(std::ostream &f, bool ascii_mode, bool miter_mode, bool symbols_mode) { log_assert(aig_m == aig_i + aig_l + aig_a); log_assert(aig_l == GetSize(aig_latchin)); @@ -215,7 +245,7 @@ struct AigerWriter f << stringf("%d\n", 2*i+2); for (int i = 0; i < aig_l; i++) { - if (aig_latchinit.at(i) == 0) + if (zinit_mode || aig_latchinit.at(i) == 0) f << stringf("%d %d\n", 2*(aig_i+i)+2, aig_latchin.at(i)); else if (aig_latchinit.at(i) == 1) f << stringf("%d %d 1\n", 2*(aig_i+i)+2, aig_latchin.at(i)); @@ -232,7 +262,7 @@ struct AigerWriter else { for (int i = 0; i < aig_l; i++) { - if (aig_latchinit.at(i) == 0) + if (zinit_mode || aig_latchinit.at(i) == 0) f << stringf("%d\n", aig_latchin.at(i)); else if (aig_latchinit.at(i) == 1) f << stringf("%d 1\n", aig_latchin.at(i)); @@ -254,19 +284,69 @@ struct AigerWriter } } + if (symbols_mode) + { + for (auto wire : module->wires()) + { + if (wire->name[0] == '$') + continue; + + SigSpec sig = sigmap(wire); + + for (int i = 0; i < GetSize(wire); i++) + { + if (wire->port_input) { + int a = aig_map.at(sig[i]); + log_assert((a & 1) == 0); + if (GetSize(wire) != 1) + f << stringf("i%d %s[%d]\n", (a >> 1)-1, log_id(wire), i); + else + f << stringf("i%d %s\n", (a >> 1)-1, log_id(wire)); + } + + if (wire->port_output) { + int o = ordered_outputs.at(sig[i]); + if (GetSize(wire) != 1) + f << stringf("%c%d %s[%d]\n", miter_mode ? 'b' : 'o', o, log_id(wire), i); + else + f << stringf("%c%d %s\n", miter_mode ? 'b' : 'o', o, log_id(wire)); + } + + if (init_inputs.count(sig[i])) { + int a = init_inputs.at(sig[i]); + log_assert((a & 1) == 0); + if (GetSize(wire) != 1) + f << stringf("i%d init:%s[%d]\n", (a >> 1)-1, log_id(wire), i); + else + f << stringf("i%d init:%s\n", (a >> 1)-1, log_id(wire)); + } + + if (ordered_latches.count(sig[i])) { + int l = ordered_latches.at(sig[i]); + const char *p = (zinit_mode && (aig_latchinit.at(l) == 1)) ? "!" : ""; + if (GetSize(wire) != 1) + f << stringf("l%d %s%s[%d]\n", l, p, log_id(wire), i); + else + f << stringf("l%d %s%s\n", l, p, log_id(wire)); + } + } + } + } + f << stringf("c\nGenerated by %s\n", yosys_version_str); } - void write_map(std::ostream &f) + void write_map(std::ostream &f, bool verbose_map) { dict input_lines; + dict init_lines; dict output_lines; dict latch_lines; dict wire_lines; for (auto wire : module->wires()) { - if (wire->name[0] == '$') + if (!verbose_map && wire->name[0] == '$') continue; SigSpec sig = sigmap(wire); @@ -277,21 +357,32 @@ struct AigerWriter continue; int a = aig_map.at(sig[i]); - // wire_lines[a] = stringf("wire %d %d %s\n", a, i, log_id(wire)); + + if (verbose_map) + wire_lines[a] += stringf("wire %d %d %s\n", a, i, log_id(wire)); if (wire->port_input) { log_assert((a & 1) == 0); - input_lines[a] = stringf("input %d %d %s\n", (a >> 1)-1, i, log_id(wire)); + input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, i, log_id(wire)); } if (wire->port_output) { - int n = ordered_outputs.at(sig[i]); - output_lines[n] = stringf("output %d %d %s\n", n-1, i, log_id(wire)); + int o = ordered_outputs.at(sig[i]); + output_lines[o] += stringf("output %d %d %s\n", o, i, log_id(wire)); + } + + if (init_inputs.count(sig[i])) { + int a = init_inputs.at(sig[i]); + log_assert((a & 1) == 0); + init_lines[a] += stringf("init %d %d %s\n", (a >> 1)-1, i, log_id(wire)); } if (ordered_latches.count(sig[i])) { - int n = ordered_latches.at(sig[i]); - latch_lines[n] = stringf("latch %d %d %s\n", n-1, i, log_id(wire)); + int l = ordered_latches.at(sig[i]); + if (zinit_mode && (aig_latchinit.at(l) == 1)) + latch_lines[l] += stringf("invlatch %d %d %s\n", l, i, log_id(wire)); + else + latch_lines[l] += stringf("latch %d %d %s\n", l, i, log_id(wire)); } } } @@ -300,6 +391,10 @@ struct AigerWriter for (auto &it : input_lines) f << it.second; + init_lines.sort(); + for (auto &it : init_lines) + f << it.second; + output_lines.sort(); for (auto &it : output_lines) f << it.second; @@ -328,15 +423,21 @@ struct AigerBackend : public Backend { log(" -ascii\n"); log(" write ASCII version of AGIER format\n"); log("\n"); - // log(" -zinit\n"); - // log(" convert FFs to zero-initialized FFs, adding additional inputs for\n"); - // log(" uninitialized FFs.\n"); - // log("\n"); + log(" -zinit\n"); + log(" convert FFs to zero-initialized FFs, adding additional inputs for\n"); + log(" uninitialized FFs.\n"); + log("\n"); log(" -miter\n"); log(" design outputs are AIGER bad state properties\n"); log("\n"); + log(" -symbols\n"); + log(" include a symbol table in the generated AIGER file\n"); + log("\n"); log(" -map \n"); - log(" write an extra file with port, latch and wire mappings\n"); + log(" write an extra file with port and latch symbols\n"); + log("\n"); + log(" -vmap \n"); + log(" like -map, but more verbose\n"); log("\n"); } virtual void execute(std::ostream *&f, std::string filename, std::vector args, RTLIL::Design *design) @@ -344,6 +445,8 @@ struct AigerBackend : public Backend { bool ascii_mode = false; bool zinit_mode = false; bool miter_mode = false; + bool symbols_mode = false; + bool verbose_map = false; std::string map_filename; log_header(design, "Executing AIGER backend.\n"); @@ -363,10 +466,19 @@ struct AigerBackend : public Backend { miter_mode = true; continue; } - if (args[argidx] == "-map" && argidx+1 < args.size()) { + if (args[argidx] == "-symbols") { + symbols_mode = true; + continue; + } + if (map_filename.empty() && args[argidx] == "-map" && argidx+1 < args.size()) { map_filename = args[++argidx]; continue; } + if (map_filename.empty() && args[argidx] == "-vmap" && argidx+1 < args.size()) { + map_filename = args[++argidx]; + verbose_map = true; + continue; + } break; } extra_args(f, filename, args, argidx); @@ -376,18 +488,15 @@ struct AigerBackend : public Backend { if (top_module == nullptr) log_error("Can't find top module in current design!\n"); - if (zinit_mode) - log_error("zinit mode is not implemented yet.\n"); - AigerWriter writer(top_module, zinit_mode); - writer.write_aiger(*f, ascii_mode, miter_mode); + writer.write_aiger(*f, ascii_mode, miter_mode, symbols_mode); if (!map_filename.empty()) { std::ofstream mapf; mapf.open(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_map(mapf); + writer.write_map(mapf, verbose_map); } } } AigerBackend; -- 2.30.2