Add -no-startoffset option to write_aiger

diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 35935b847e02e3489d69fb4d479dad16d79c4e35..547d131ee34e70556ad7bd74de4870749637d8f6 100644 (file)
--- 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;