diff options
Diffstat (limited to 'backends/aiger')
| -rw-r--r-- | backends/aiger/aiger.cc | 25 | ||||
| -rw-r--r-- | backends/aiger/xaiger.cc | 31 |
2 files changed, 33 insertions, 23 deletions
diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc index 35935b847..547d131ee 100644 --- a/backends/aiger/aiger.cc +++ b/backends/aiger/aiger.cc @@ -606,7 +606,7 @@ struct AigerWriter f << stringf("c\nGenerated by %s\n", yosys_version_str); } - void write_map(std::ostream &f, bool verbose_map) + void write_map(std::ostream &f, bool verbose_map, bool no_startoffset) { dict<int, string> input_lines; dict<int, string> init_lines; @@ -627,32 +627,33 @@ struct AigerWriter continue; int a = aig_map.at(sig[i]); + int index = no_startoffset ? i : (wire->start_offset+i); if (verbose_map) - wire_lines[a] += stringf("wire %d %d %s\n", a, wire->start_offset+i, log_id(wire)); + wire_lines[a] += stringf("wire %d %d %s\n", a, index, log_id(wire)); if (wire->port_input) { log_assert((a & 1) == 0); - input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, wire->start_offset+i, log_id(wire)); + input_lines[a] += stringf("input %d %d %s\n", (a >> 1)-1, index, log_id(wire)); } if (wire->port_output) { int o = ordered_outputs.at(sig[i]); - output_lines[o] += stringf("output %d %d %s\n", o, wire->start_offset+i, log_id(wire)); + output_lines[o] += stringf("output %d %d %s\n", o, index, 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, wire->start_offset+i, log_id(wire)); + init_lines[a] += stringf("init %d %d %s\n", (a >> 1)-1, index, log_id(wire)); } if (ordered_latches.count(sig[i])) { 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, wire->start_offset+i, log_id(wire)); + latch_lines[l] += stringf("invlatch %d %d %s\n", l, index, log_id(wire)); else - latch_lines[l] += stringf("latch %d %d %s\n", l, wire->start_offset+i, log_id(wire)); + latch_lines[l] += stringf("latch %d %d %s\n", l, index, log_id(wire)); } } } @@ -713,6 +714,9 @@ struct AigerBackend : public Backend { log(" -vmap <filename>\n"); log(" like -map, but more verbose\n"); log("\n"); + log(" -no-startoffset\n"); + log(" make indexes zero based, enable using map files with smt solvers.\n"); + log("\n"); log(" -I, -O, -B, -L\n"); log(" If the design contains no input/output/assert/flip-flop then create one\n"); log(" dummy input/output/bad_state-pin or latch to make the tools reading the\n"); @@ -730,6 +734,7 @@ struct AigerBackend : public Backend { bool omode = false; bool bmode = false; bool lmode = false; + bool no_startoffset = false; std::string map_filename; log_header(design, "Executing AIGER backend.\n"); @@ -762,6 +767,10 @@ struct AigerBackend : public Backend { verbose_map = true; continue; } + if (args[argidx] == "-no-startoffset") { + no_startoffset = true; + continue; + } if (args[argidx] == "-I") { imode = true; continue; @@ -804,7 +813,7 @@ struct AigerBackend : public Backend { 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, verbose_map); + writer.write_map(mapf, verbose_map, no_startoffset); } } } AigerBackend; diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 66955d88e..e223f185e 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -261,26 +261,27 @@ struct XAigerWriter if (!timing.count(inst_module->name)) timing.setup_module(inst_module); - auto &t = timing.at(inst_module->name).arrival; - for (const auto &conn : cell->connections()) { - auto port_wire = inst_module->wire(conn.first); - if (!port_wire->port_output) + + for (auto &i : timing.at(inst_module->name).arrival) { + if (!cell->hasPort(i.first.name)) continue; - for (int i = 0; i < GetSize(conn.second); i++) { - auto d = t.at(TimingInfo::NameBit(conn.first,i), 0); - if (d == 0) - continue; + auto port_wire = inst_module->wire(i.first.name); + log_assert(port_wire->port_output); + + auto d = i.second.first; + if (d == 0) + continue; + auto offset = i.first.offset; #ifndef NDEBUG - if (ys_debug(1)) { - static std::set<std::tuple<IdString,IdString,int>> seen; - if (seen.emplace(inst_module->name, conn.first, i).second) log("%s.%s[%d] abc9_arrival = %d\n", - log_id(cell->type), log_id(conn.first), i, d); - } -#endif - arrival_times[conn.second[i]] = d; + if (ys_debug(1)) { + static pool<std::pair<IdString,TimingInfo::NameBit>> seen; + if (seen.emplace(inst_module->name, i.first).second) log("%s.%s[%d] abc9_arrival = %d\n", + log_id(cell->type), log_id(i.first.name), offset, d); } +#endif + arrival_times[cell->getPort(i.first.name)[offset]] = d; } if (abc9_flop) |