Merge branch 'master' of https://github.com/cliffordwolf/yosys into btor

4 files changed, 172 insertions, 11 deletions

diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index 2921c92d8..051d8dc68 100644
--- a/passes/opt/opt_clean.cc
+++ b/passes/opt/opt_clean.cc
@@ -47,7 +47,7 @@ static void rmunused_module_cells(RTLIL::Module *module, bool verbose)
 				wire2driver.insert(sig, cell);
 			}
 		}
-		if (cell->type == "$memwr" || cell->get_bool_attribute("\\keep"))
+		if (cell->type == "$memwr" || cell->type == "$assert" || cell->get_bool_attribute("\\keep"))
 			queue.insert(cell);
 		unused.insert(cell);
 	}
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc
index fef99dfc0..cf3cd59f5 100644
--- a/passes/sat/sat.cc
+++ b/passes/sat/sat.cc
@@ -47,6 +47,7 @@ struct SatHelper
 	std::vector<std::pair<std::string, std::string>> sets, prove, prove_x, sets_init;
 	std::map<int, std::vector<std::pair<std::string, std::string>>> sets_at;
 	std::map<int, std::vector<std::string>> unsets_at;
+	bool prove_asserts;
 
 	// undef constraints
 	bool enable_undef, set_init_undef;
@@ -284,7 +285,7 @@ struct SatHelper
 
 	int setup_proof(int timestep = -1)
 	{
-		assert(prove.size() + prove_x.size() > 0);
+		assert(prove.size() || prove_x.size() || prove_asserts);
 
 		RTLIL::SigSpec big_lhs, big_rhs;
 		std::vector<int> prove_bits;
@@ -352,6 +353,9 @@ struct SatHelper
 				prove_bits.push_back(ez.OR(undef_lhs.at(i), ez.AND(ez.NOT(undef_rhs.at(i)), ez.NOT(ez.XOR(value_lhs.at(i), value_rhs.at(i))))));
 		}
 
+		if (prove_asserts)
+			prove_bits.push_back(satgen.importAsserts(timestep));
+
 		return ez.expression(ezSAT::OpAnd, prove_bits);
 	}
 
@@ -717,15 +721,21 @@ struct SatPass : public Pass {
 		log("The following additional options can be used to set up a proof. If also -seq\n");
 		log("is passed, a temporal induction proof is performed.\n");
 		log("\n");
+		log("    -tempinduct\n");
+		log("        Perform a temporal induction proof. In a temporalinduction proof it is\n");
+		log("        proven that the condition holds forever after the number of time steps\n");
+		log("        specified using -seq.\n");
+		log("\n");
 		log("    -prove <signal> <value>\n");
-		log("        Attempt to proof that <signal> is always <value>. In a temporal\n");
-		log("        induction proof it is proven that the condition holds forever after\n");
-		log("        the number of time steps passed using -seq.\n");
+		log("        Attempt to proof that <signal> is always <value>.\n");
 		log("\n");
 		log("    -prove-x <signal> <value>\n");
 		log("        Like -prove, but an undef (x) bit in the lhs matches any value on\n");
 		log("        the right hand side. Useful for equivialence checking.\n");
 		log("\n");
+		log("    -prove-asserts\n");
+		log("        Prove that all asserts in the design hold.\n");
+		log("\n");
 		log("    -maxsteps <N>\n");
 		log("        Set a maximum length for the induction.\n");
 		log("\n");
@@ -748,6 +758,7 @@ struct SatPass : public Pass {
 		int loopcount = 0, seq_len = 0, maxsteps = 0, timeout = 0;
 		bool verify = false, fail_on_timeout = false, enable_undef = false, set_def_inputs = false;
 		bool ignore_div_by_zero = false, set_init_undef = false, max_undef = false;
+		bool tempinduct = false, prove_asserts = false;
 
 		log_header("Executing SAT pass (solving SAT problems in the circuit).\n");
 
@@ -817,6 +828,10 @@ struct SatPass : public Pass {
 				enable_undef = true;
 				continue;
 			}
+			if (args[argidx] == "-tempinduct") {
+				tempinduct = true;
+				continue;
+			}
 			if (args[argidx] == "-prove" && argidx+2 < args.size()) {
 				std::string lhs = args[++argidx];
 				std::string rhs = args[++argidx];
@@ -830,6 +845,10 @@ struct SatPass : public Pass {
 				enable_undef = true;
 				continue;
 			}
+			if (args[argidx] == "-prove-asserts") {
+				prove_asserts = true;
+				continue;
+			}
 			if (args[argidx] == "-seq" && argidx+1 < args.size()) {
 				seq_len = atoi(args[++argidx].c_str());
 				continue;
@@ -894,16 +913,22 @@ struct SatPass : public Pass {
 		if (module == NULL) 
 			log_cmd_error("Can't perform SAT on an empty selection!\n");
 
-		if (prove.size() + prove_x.size() == 0 && verify)
+		if (!prove.size() && !prove_x.size() && !prove_asserts && verify)
 			log_cmd_error("Got -verify but nothing to prove!\n");
 
+		if (!prove.size() && !prove_x.size() && !prove_asserts && tempinduct)
+			log_cmd_error("Got -tempinduct but nothing to prove!\n");
+
+		if (seq_len == 0 && tempinduct)
+			log_cmd_error("Got -tempinduct but no -seq argument!\n");
+
 		if (set_def_inputs) {
 			for (auto &it : module->wires)
 				if (it.second->port_input)
 					sets_def.push_back(it.second->name);
 		}
 
-		if (prove.size() + prove_x.size() > 0 && seq_len > 0)
+		if (tempinduct)
 		{
 			if (loopcount > 0 || max_undef)
 				log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
@@ -914,6 +939,7 @@ struct SatPass : public Pass {
 			basecase.sets = sets;
 			basecase.prove = prove;
 			basecase.prove_x = prove_x;
+			basecase.prove_asserts = prove_asserts;
 			basecase.sets_at = sets_at;
 			basecase.unsets_at = unsets_at;
 			basecase.shows = shows;
@@ -935,6 +961,7 @@ struct SatPass : public Pass {
 			inductstep.sets = sets;
 			inductstep.prove = prove;
 			inductstep.prove_x = prove_x;
+			inductstep.prove_asserts = prove_asserts;
 			inductstep.shows = shows;
 			inductstep.timeout = timeout;
 			inductstep.sets_def = sets_def;
@@ -1021,6 +1048,7 @@ struct SatPass : public Pass {
 			sathelper.sets = sets;
 			sathelper.prove = prove;
 			sathelper.prove_x = prove_x;
+			sathelper.prove_asserts = prove_asserts;
 			sathelper.sets_at = sets_at;
 			sathelper.unsets_at = unsets_at;
 			sathelper.shows = shows;
@@ -1037,11 +1065,14 @@ struct SatPass : public Pass {
 
 			if (seq_len == 0) {
 				sathelper.setup();
-				if (sathelper.prove.size() + sathelper.prove_x.size() > 0)
+				if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
 					sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
 			} else {
-				for (int timestep = 1; timestep <= seq_len; timestep++)
+				for (int timestep = 1; timestep <= seq_len; timestep++) {
 					sathelper.setup(timestep);
+					if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
+						sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof(timestep)));
+				}
 				sathelper.setup_init();
 			}
 			sathelper.generate_model();
@@ -1064,7 +1095,7 @@ struct SatPass : public Pass {
 					sathelper.maximize_undefs();
 				}
 
-				if (prove.size() + prove_x.size() == 0) {
+				if (!prove.size() && !prove_x.size() && !prove_asserts) {
 					log("SAT solving finished - model found:\n");
 				} else {
 					log("SAT proof finished - model found: FAIL!\n");
@@ -1090,7 +1121,7 @@ struct SatPass : public Pass {
 					goto timeout;
 				if (rerun_counter)
 					log("SAT solving finished - no more models found (after %d distinct solutions).\n", rerun_counter);
-				else if (prove.size() + prove_x.size() == 0)
+				else if (!prove.size() && !prove_x.size() && !prove_asserts)
 					log("SAT solving finished - no model found.\n");
 				else {
 					log("SAT proof finished - no model found: SUCCESS!\n");
diff --git a/passes/techmap/Makefile.inc b/passes/techmap/Makefile.inc
index 0a56932b7..9751a4744 100644
--- a/passes/techmap/Makefile.inc
+++ b/passes/techmap/Makefile.inc
@@ -3,6 +3,7 @@ OBJS += passes/techmap/techmap.o
 OBJS += passes/techmap/simplemap.o
 OBJS += passes/techmap/dfflibmap.o
 OBJS += passes/techmap/iopadmap.o
+OBJS += passes/techmap/hilomap.o
 OBJS += passes/techmap/libparse.o
 
 GENFILES += passes/techmap/stdcells.inc
diff --git a/passes/techmap/hilomap.cc b/passes/techmap/hilomap.cc
new file mode 100644
index 000000000..bc5caa38c
--- /dev/null
+++ b/passes/techmap/hilomap.cc
@@ -0,0 +1,129 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
+ *  
+ *  Permission to use, copy, modify, and/or distribute this software for any
+ *  purpose with or without fee is hereby granted, provided that the above
+ *  copyright notice and this permission notice appear in all copies.
+ *  
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/register.h"
+#include "kernel/rtlil.h"
+#include "kernel/log.h"
+
+static std::string hicell_celltype, hicell_portname;
+static std::string locell_celltype, locell_portname;
+static bool singleton_mode;
+
+static RTLIL::Module *module;
+static RTLIL::SigChunk last_hi, last_lo;
+
+void hilomap_worker(RTLIL::SigSpec &sig)
+{
+	sig.expand();
+	for (auto &c : sig.chunks) {
+		if (c.wire == NULL && (c.data.bits.at(0) == RTLIL::State::S1) && !hicell_celltype.empty()) {
+			if (!singleton_mode || last_hi.width == 0) {
+				last_hi = RTLIL::SigChunk(NEW_WIRE(module, 1));
+				RTLIL::Cell *cell = new RTLIL::Cell;
+				cell->name = NEW_ID;
+				cell->type = RTLIL::escape_id(hicell_celltype);
+				cell->connections[RTLIL::escape_id(hicell_portname)] = last_hi;
+				module->add(cell);
+			}
+			c = last_hi;
+		}
+		if (c.wire == NULL && (c.data.bits.at(0) == RTLIL::State::S0) && !locell_celltype.empty()) {
+			if (!singleton_mode || last_lo.width == 0) {
+				last_lo = RTLIL::SigChunk(NEW_WIRE(module, 1));
+				RTLIL::Cell *cell = new RTLIL::Cell;
+				cell->name = NEW_ID;
+				cell->type = RTLIL::escape_id(locell_celltype);
+				cell->connections[RTLIL::escape_id(locell_portname)] = last_lo;
+				module->add(cell);
+			}
+			c = last_lo;
+		}
+	}
+	sig.optimize();
+}
+
+struct HilomapPass : public Pass {
+	HilomapPass() : Pass("hilomap", "technology mapping of constant hi- and/or lo-drivers") { }
+	virtual void help()
+	{
+		log("\n");
+		log("    hilomap [options] [selection]\n");
+		log("\n");
+		log("Map module inputs/outputs to PAD cells from a library. This pass\n");
+		log("can only map to very simple PAD cells. Use 'techmap' to further map\n");
+		log("the resulting cells to more sophisticated PAD cells.\n");
+		log("\n");
+		log("    -hicell <celltype> <portname>\n");
+		log("        Replace constant hi bits with this cell.\n");
+		log("\n");
+		log("    -locell <celltype> <portname>\n");
+		log("        Replace constant lo bits with this cell.\n");
+		log("\n");
+		log("    -singleton\n");
+		log("        Create only one hi/lo cell and connect all constant bits\n");
+		log("        to that cell. Per default a separate cell is created for\n");
+		log("        each constant bit.\n");
+		log("\n");
+	}
+	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+	{
+		log_header("Executing HILOPAD pass (mapping to constant drivers).\n");
+
+		hicell_celltype = std::string();
+		hicell_portname = std::string();
+		locell_celltype = std::string();
+		locell_portname = std::string();
+		singleton_mode = false;
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			if (args[argidx] == "-hicell" && argidx+2 < args.size()) {
+				hicell_celltype = args[++argidx];
+				hicell_portname = args[++argidx];
+				continue;
+			}
+			if (args[argidx] == "-locell" && argidx+2 < args.size()) {
+				locell_celltype = args[++argidx];
+				locell_portname = args[++argidx];
+				continue;
+			}
+			if (args[argidx] == "-singleton") {
+				singleton_mode = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(args, argidx, design);
+
+		for (auto &it : design->modules)
+		{
+			module = it.second;
+
+			if (!design->selected(module))
+				continue;
+
+			last_hi = RTLIL::SigChunk();
+			last_lo = RTLIL::SigChunk();
+
+			module->rewrite_sigspecs(hilomap_worker);
+		}
+	}
+} HilomapPass;
+