dict<SigBit, int> 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)
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);
}
}
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)
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
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));
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));
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));
}
}
+ 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<int, string> input_lines;
+ dict<int, string> init_lines;
dict<int, string> output_lines;
dict<int, string> latch_lines;
dict<int, string> wire_lines;
for (auto wire : module->wires())
{
- if (wire->name[0] == '$')
+ if (!verbose_map && wire->name[0] == '$')
continue;
SigSpec sig = sigmap(wire);
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));
}
}
}
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;
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 <filename>\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 <filename>\n");
+ log(" like -map, but more verbose\n");
log("\n");
}
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
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");
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);
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;
projects / yosys.git / commitdiff