Merge branch 'master' into SergeyDegtyar/efinix

5 files changed, 111 insertions, 60 deletions

diff --git a/backends/aiger/aiger.cc b/backends/aiger/aiger.cc
index 7c851bb91..3e8b14dee 100644
--- a/backends/aiger/aiger.cc
+++ b/backends/aiger/aiger.cc
@@ -101,7 +101,7 @@ struct AigerWriter
 		return a;
 	}
 
-	AigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode) : module(module), zinit_mode(zinit_mode), sigmap(module)
+	AigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode, bool lmode) : module(module), zinit_mode(zinit_mode), sigmap(module)
 	{
 		pool<SigBit> undriven_bits;
 		pool<SigBit> unused_bits;
@@ -367,6 +367,12 @@ struct AigerWriter
 				aig_latchin.push_back(a);
 		}
 
+		if (lmode && aig_l == 0) {
+			aig_m++, aig_l++;
+			aig_latchinit.push_back(0);
+			aig_latchin.push_back(0);
+		}
+
 		if (!initstate_bits.empty() || !init_inputs.empty())
 			aig_latchin.push_back(1);
 
@@ -704,9 +710,9 @@ struct AigerBackend : public Backend {
 		log("    -vmap <filename>\n");
 		log("        like -map, but more verbose\n");
 		log("\n");
-		log("    -I, -O, -B\n");
-		log("        If the design contains no input/output/assert then create one\n");
-		log("        dummy input/output/bad_state pin to make the tools reading the\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");
 		log("        AIGER file happy.\n");
 		log("\n");
 	}
@@ -720,6 +726,7 @@ struct AigerBackend : public Backend {
 		bool imode = false;
 		bool omode = false;
 		bool bmode = false;
+		bool lmode = false;
 		std::string map_filename;
 
 		log_header(design, "Executing AIGER backend.\n");
@@ -764,16 +771,20 @@ struct AigerBackend : public Backend {
 				bmode = true;
 				continue;
 			}
+			if (args[argidx] == "-L") {
+				lmode = true;
+				continue;
+			}
 			break;
 		}
-		extra_args(f, filename, args, argidx);
+		extra_args(f, filename, args, argidx, !ascii_mode);
 
 		Module *top_module = design->top_module();
 
 		if (top_module == nullptr)
 			log_error("Can't find top module in current design!\n");
 
-		AigerWriter writer(top_module, zinit_mode, imode, omode, bmode);
+		AigerWriter writer(top_module, zinit_mode, imode, omode, bmode, lmode);
 		writer.write_aiger(*f, ascii_mode, miter_mode, symbols_mode);
 
 		if (!map_filename.empty()) {
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc
index e1b84236d..4018cc9de 100644
--- a/backends/aiger/xaiger.cc
+++ b/backends/aiger/xaiger.cc
@@ -83,6 +83,7 @@ struct XAigerWriter
 	dict<SigBit, pair<SigBit, SigBit>> and_map;
 	vector<std::tuple<SigBit,RTLIL::Cell*,RTLIL::IdString,int>> ci_bits;
 	vector<std::tuple<SigBit,RTLIL::Cell*,RTLIL::IdString,int,int>> co_bits;
+	dict<SigBit, float> arrival_times;
 
 	vector<pair<int, int>> aig_gates;
 	vector<int> aig_outputs;
@@ -247,14 +248,15 @@ struct XAigerWriter
 				if (!holes_mode) {
 					toposort.node(cell->name);
 					for (const auto &conn : cell->connections()) {
-						if (cell->input(conn.first)) {
+						auto port_wire = inst_module->wire(conn.first);
+						if (port_wire->port_input) {
 							// Ignore inout for the sake of topographical ordering
-							if (cell->output(conn.first)) continue;
+							if (port_wire->port_output) continue;
 							for (auto bit : sigmap(conn.second))
 								bit_users[bit].insert(cell->name);
 						}
 
-						if (cell->output(conn.first))
+						if (port_wire->port_output)
 							for (auto bit : sigmap(conn.second))
 								bit_drivers[bit].insert(cell->name);
 					}
@@ -271,7 +273,7 @@ struct XAigerWriter
 						log_error("Connection '%s' on cell '%s' (type '%s') not recognised!\n", log_id(c.first), log_id(cell), log_id(cell->type));
 
 					if (is_input) {
-						for (auto b : c.second.bits()) {
+						for (auto b : c.second) {
 							Wire *w = b.wire;
 							if (!w) continue;
 							if (!w->port_output || !cell_known) {
@@ -287,7 +289,17 @@ struct XAigerWriter
 						}
 					}
 					if (is_output) {
-						for (auto b : c.second.bits()) {
+						int arrival = 0;
+						if (port_wire) {
+							auto it = port_wire->attributes.find("\\abc_arrival");
+							if (it != port_wire->attributes.end()) {
+								if (it->second.flags != 0)
+									log_error("Attribute 'abc_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(port_wire), log_id(cell->type));
+								arrival = it->second.as_int();
+							}
+						}
+
+						for (auto b : c.second) {
 							Wire *w = b.wire;
 							if (!w) continue;
 							input_bits.insert(b);
@@ -295,6 +307,9 @@ struct XAigerWriter
 							if (O != b)
 								alias_map[O] = b;
 							undriven_bits.erase(O);
+
+							if (arrival)
+								arrival_times[b] = arrival;
 						}
 					}
 				}
@@ -335,6 +350,8 @@ struct XAigerWriter
 				if (!box_module || !box_module->attributes.count("\\abc_box_id"))
 					continue;
 
+				bool blackbox = box_module->get_blackbox_attribute(true /* ignore_wb */);
+
 				// Fully pad all unused input connections of this box cell with S0
 				// Fully pad all undriven output connections of this box cell with anonymous wires
 				// NB: Assume box_module->ports are sorted alphabetically
@@ -379,7 +396,10 @@ struct XAigerWriter
 							rhs = it->second;
 						}
 						else {
-							rhs = module->addWire(NEW_ID, GetSize(w));
+							Wire *wire = module->addWire(NEW_ID, GetSize(w));
+							if (blackbox)
+								wire->set_bool_attribute(ID(abc_padding));
+							rhs = wire;
 							cell->setPort(port_name, rhs);
 						}
 
@@ -390,12 +410,7 @@ struct XAigerWriter
 							if (O != b)
 								alias_map[O] = b;
 							undriven_bits.erase(O);
-
-							auto jt = input_bits.find(b);
-							if (jt != input_bits.end()) {
-								log_assert(keep_bits.count(O));
-								input_bits.erase(b);
-							}
+							input_bits.erase(b);
 						}
 					}
 				}
@@ -414,7 +429,7 @@ struct XAigerWriter
 			// inherit existing inout's drivers
 			if ((wire->port_input && wire->port_output && !undriven_bits.count(bit))
 					|| keep_bits.count(bit)) {
-				RTLIL::IdString wire_name = wire->name.str() + "$inout.out";
+				RTLIL::IdString wire_name = stringf("$%s$inout.out", wire->name.c_str());
 				RTLIL::Wire *new_wire = module->wire(wire_name);
 				if (!new_wire)
 					new_wire = module->addWire(wire_name, GetSize(wire));
@@ -489,16 +504,16 @@ struct XAigerWriter
 			aig_outputs.push_back(bit2aig(bit));
 		}
 
+		if (output_bits.empty()) {
+			output_bits.insert(State::S0);
+			omode = true;
+		}
+
 		for (auto bit : output_bits) {
 			ordered_outputs[bit] = aig_o++;
 			aig_outputs.push_back(bit2aig(bit));
 		}
 
-		if (output_bits.empty()) {
-			aig_o++;
-			aig_outputs.push_back(0);
-			omode = true;
-		}
 	}
 
 	void write_aiger(std::ostream &f, bool ascii_mode)
@@ -560,26 +575,38 @@ struct XAigerWriter
 
 		f << "c";
 
-		if (!box_list.empty()) {
-			auto write_buffer = [](std::stringstream &buffer, int i32) {
-				int32_t i32_be = to_big_endian(i32);
-				buffer.write(reinterpret_cast<const char*>(&i32_be), sizeof(i32_be));
-			};
-
-			std::stringstream h_buffer;
-			auto write_h_buffer = std::bind(write_buffer, std::ref(h_buffer), std::placeholders::_1);
-			write_h_buffer(1);
-			log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ci_bits));
-			write_h_buffer(input_bits.size() + ci_bits.size());
-			log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(co_bits));
-			write_h_buffer(output_bits.size() + co_bits.size());
-			log_debug("piNum = %d\n", GetSize(input_bits));
-			write_h_buffer(input_bits.size());
-			log_debug("poNum = %d\n", GetSize(output_bits));
-			write_h_buffer(output_bits.size());
-			log_debug("boxNum = %d\n", GetSize(box_list));
-			write_h_buffer(box_list.size());
+		log_assert(!output_bits.empty());
+		auto write_buffer = [](std::stringstream &buffer, int i32) {
+			int32_t i32_be = to_big_endian(i32);
+			buffer.write(reinterpret_cast<const char*>(&i32_be), sizeof(i32_be));
+		};
+		std::stringstream h_buffer;
+		auto write_h_buffer = std::bind(write_buffer, std::ref(h_buffer), std::placeholders::_1);
+		write_h_buffer(1);
+		log_debug("ciNum = %d\n", GetSize(input_bits) + GetSize(ci_bits));
+		write_h_buffer(input_bits.size() + ci_bits.size());
+		log_debug("coNum = %d\n", GetSize(output_bits) + GetSize(co_bits));
+		write_h_buffer(output_bits.size() + GetSize(co_bits));
+		log_debug("piNum = %d\n", GetSize(input_bits));
+		write_h_buffer(input_bits.size());
+		log_debug("poNum = %d\n", GetSize(output_bits));
+		write_h_buffer(output_bits.size());
+		log_debug("boxNum = %d\n", GetSize(box_list));
+		write_h_buffer(box_list.size());
+
+		auto write_buffer_float = [](std::stringstream &buffer, float f32) {
+			buffer.write(reinterpret_cast<const char*>(&f32), sizeof(f32));
+		};
+		std::stringstream i_buffer;
+		auto write_i_buffer = std::bind(write_buffer_float, std::ref(i_buffer), std::placeholders::_1);
+		for (auto bit : input_bits)
+			write_i_buffer(arrival_times.at(bit, 0));
+		//std::stringstream o_buffer;
+		//auto write_o_buffer = std::bind(write_buffer_float, std::ref(o_buffer), std::placeholders::_1);
+		//for (auto bit : output_bits)
+		//	write_o_buffer(0);
 
+		if (!box_list.empty()) {
 			RTLIL::Module *holes_module = module->design->addModule("$__holes__");
 			log_assert(holes_module);
 
@@ -643,19 +670,12 @@ struct XAigerWriter
 				write_h_buffer(box_count++);
 			}
 
-			f << "h";
-			std::string buffer_str = h_buffer.str();
-			int32_t buffer_size_be = to_big_endian(buffer_str.size());
-			f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
-			f.write(buffer_str.data(), buffer_str.size());
-
 			std::stringstream r_buffer;
 			auto write_r_buffer = std::bind(write_buffer, std::ref(r_buffer), std::placeholders::_1);
 			write_r_buffer(0);
-
 			f << "r";
-			buffer_str = r_buffer.str();
-			buffer_size_be = to_big_endian(buffer_str.size());
+			std::string buffer_str = r_buffer.str();
+			int32_t buffer_size_be = to_big_endian(buffer_str.size());
 			f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
 			f.write(buffer_str.data(), buffer_str.size());
 
@@ -709,6 +729,23 @@ struct XAigerWriter
 			}
 		}
 
+		f << "h";
+		std::string buffer_str = h_buffer.str();
+		int32_t buffer_size_be = to_big_endian(buffer_str.size());
+		f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+		f.write(buffer_str.data(), buffer_str.size());
+
+		f << "i";
+		buffer_str = i_buffer.str();
+		buffer_size_be = to_big_endian(buffer_str.size());
+		f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+		f.write(buffer_str.data(), buffer_str.size());
+		//f << "o";
+		//buffer_str = o_buffer.str();
+		//buffer_size_be = to_big_endian(buffer_str.size());
+		//f.write(reinterpret_cast<const char*>(&buffer_size_be), sizeof(buffer_size_be));
+		//f.write(buffer_str.data(), buffer_str.size());
+
 		f << stringf("Generated by %s\n", yosys_version_str);
 	}
 
@@ -760,11 +797,11 @@ struct XAigerWriter
 			f << stringf("box %d %d %s\n", box_count++, 0, log_id(cell->name));
 
 		output_lines.sort();
+		if (omode)
+			output_lines[State::S0] = "output 0 0 $__dummy__\n";
 		for (auto &it : output_lines)
 			f << it.second;
 		log_assert(output_lines.size() == output_bits.size());
-		if (omode && output_bits.empty())
-			f << "output " << output_lines.size() << " 0 $__dummy__\n";
 
 		wire_lines.sort();
 		for (auto &it : wire_lines)
@@ -819,7 +856,7 @@ struct XAigerBackend : public Backend {
 			}
 			break;
 		}
-		extra_args(f, filename, args, argidx);
+		extra_args(f, filename, args, argidx, !ascii_mode);
 
 		Module *top_module = design->top_module();
 
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 7c054d655..f617b7ec2 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -685,7 +685,7 @@ struct BtorWorker
 				}
 				else
 				{
-					int nid_init_val = next_nid++;
+					nid_init_val = next_nid++;
 					btorf("%d state %d\n", nid_init_val, sid);
 
 					for (int i = 0; i < nwords; i++) {
@@ -897,9 +897,12 @@ struct BtorWorker
 
 							int sid = get_bv_sid(GetSize(s));
 							int nid = next_nid++;
-							btorf("%d input %d %s\n", nid, sid);
+							btorf("%d input %d\n", nid, sid);
 							nid_width[nid] = GetSize(s);
 
+							for (int j = 0; j < GetSize(s); j++)
+								nidbits.push_back(make_pair(nid, j));
+
 							i += GetSize(s)-1;
 							continue;
 						}
diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc
index fff110bb0..671686173 100644
--- a/backends/protobuf/protobuf.cc
+++ b/backends/protobuf/protobuf.cc
@@ -266,7 +266,7 @@ struct ProtobufBackend : public Backend {
 			}
 			break;
 		}
-		extra_args(f, filename, args, argidx);
+		extra_args(f, filename, args, argidx, !text_mode);
 
 		log_header(design, "Executing Protobuf backend.\n");
 
@@ -338,7 +338,7 @@ struct ProtobufPass : public Pass {
 		if (!filename.empty()) {
 			rewrite_filename(filename);
 			std::ofstream *ff = new std::ofstream;
-			ff->open(filename.c_str(), std::ofstream::trunc);
+			ff->open(filename.c_str(), text_mode ? std::ofstream::trunc : (std::ofstream::trunc | std::ofstream::binary));
 			if (ff->fail()) {
 				delete ff;
 				log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
diff --git a/backends/smt2/Makefile.inc b/backends/smt2/Makefile.inc
index 92941d4cf..68394a909 100644
--- a/backends/smt2/Makefile.inc
+++ b/backends/smt2/Makefile.inc
@@ -16,7 +16,7 @@ yosys-smtbmc-script.py: backends/smt2/smtbmc.py
 		-e "s|#!/usr/bin/env python3|#!$(PYTHON)|" < $< > $@
 
 yosys-smtbmc.exe: misc/launcher.c yosys-smtbmc-script.py
-	$(P) gcc -DGUI=0 -O -s -o $@ $<
+	$(P) $(CXX) -DGUI=0 -O -s -o $@ $<
 # Other targets
 else
 TARGETS += yosys-smtbmc