Added "write_aiger -zinit -symbols -vmap"

1 files 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<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)
@@ -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<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);
@@ -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 <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)
@@ -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;