Merge remote-tracking branch 'origin/master' into xaig_dff

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,6 +771,10 @@ struct AigerBackend : public Backend {
 				bmode = true;
 				continue;
 			}
+			if (args[argidx] == "-L") {
+				lmode = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(f, filename, args, argidx);
@@ -773,7 +784,7 @@ struct AigerBackend : public Backend {
 		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()) {

backends/aiger/xaiger.cc

@@ -345,12 +345,12 @@ struct XAigerWriter
 				}
 			}
 			else {
-				bool cell_known = inst_module;
+				bool cell_known = inst_module || cell->known();
 				for (const auto &c : cell->connections()) {
 					if (c.second.is_fully_const()) continue;
 					auto port_wire = inst_module ? inst_module->wire(c.first) : nullptr;
-					auto is_input = !cell_known || port_wire->port_input;
-					auto is_output = !cell_known || port_wire->port_output;
+					auto is_input = (port_wire && port_wire->port_input) || !cell_known || cell->input(c.first);
+					auto is_output = (port_wire && port_wire->port_output) || !cell_known || cell->output(c.first);
 					if (!is_input && !is_output)
 						log_error("Connection '%s' on cell '%s' (type '%s') not recognised!\n", log_id(c.first), log_id(cell), log_id(cell->type));
 
@@ -653,6 +653,11 @@ 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));
@@ -749,6 +754,7 @@ struct XAigerWriter
 
 		f << "c";
 
+		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));
@@ -1024,6 +1030,8 @@ 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());

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++) {

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