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

16 files changed, 349 insertions, 33 deletions

diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc
index 20158488..ecc58cf6 100644
--- a/frontends/ast/ast.cc
+++ b/frontends/ast/ast.cc
@@ -80,6 +80,7 @@ std::string AST::type2str(AstNodeType type)
 	X(AST_CELLTYPE)
 	X(AST_IDENTIFIER)
 	X(AST_PREFIX)
+	X(AST_ASSERT)
 	X(AST_FCALL)
 	X(AST_TO_SIGNED)
 	X(AST_TO_UNSIGNED)
diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h
index 22853d0f..6aaa90e8 100644
--- a/frontends/ast/ast.h
+++ b/frontends/ast/ast.h
@@ -58,6 +58,7 @@ namespace AST
 		AST_CELLTYPE,
 		AST_IDENTIFIER,
 		AST_PREFIX,
+		AST_ASSERT,
 
 		AST_FCALL,
 		AST_TO_SIGNED,
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index e44b2d36..83a5c750 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -1276,6 +1276,38 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 		}
 		break;
 
+	// generate $assert cells
+	case AST_ASSERT:
+		{
+			log_assert(children.size() == 2);
+
+			RTLIL::SigSpec check = children[0]->genRTLIL();
+			log_assert(check.width == 1);
+
+			RTLIL::SigSpec en = children[1]->genRTLIL();
+			log_assert(en.width == 1);
+
+			std::stringstream sstr;
+			sstr << "$assert$" << filename << ":" << linenum << "$" << (RTLIL::autoidx++);
+
+			RTLIL::Cell *cell = new RTLIL::Cell;
+			cell->attributes["\\src"] = stringf("%s:%d", filename.c_str(), linenum);
+			cell->name = sstr.str();
+			cell->type = "$assert";
+			current_module->cells[cell->name] = cell;
+
+			for (auto &attr : attributes) {
+				if (attr.second->type != AST_CONSTANT)
+					log_error("Attribute `%s' with non-constant value at %s:%d!\n",
+							attr.first.c_str(), filename.c_str(), linenum);
+				cell->attributes[attr.first] = attr.second->asAttrConst();
+			}
+
+			cell->connections["\\A"] = check;
+			cell->connections["\\EN"] = en;
+		}
+		break;
+
 	// add entries to current_module->connections for assignments (outside of always blocks)
 	case AST_ASSIGN:
 		{
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index bc5dec7b..c266800e 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -966,6 +966,66 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 	}
 skip_dynamic_range_lvalue_expansion:;
 
+	if (stage > 1 && type == AST_ASSERT && current_block != NULL)
+	{
+		std::stringstream sstr;
+		sstr << "$assert$" << filename << ":" << linenum << "$" << (RTLIL::autoidx++);
+		std::string id_check = sstr.str() + "_CHECK", id_en = sstr.str() + "_EN";
+
+		AstNode *wire_check = new AstNode(AST_WIRE);
+		wire_check->str = id_check;
+		current_ast_mod->children.push_back(wire_check);
+		current_scope[wire_check->str] = wire_check;
+		while (wire_check->simplify(true, false, false, 1, -1, false)) { }
+
+		AstNode *wire_en = new AstNode(AST_WIRE);
+		wire_en->str = id_en;
+		current_ast_mod->children.push_back(wire_en);
+		current_scope[wire_en->str] = wire_en;
+		while (wire_en->simplify(true, false, false, 1, -1, false)) { }
+
+		std::vector<RTLIL::State> x_bit;
+		x_bit.push_back(RTLIL::State::Sx);
+
+		AstNode *assign_check = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), mkconst_bits(x_bit, false));
+		assign_check->children[0]->str = id_check;
+
+		AstNode *assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), mkconst_int(0, false, 1));
+		assign_en->children[0]->str = id_en;
+
+		AstNode *default_signals = new AstNode(AST_BLOCK);
+		default_signals->children.push_back(assign_check);
+		default_signals->children.push_back(assign_en);
+		current_top_block->children.insert(current_top_block->children.begin(), default_signals);
+
+		assign_check = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), new AstNode(AST_REDUCE_BOOL, children[0]->clone()));
+		assign_check->children[0]->str = id_check;
+
+		assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), mkconst_int(1, false, 1));
+		assign_en->children[0]->str = id_en;
+
+		newNode = new AstNode(AST_BLOCK);
+		newNode->children.push_back(assign_check);
+		newNode->children.push_back(assign_en);
+
+		AstNode *assertnode = new AstNode(AST_ASSERT);
+		assertnode->children.push_back(new AstNode(AST_IDENTIFIER));
+		assertnode->children.push_back(new AstNode(AST_IDENTIFIER));
+		assertnode->children[0]->str = id_check;
+		assertnode->children[1]->str = id_en;
+		assertnode->attributes.swap(attributes);
+		current_ast_mod->children.push_back(assertnode);
+
+		goto apply_newNode;
+	}
+
+	if (stage > 1 && type == AST_ASSERT && children.size() == 1)
+	{
+		children[0] = new AstNode(AST_REDUCE_BOOL, children[0]->clone());
+		children.push_back(mkconst_int(1, false, 1));
+		did_something = true;
+	}
+
 	// found right-hand side identifier for memory -> replace with memory read port
 	if (stage > 1 && type == AST_IDENTIFIER && id2ast != NULL && id2ast->type == AST_MEMORY && !in_lvalue &&
 			children[0]->type == AST_RANGE && children[0]->children.size() == 1) {
diff --git a/frontends/verilog/lexer.l b/frontends/verilog/lexer.l
index 9e606d90..81167cf4 100644
--- a/frontends/verilog/lexer.l
+++ b/frontends/verilog/lexer.l
@@ -113,6 +113,8 @@ namespace VERILOG_FRONTEND {
 "generate"     { return TOK_GENERATE; }
 "endgenerate"  { return TOK_ENDGENERATE; }
 
+"assert"([ \t\r\n]+"property")? { return TOK_ASSERT; }
+
 "input"   { return TOK_INPUT; }
 "output"  { return TOK_OUTPUT; }
 "inout"   { return TOK_INOUT; }
diff --git a/frontends/verilog/parser.y b/frontends/verilog/parser.y
index 874482d6..b0c4db8a 100644
--- a/frontends/verilog/parser.y
+++ b/frontends/verilog/parser.y
@@ -104,7 +104,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 %token TOK_GENERATE TOK_ENDGENERATE TOK_GENVAR
 %token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE
 %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED
-%token TOK_POS_INDEXED TOK_NEG_INDEXED
+%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT
 
 %type <ast> wire_type range non_opt_range expr basic_expr concat_list rvalue lvalue lvalue_concat_list
 %type <string> opt_label tok_prim_wrapper hierarchical_id
@@ -366,7 +366,7 @@ module_body:
 
 module_body_stmt:
 	task_func_decl | param_decl | localparam_decl | defparam_decl | wire_decl | assign_stmt | cell_stmt |
-	always_stmt | TOK_GENERATE module_gen_body TOK_ENDGENERATE | defattr;
+	always_stmt | TOK_GENERATE module_gen_body TOK_ENDGENERATE | defattr | assert;
 
 task_func_decl:
 	TOK_TASK TOK_ID ';' {
@@ -748,6 +748,11 @@ opt_label:
 		$$ = NULL;
 	};
 
+assert:
+	TOK_ASSERT '(' expr ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_ASSERT, $3));
+	};
+
 simple_behavioral_stmt:
 	lvalue '=' expr {
 		AstNode *node = new AstNode(AST_ASSIGN_EQ, $1, $3);
@@ -760,7 +765,7 @@ simple_behavioral_stmt:
 
 // this production creates the obligatory if-else shift/reduce conflict
 behavioral_stmt:
-	defattr | wire_decl |
+	defattr | assert | wire_decl |
 	simple_behavioral_stmt ';' |
 	hierarchical_id attr {
 		AstNode *node = new AstNode(AST_TCALL);
diff --git a/frontends/verilog/preproc.cc b/frontends/verilog/preproc.cc
index 5cfa0f24..db53e8c6 100644
--- a/frontends/verilog/preproc.cc
+++ b/frontends/verilog/preproc.cc
@@ -386,7 +386,7 @@ std::string frontend_verilog_preproc(FILE *f, std::string filename, const std::m
 			std::string name = tok.substr(1);
 			// printf("expand: >>%s<< -> >>%s<<\n", name.c_str(), defines_map[name].c_str());
 			std::string skipped_spaces = skip_spaces();
-			tok = next_token(true);
+			tok = next_token(false);
 			if (tok == "(" && defines_with_args.count(name) > 0) {
 				int level = 1;
 				std::vector<std::string> args;
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index 2f311c82..9e63e9d1 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -96,6 +96,7 @@ struct CellTypes
 		cell_types.insert("$pmux");
 		cell_types.insert("$safe_pmux");
 		cell_types.insert("$lut");
+		cell_types.insert("$assert");
 	}
 
 	void setup_internals_mem()
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 66152573..7638d468 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -595,6 +595,13 @@ namespace {
 				return;
 			}
 
+			if (cell->type == "$assert") {
+				port("\\A", 1);
+				port("\\EN", 1);
+				check_expected();
+				return;
+			}
+
 			if (cell->type == "$_INV_") { check_gate("AY"); return; }
 			if (cell->type == "$_AND_") { check_gate("ABY"); return; }
 			if (cell->type == "$_OR_")  { check_gate("ABY"); return; }
diff --git a/kernel/satgen.h b/kernel/satgen.h
index a668c73a..0909e58e 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -38,6 +38,7 @@ struct SatGen
 	SigMap *sigmap;
 	std::string prefix;
 	SigPool initial_state;
+	RTLIL::SigSpec asserts_a, asserts_en;
 	bool ignore_div_by_zero;
 	bool model_undef;
 
@@ -96,6 +97,19 @@ struct SatGen
 		return importSigSpecWorker(sig, pf, true, false);
 	}
 
+	int importAsserts(int timestep = -1)
+	{
+		std::vector<int> check_bits, enable_bits;
+		if (model_undef) {
+			check_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_a, timestep)), importDefSigSpec(asserts_a, timestep));
+			enable_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_en, timestep)), importDefSigSpec(asserts_en, timestep));
+		} else {
+			check_bits = importDefSigSpec(asserts_a, timestep);
+			enable_bits = importDefSigSpec(asserts_en, timestep);
+		}
+		return ez->vec_reduce_and(ez->vec_or(check_bits, ez->vec_not(enable_bits)));
+	}
+
 	int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep_lhs = -1, int timestep_rhs = -1)
 	{
 		if (timestep_rhs < 0)
@@ -765,6 +779,13 @@ struct SatGen
 			return true;
 		}
 
+		if (cell->type == "$assert")
+		{
+			asserts_a.append((*sigmap)(cell->connections.at("\\A")));
+			asserts_en.append((*sigmap)(cell->connections.at("\\EN")));
+			return true;
+		}
+
 		// Unsupported internal cell types: $pow $lut
 		// .. and all sequential cells except $dff and $_DFF_[NP]_
 		return false;
diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex
index b84e1b30..b848a2b6 100644
--- a/manual/CHAPTER_CellLib.tex
+++ b/manual/CHAPTER_CellLib.tex
@@ -418,3 +418,7 @@ from the gate level logic network can be mapped to physical flip-flop cells from
 pass. The combinatorial logic cells can be mapped to physical cells from a Liberty file via ABC \citeweblink{ABC}
 using the {\tt abc} pass.
 
+\begin{fixme}
+Add information about {\tt \$assert} cells.
+\end{fixme}
+
diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index 2921c92d..051d8dc6 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 fef99dfc..cf3cd59f 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 0a56932b..9751a474 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 00000000..bc5caa38
--- /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;
+ 
diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index f3d652f0..8f354a63 100644
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -65,10 +65,10 @@ parameter Y_WIDTH = 0;
 output [Y_WIDTH-1:0] Y;
 
 generate
-	if (!A_SIGNED && 0 < A_WIDTH && A_WIDTH < Y_WIDTH) begin:A
+	if (!A_SIGNED && 0 < A_WIDTH && A_WIDTH < Y_WIDTH) begin:BLOCK1
 		assign Y[A_WIDTH-1:0] = A_BUF.val;
 		assign Y[Y_WIDTH-1:A_WIDTH] = 0;
-	end else begin:B
+	end else begin:BLOCK2
 		assign Y = +A_BUF.val;
 	end
 endgenerate
@@ -715,16 +715,33 @@ generate
 		\$lut #( .WIDTH(WIDTH-1), .LUT(LUT                  ) ) lut0 ( .I(I[WIDTH-2:0]), .O(lut0_out) );
 		\$lut #( .WIDTH(WIDTH-1), .LUT(LUT >> (2**(WIDTH-1))) ) lut1 ( .I(I[WIDTH-2:0]), .O(lut1_out) );
 	end
+
+	if (WIDTH > 0) begin:lutlogic
+		always @* begin
+			casez ({I[WIDTH-1], lut0_out, lut1_out})
+				3'b?11: O = 1'b1;
+				3'b?00: O = 1'b0;
+				3'b0??: O = lut0_out;
+				3'b1??: O = lut1_out;
+				default: O = 1'bx;
+			endcase
+		end
+	end
 endgenerate
 
+endmodule
+
+// --------------------------------------------------------
+
+module \$assert (A, EN);
+
+input A, EN;
+
 always @* begin
-	casez ({I[WIDTH-1], lut0_out, lut1_out})
-		3'b?11: O = 1'b1;
-		3'b?00: O = 1'b0;
-		3'b0??: O = lut0_out;
-		3'b1??: O = lut1_out;
-		default: O = 1'bx;
-	endcase
+	if (A !== 1'b1 && EN === 1'b1) begin
+		$display("Assertation failed!");
+		$finish;
+	end
 end
 
 endmodule
@@ -953,8 +970,10 @@ input [ABITS-1:0] ADDR;
 output [WIDTH-1:0] DATA;
 
 initial begin
-	$display("ERROR: Found non-simulatable instance of $memrd!");
-	$finish;
+	if (MEMID != "") begin
+		$display("ERROR: Found non-simulatable instance of $memrd!");
+		$finish;
+	end
 end
 
 endmodule
@@ -975,8 +994,10 @@ input [ABITS-1:0] ADDR;
 input [WIDTH-1:0] DATA;
 
 initial begin
-	$display("ERROR: Found non-simulatable instance of $memwr!");
-	$finish;
+	if (MEMID != "") begin
+		$display("ERROR: Found non-simulatable instance of $memwr!");
+		$finish;
+	end
 end
 
 endmodule
@@ -1008,7 +1029,7 @@ input [WR_PORTS*ABITS-1:0] WR_ADDR;
 input [WR_PORTS*WIDTH-1:0] WR_DATA;
 
 reg [WIDTH-1:0] data [SIZE-1:0];
-event update_async_rd;
+reg update_async_rd;
 
 genvar i;
 generate
@@ -1032,21 +1053,21 @@ generate
 			always @(WR_ADDR or WR_DATA or WR_EN) begin
 				if (WR_EN[i]) begin
 					data[ WR_ADDR[ (i+1)*ABITS-1 : i*ABITS ] - OFFSET ] <= WR_DATA[ (i+1)*WIDTH-1 : i*WIDTH ];
-					#1 -> update_async_rd;
+					update_async_rd <= 1; update_async_rd <= 0;
 				end
 			end
 		end else
-		if (RD_CLK_POLARITY[i] == 1) begin:rd_posclk
+		if (WR_CLK_POLARITY[i] == 1) begin:rd_posclk
 			always @(posedge WR_CLK[i])
 				if (WR_EN[i]) begin
 					data[ WR_ADDR[ (i+1)*ABITS-1 : i*ABITS ] - OFFSET ] <= WR_DATA[ (i+1)*WIDTH-1 : i*WIDTH ];
-					#1 -> update_async_rd;
+					update_async_rd <= 1; update_async_rd <= 0;
 				end
 		end else begin:rd_negclk
 			always @(negedge WR_CLK[i])
 				if (WR_EN[i]) begin
 					data[ WR_ADDR[ (i+1)*ABITS-1 : i*ABITS ] - OFFSET ] <= WR_DATA[ (i+1)*WIDTH-1 : i*WIDTH ];
-					#1 -> update_async_rd;
+					update_async_rd <= 1; update_async_rd <= 0;
 				end
 		end
 	end