Add -no-startoffset option to write_aiger

Author: mmicko

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;