20 files changed, 472 insertions, 93 deletions
diff --git a/.editorconfig b/.editorconfig
new file mode 100644
index 000000000..4d6f5ef7a
--- /dev/null
+++ b/.editorconfig
@@ -0,0 +1,7 @@
+root = true
+
+[*]
+indent_style = tab
+indent_size = tab
+trim_trailing_whitespace = true
+insert_final_newline = true
diff --git a/Makefile b/Makefile
index 8da6315fb..128539f6a 100644
--- a/Makefile
+++ b/Makefile
@@ -72,6 +72,7 @@ PKG_CONFIG ?= pkg-config
 SED ?= sed
 BISON ?= bison
 STRIP ?= strip
+AWK ?= awk
 
 ifeq ($(OS), Darwin)
 PLUGIN_LDFLAGS += -undefined dynamic_lookup
@@ -395,8 +396,8 @@ endef
 ifeq ($(PRETTY), 1)
 P_STATUS = 0
 P_OFFSET = 0
-P_UPDATE = $(eval P_STATUS=$(shell echo $(OBJS) yosys$(EXE) | gawk 'BEGIN { RS = " "; I = $(P_STATUS)+0; } $$1 == "$@" && NR > I { I = NR; } END { print I; }'))
-P_SHOW = [$(shell gawk "BEGIN { N=$(words $(OBJS) yosys$(EXE)); printf \"%3d\", $(P_OFFSET)+90*$(P_STATUS)/N; exit; }")%]
+P_UPDATE = $(eval P_STATUS=$(shell echo $(OBJS) yosys$(EXE) | $(AWK) 'BEGIN { RS = " "; I = $(P_STATUS)+0; } $$1 == "$@" && NR > I { I = NR; } END { print I; }'))
+P_SHOW = [$(shell $(AWK) "BEGIN { N=$(words $(OBJS) yosys$(EXE)); printf \"%3d\", $(P_OFFSET)+90*$(P_STATUS)/N; exit; }")%]
 P = @echo "$(if $(findstring $@,$(TARGETS) $(EXTRA_TARGETS)),$(eval P_OFFSET = 10))$(call P_UPDATE)$(call P_SHOW) Building $@";
 Q = @
 S = -s
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 58d2a8625..ab2702807 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -506,6 +506,18 @@ struct BtorWorker
 				}
 			}
 
+			Const initval;
+			for (int i = 0; i < GetSize(sig_q); i++)
+				if (initbits.count(sig_q[i]))
+					initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0);
+				else
+					initval.bits.push_back(State::Sx);
+
+			int nid_init_val = -1;
+
+			if (!initval.is_fully_undef())
+				nid_init_val = get_sig_nid(initval);
+
 			int sid = get_bv_sid(GetSize(sig_q));
 			int nid = next_nid++;
 
@@ -514,15 +526,7 @@ struct BtorWorker
 			else
 				btorf("%d state %d %s\n", nid, sid, log_id(symbol));
 
-			Const initval;
-			for (int i = 0; i < GetSize(sig_q); i++)
-				if (initbits.count(sig_q[i]))
-					initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0);
-				else
-					initval.bits.push_back(State::Sx);
-
-			if (!initval.is_fully_undef()) {
-				int nid_init_val = get_sig_nid(initval);
+			if (nid_init_val >= 0) {
 				int nid_init = next_nid++;
 				if (verbose)
 					btorf("; initval = %s\n", log_signal(initval));
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index b944ee004..721a395e3 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -32,6 +32,7 @@ cexfile = None
 aimfile = None
 aiwfile = None
 aigheader = True
+btorwitfile = None
 vlogtbfile = None
 vlogtbtop = None
 inconstr = list()
@@ -92,6 +93,9 @@ yosys-smtbmc [options] <yosys_smt2_output>
         the AIGER witness file does not include the status and
         properties lines.
 
+    --btorwit <btor_witness_filename>
+        read a BTOR witness.
+
     --noinfo
         only run the core proof, do not collect and print any
         additional information (e.g. which assert failed)
@@ -152,7 +156,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
 
 try:
     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
-            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "presat",
+            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
              "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
              "smtc-init", "smtc-top=", "noinit"])
 except:
@@ -189,6 +193,8 @@ for o, a in opts:
             aiwfile = a + ".aiw"
     elif o == "--aig-noheader":
         aigheader = False
+    elif o == "--btorwit":
+        btorwitfile = a
     elif o == "--dump-vcd":
         vcdfile = a
     elif o == "--dump-vlogtb":
@@ -575,6 +581,103 @@ if aimfile is not None:
                 num_steps = max(num_steps, step+1)
             step += 1
 
+if btorwitfile is not None:
+    with open(btorwitfile, "r") as f:
+        step = None
+        suffix = None
+        altsuffix = None
+        header_okay = False
+
+        for line in f:
+            line = line.strip()
+
+            if line == "sat":
+                header_okay = True
+                continue
+
+            if not header_okay:
+                continue
+
+            if line == "" or line[0] == "b" or line[0] == "j":
+                continue
+
+            if line == ".":
+                break
+
+            if line[0] == '#' or line[0] == '@':
+                step = int(line[1:])
+                suffix = line
+                altsuffix = suffix
+                if suffix[0] == "@":
+                    altsuffix = "#" + suffix[1:]
+                else:
+                    altsuffix = "@" + suffix[1:]
+                continue
+
+            line = line.split()
+
+            if len(line) == 0:
+                continue
+
+            if line[-1].endswith(suffix):
+                line[-1] = line[-1][0:len(line[-1]) - len(suffix)]
+
+            if line[-1].endswith(altsuffix):
+                line[-1] = line[-1][0:len(line[-1]) - len(altsuffix)]
+
+            if line[-1][0] == "$":
+                continue
+
+            # BV assignments
+            if len(line) == 3 and line[1][0] != "[":
+                value = line[1]
+                name = line[2]
+
+                path = smt.get_path(topmod, name)
+
+                if not smt.net_exists(topmod, path):
+                    continue
+
+                width = smt.net_width(topmod, path)
+
+                if width == 1:
+                    assert value in ["0", "1"]
+                    value = "true" if value == "1" else "false"
+                else:
+                    value = "#b" + value
+
+                smtexpr = "(= [%s] %s)" % (name, value)
+                constr_assumes[step].append((btorwitfile, smtexpr))
+
+            # Array assignments
+            if len(line) == 4 and line[1][0] == "[":
+                index = line[1]
+                value = line[2]
+                name = line[3]
+
+                path = smt.get_path(topmod, name)
+
+                if not smt.mem_exists(topmod, path):
+                    continue
+
+                meminfo = smt.mem_info(topmod, path)
+
+                if meminfo[1] == 1:
+                    assert value in ["0", "1"]
+                    value = "true" if value == "1" else "false"
+                else:
+                    value = "#b" + value
+
+                assert index[0] == "["
+                assert index[-1] == "]"
+                index = "#b" + index[1:-1]
+
+                smtexpr = "(= (select [%s] %s) %s)" % (name, index, value)
+                constr_assumes[step].append((btorwitfile, smtexpr))
+
+        skip_steps = step
+        num_steps = step+1
+
 def write_vcd_trace(steps_start, steps_stop, index):
     filename = vcdfile.replace("%", index)
     print_msg("Writing trace to VCD file: %s" % (filename))
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 850abfad7..3a47b478f 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -1352,6 +1352,8 @@ void dump_process(std::ostream &f, std::string indent, RTLIL::Process *proc, boo
 
 		if (sync->type == RTLIL::STa) {
 			f << stringf("%s" "always @* begin\n", indent.c_str());
+		} else if (sync->type == RTLIL::STi) {
+			f << stringf("%s" "initial begin\n", indent.c_str());
 		} else {
 			f << stringf("%s" "always @(", indent.c_str());
 			if (sync->type == RTLIL::STp || sync->type == RTLIL::ST1)
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 5ab1b62df..51e112ed3 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -35,6 +35,7 @@
 
 %{
 #include <list>
+#include <stack>
 #include <string.h>
 #include "frontends/verilog/verilog_frontend.h"
 #include "kernel/log.h"
@@ -47,7 +48,8 @@ YOSYS_NAMESPACE_BEGIN
 namespace VERILOG_FRONTEND {
 	int port_counter;
 	std::map<std::string, int> port_stubs;
-	std::map<std::string, AstNode*> attr_list, default_attr_list;
+	std::map<std::string, AstNode*> *attr_list, default_attr_list;
+	std::stack<std::map<std::string, AstNode*> *> attr_list_stack;
 	std::map<std::string, AstNode*> *albuf;
 	std::vector<AstNode*> ast_stack;
 	struct AstNode *astbuf1, *astbuf2, *astbuf3;
@@ -175,15 +177,18 @@ design:
 
 attr:
 	{
-		for (auto &it : attr_list)
-			delete it.second;
-		attr_list.clear();
+		if (attr_list != nullptr)
+			attr_list_stack.push(attr_list);
+		attr_list = new std::map<std::string, AstNode*>;
 		for (auto &it : default_attr_list)
-			attr_list[it.first] = it.second->clone();
+			(*attr_list)[it.first] = it.second->clone();
 	} attr_opt {
-		std::map<std::string, AstNode*> *al = new std::map<std::string, AstNode*>;
-		al->swap(attr_list);
-		$$ = al;
+		$$ = attr_list;
+		if (!attr_list_stack.empty()) {
+			attr_list = attr_list_stack.top();
+			attr_list_stack.pop();
+		} else
+			attr_list = nullptr;
 	};
 
 attr_opt:
@@ -192,15 +197,20 @@ attr_opt:
 
 defattr:
 	DEFATTR_BEGIN {
+		if (attr_list != nullptr)
+			attr_list_stack.push(attr_list);
+		attr_list = new std::map<std::string, AstNode*>;
 		for (auto &it : default_attr_list)
 			delete it.second;
 		default_attr_list.clear();
-		for (auto &it : attr_list)
-			delete it.second;
-		attr_list.clear();
 	} opt_attr_list {
-		default_attr_list = attr_list;
-		attr_list.clear();
+		attr_list->swap(default_attr_list);
+		delete attr_list;
+		if (!attr_list_stack.empty()) {
+			attr_list = attr_list_stack.top();
+			attr_list_stack.pop();
+		} else
+			attr_list = nullptr;
 	} DEFATTR_END;
 
 opt_attr_list:
@@ -212,15 +222,15 @@ attr_list:
 
 attr_assign:
 	hierarchical_id {
-		if (attr_list.count(*$1) != 0)
-			delete attr_list[*$1];
-		attr_list[*$1] = AstNode::mkconst_int(1, false);
+		if (attr_list->count(*$1) != 0)
+			delete (*attr_list)[*$1];
+		(*attr_list)[*$1] = AstNode::mkconst_int(1, false);
 		delete $1;
 	} |
 	hierarchical_id '=' expr {
-		if (attr_list.count(*$1) != 0)
-			delete attr_list[*$1];
-		attr_list[*$1] = $3;
+		if (attr_list->count(*$1) != 0)
+			delete (*attr_list)[*$1];
+		(*attr_list)[*$1] = $3;
 		delete $1;
 	};
 
diff --git a/passes/cmds/rename.cc b/passes/cmds/rename.cc
index dce576fdf..4b4af0a40 100644
--- a/passes/cmds/rename.cc
+++ b/passes/cmds/rename.cc
@@ -52,6 +52,15 @@ static void rename_in_module(RTLIL::Module *module, std::string from_name, std::
 	log_cmd_error("Object `%s' not found!\n", from_name.c_str());
 }
 
+static std::string derive_name_from_src(const std::string &src, int counter)
+{
+	std::string src_base = src.substr(0, src.find('|'));
+	if (src_base.empty())
+		return stringf("$%d", counter);
+	else
+		return stringf("\\%s$%d", src_base.c_str(), counter);
+}
+
 struct RenamePass : public Pass {
 	RenamePass() : Pass("rename", "rename object in the design") { }
 	void help() YS_OVERRIDE
@@ -63,6 +72,10 @@ struct RenamePass : public Pass {
 		log("Rename the specified object. Note that selection patterns are not supported\n");
 		log("by this command.\n");
 		log("\n");
+		log("    rename -src [selection]\n");
+		log("\n");
+		log("Assign names auto-generated from the src attribute to all selected wires and\n");
+		log("cells with private names.\n");
 		log("\n");
 		log("    rename -enumerate [-pattern <pattern>] [selection]\n");
 		log("\n");
@@ -84,6 +97,7 @@ struct RenamePass : public Pass {
 	void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
 	{
 		std::string pattern_prefix = "_", pattern_suffix = "_";
+		bool flag_src = false;
 		bool flag_enumerate = false;
 		bool flag_hide = false;
 		bool flag_top = false;
@@ -93,6 +107,11 @@ struct RenamePass : public Pass {
 		for (argidx = 1; argidx < args.size(); argidx++)
 		{
 			std::string arg = args[argidx];
+			if (arg == "-src" && !got_mode) {
+				flag_src = true;
+				got_mode = true;
+				continue;
+			}
 			if (arg == "-enumerate" && !got_mode) {
 				flag_enumerate = true;
 				got_mode = true;
@@ -117,6 +136,37 @@ struct RenamePass : public Pass {
 			break;
 		}
 
+		if (flag_src)
+		{
+			extra_args(args, argidx, design);
+
+			for (auto &mod : design->modules_)
+			{
+				int counter = 0;
+
+				RTLIL::Module *module = mod.second;
+				if (!design->selected(module))
+					continue;
+
+				dict<RTLIL::IdString, RTLIL::Wire*> new_wires;
+				for (auto &it : module->wires_) {
+					if (it.first[0] == '$' && design->selected(module, it.second))
+						it.second->name = derive_name_from_src(it.second->get_src_attribute(), counter++);
+					new_wires[it.second->name] = it.second;
+				}
+				module->wires_.swap(new_wires);
+				module->fixup_ports();
+
+				dict<RTLIL::IdString, RTLIL::Cell*> new_cells;
+				for (auto &it : module->cells_) {
+					if (it.first[0] == '$' && design->selected(module, it.second))
+						it.second->name = derive_name_from_src(it.second->get_src_attribute(), counter++);
+					new_cells[it.second->name] = it.second;
+				}
+				module->cells_.swap(new_cells);
+			}
+		}
+		else
 		if (flag_enumerate)
 		{
 			extra_args(args, argidx, design);
diff --git a/passes/equiv/Makefile.inc b/passes/equiv/Makefile.inc
index dd7b3be02..27ea54b22 100644
--- a/passes/equiv/Makefile.inc
+++ b/passes/equiv/Makefile.inc
@@ -9,4 +9,4 @@ OBJS += passes/equiv/equiv_induct.o
 OBJS += passes/equiv/equiv_struct.o
 OBJS += passes/equiv/equiv_purge.o
 OBJS += passes/equiv/equiv_mark.o
-
+OBJS += passes/equiv/equiv_opt.o
diff --git a/passes/equiv/equiv_opt.cc b/passes/equiv/equiv_opt.cc
new file mode 100644
index 000000000..86550a69b
--- /dev/null
+++ b/passes/equiv/equiv_opt.cc
@@ -0,0 +1,157 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2018  whitequark <whitequark@whitequark.org>
+ *
+ *  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"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct EquivOptPass:public ScriptPass
+{
+	EquivOptPass() : ScriptPass("equiv_opt", "prove equivalence for optimized circuit") { }
+
+	void help() YS_OVERRIDE
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    equiv_opt [options] [command]\n");
+		log("\n");
+		log("This command checks circuit equivalence before and after an optimization pass.\n");
+		log("\n");
+		log("    -run <from_label>:<to_label>\n");
+		log("        only run the commands between the labels (see below). an empty\n");
+		log("        from label is synonymous to the start of the command list, and empty to\n");
+		log("        label is synonymous to the end of the command list.\n");
+		log("\n");
+		log("    -map <filename>\n");
+		log("        expand the modules in this file before proving equivalence. this is\n");
+		log("        useful for handling architecture-specific primitives.\n");
+		log("\n");
+		log("    -assert\n");
+		log("        produce an error if the circuits are not equivalent\n");
+		log("\n");
+		log("The following commands are executed by this verification command:\n");
+		help_script();
+		log("\n");
+	}
+
+	std::string command, techmap_opts;
+	bool assert;
+
+	void clear_flags() YS_OVERRIDE
+	{
+		command = "";
+		techmap_opts = "";
+		assert = false;
+	}
+
+	void execute(std::vector < std::string > args, RTLIL::Design * design) YS_OVERRIDE
+	{
+		string run_from, run_to;
+		clear_flags();
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-run" && argidx + 1 < args.size()) {
+				size_t pos = args[argidx + 1].find(':');
+				if (pos == std::string::npos)
+					break;
+				run_from = args[++argidx].substr(0, pos);
+				run_to = args[argidx].substr(pos + 1);
+				continue;
+			}
+			if (args[argidx] == "-map" && argidx + 1 < args.size()) {
+				techmap_opts += " -map " + args[++argidx];
+				continue;
+			}
+			if (args[argidx] == "-assert") {
+				assert = true;
+				continue;
+			}
+			break;
+		}
+
+		for (; argidx < args.size(); argidx++) {
+			if (command.empty()) {
+				if (args[argidx].substr(0, 1) == "-")
+					cmd_error(args, argidx, "Unknown option.");
+			} else {
+				command += " ";
+			}
+			command += args[argidx];
+		}
+
+		if (command.empty())
+			log_cmd_error("No optimization pass specified!\n");
+
+		if (!design->full_selection())
+			log_cmd_error("This command only operates on fully selected designs!\n");
+
+		log_header(design, "Executing EQUIV_OPT pass.\n");
+		log_push();
+
+		run_script(design, run_from, run_to);
+
+		log_pop();
+	}
+
+	void script() YS_OVERRIDE
+	{
+		if (check_label("run_pass")) {
+			run("hierarchy -auto-top");
+			run("design -save preopt");
+			if (help_mode)
+				run("[command]");
+			else
+				run(command);
+			run("design -stash postopt");
+		}
+
+		if (check_label("prepare")) {
+			run("design -copy-from preopt  -as gold A:top");
+			run("design -copy-from postopt -as gate A:top");
+		}
+
+		if ((!techmap_opts.empty() || help_mode) && check_label("techmap", "(only with -map)")) {
+			string opts;
+			if (help_mode)
+				opts = " -map <filename> ...";
+			else
+				opts = techmap_opts;
+			run("techmap -D EQUIV -autoproc" + opts);
+		}
+
+		if (check_label("prove")) {
+			run("equiv_make gold gate equiv");
+			run("equiv_induct equiv");
+			if (help_mode)
+				run("equiv_status [-assert] equiv");
+			else if (assert)
+				run("equiv_status -assert equiv");
+			else
+				run("equiv_status equiv");
+		}
+
+		if (check_label("restore")) {
+			run("design -load preopt");
+		}
+	}
+} EquivOptPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/memory/memory_bram.cc b/passes/memory/memory_bram.cc
index 8740042c4..cf4095d06 100644
--- a/passes/memory/memory_bram.cc
+++ b/passes/memory/memory_bram.cc
@@ -472,8 +472,12 @@ bool replace_cell(Cell *cell, const rules_t &rules, const rules_t::bram_t &bram,
 		std::vector<SigSpec> new_wr_en(GetSize(old_wr_en));
 		std::vector<SigSpec> new_wr_data(GetSize(old_wr_data));
 		std::vector<SigSpec> new_rd_data(GetSize(old_rd_data));
+		std::vector<std::vector<State>> new_initdata;
 		std::vector<int> shuffle_map;
 
+		if (cell_init)
+			new_initdata.resize(mem_size);
+
 		for (auto &it : en_order)
 		{
 			auto &bits = bits_wr_en.at(it);
@@ -489,6 +493,10 @@ bool replace_cell(Cell *cell, const rules_t &rules, const rules_t::bram_t &bram,
 				}
 				for (int j = 0; j < rd_ports; j++)
 					new_rd_data[j].append(old_rd_data[j][bits[i]]);
+				if (cell_init) {
+					for (int j = 0; j < mem_size; j++)
+						new_initdata[j].push_back(initdata[j][bits[i]]);
+				}
 				shuffle_map.push_back(bits[i]);
 			}
 
@@ -499,6 +507,10 @@ bool replace_cell(Cell *cell, const rules_t &rules, const rules_t::bram_t &bram,
 				}
 				for (int j = 0; j < rd_ports; j++)
 					new_rd_data[j].append(State::Sx);
+				if (cell_init) {
+					for (int j = 0; j < mem_size; j++)
+						new_initdata[j].push_back(State::Sx);
+				}
 				shuffle_map.push_back(-1);
 			}
 		}
@@ -522,6 +534,11 @@ bool replace_cell(Cell *cell, const rules_t &rules, const rules_t::bram_t &bram,
 
 		for (int i = 0; i < rd_ports; i++)
 			rd_data.replace(i*mem_width, new_rd_data[i]);
+
+		if (cell_init) {
+			for (int i = 0; i < mem_size; i++)
+				initdata[i] = Const(new_initdata[i]);
+		}
 	}
 
 	// assign write ports
diff --git a/passes/opt/opt_lut.cc b/passes/opt/opt_lut.cc
index ba2cc6ee7..be050c713 100644
--- a/passes/opt/opt_lut.cc
+++ b/passes/opt/opt_lut.cc
@@ -58,7 +58,7 @@ struct OptLutWorker
 			}
 		}
 
-		return lut_table.extract(lut_index).as_int();
+		return lut_table.extract(lut_index).as_bool();
 	}
 
 	void show_stats_by_arity()
diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc
index d2d15a4a9..d3bdd555b 100644
--- a/passes/techmap/abc.cc
+++ b/passes/techmap/abc.cc
@@ -329,6 +329,18 @@ void extract_cell(RTLIL::Cell *cell, bool keepff)
 
 std::string remap_name(RTLIL::IdString abc_name)
 {
+	std::string abc_sname = abc_name.substr(1);
+	if (abc_sname.substr(0, 5) == "ys__n") {
+		int sid = std::stoi(abc_sname.substr(5));
+		bool inv = abc_sname.back() == 'v';
+		for (auto sig : signal_list) {
+			if (sig.id == sid) {
+				std::stringstream sstr;
+				sstr << "$abc$" << map_autoidx << "$" << log_signal(sig.bit) << (inv ? "_inv" : "");
+				return sstr.str();
+			}
+		}
+	}
 	std::stringstream sstr;
 	sstr << "$abc$" << map_autoidx << "$" << abc_name.substr(1);
 	return sstr.str();
@@ -353,12 +365,12 @@ void dump_loop_graph(FILE *f, int &nr, std::map<int, std::set<int>> &edges, std:
 	}
 
 	for (auto n : nodes)
-		fprintf(f, "  n%d [label=\"%s\\nid=%d, count=%d\"%s];\n", n, log_signal(signal_list[n].bit),
+		fprintf(f, "  ys__n%d [label=\"%s\\nid=%d, count=%d\"%s];\n", n, log_signal(signal_list[n].bit),
 				n, in_counts[n], workpool.count(n) ? ", shape=box" : "");
 
 	for (auto &e : edges)
 	for (auto n : e.second)
-		fprintf(f, "  n%d -> n%d;\n", e.first, n);
+		fprintf(f, "  ys__n%d -> ys__n%d;\n", e.first, n);
 
 	fprintf(f, "}\n");
 }
@@ -624,7 +636,7 @@ struct abc_output_filter
 void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::string script_file, std::string exe_file,
 		std::string liberty_file, std::string constr_file, bool cleanup, vector<int> lut_costs, bool dff_mode, std::string clk_str,
 		bool keepff, std::string delay_target, std::string sop_inputs, std::string sop_products, std::string lutin_shared, bool fast_mode,
-		const std::vector<RTLIL::Cell*> &cells, bool show_tempdir, bool sop_mode)
+		const std::vector<RTLIL::Cell*> &cells, bool show_tempdir, bool sop_mode, bool abc_dress)
 {
 	module = current_module;
 	map_autoidx = autoidx++;
@@ -728,7 +740,8 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 
 	for (size_t pos = abc_script.find("{S}"); pos != std::string::npos; pos = abc_script.find("{S}", pos))
 		abc_script = abc_script.substr(0, pos) + lutin_shared + abc_script.substr(pos+3);
-
+	if (abc_dress)
+		abc_script += "; dress";
 	abc_script += stringf("; write_blif %s/output.blif", tempdir_name.c_str());
 	abc_script = add_echos_to_abc_cmd(abc_script);
 
@@ -784,7 +797,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 	for (auto &si : signal_list) {
 		if (!si.is_port || si.type != G(NONE))
 			continue;
-		fprintf(f, " n%d", si.id);
+		fprintf(f, " ys__n%d", si.id);
 		pi_map[count_input++] = log_signal(si.bit);
 	}
 	if (count_input == 0)
@@ -796,17 +809,17 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 	for (auto &si : signal_list) {
 		if (!si.is_port || si.type == G(NONE))
 			continue;
-		fprintf(f, " n%d", si.id);
+		fprintf(f, " ys__n%d", si.id);
 		po_map[count_output++] = log_signal(si.bit);
 	}
 	fprintf(f, "\n");
 
 	for (auto &si : signal_list)
-		fprintf(f, "# n%-5d %s\n", si.id, log_signal(si.bit));
+		fprintf(f, "# ys__n%-5d %s\n", si.id, log_signal(si.bit));
 
 	for (auto &si : signal_list) {
 		if (si.bit.wire == NULL) {
-			fprintf(f, ".names n%d\n", si.id);
+			fprintf(f, ".names ys__n%d\n", si.id);
 			if (si.bit == RTLIL::State::S1)
 				fprintf(f, "1\n");
 		}
@@ -815,68 +828,68 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 	int count_gates = 0;
 	for (auto &si : signal_list) {
 		if (si.type == G(BUF)) {
-			fprintf(f, ".names n%d n%d\n", si.in1, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d\n", si.in1, si.id);
 			fprintf(f, "1 1\n");
 		} else if (si.type == G(NOT)) {
-			fprintf(f, ".names n%d n%d\n", si.in1, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d\n", si.in1, si.id);
 			fprintf(f, "0 1\n");
 		} else if (si.type == G(AND)) {
-			fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d ys__n%d\n", si.in1, si.in2, si.id);
 			fprintf(f, "11 1\n");
 		} else if (si.type == G(NAND)) {
-			fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d ys__n%d\n", si.in1, si.in2, si.id);
 			fprintf(f, "0- 1\n");
 			fprintf(f, "-0 1\n");
 		} else if (si.type == G(OR)) {
-			fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d ys__n%d\n", si.in1, si.in2, si.id);
 			fprintf(f, "-1 1\n");
 			fprintf(f, "1- 1\n");
 		} else if (si.type == G(NOR)) {
-			fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d ys__n%d\n", si.in1, si.in2, si.id);
 			fprintf(f, "00 1\n");
 		} else if (si.type == G(XOR)) {
-			fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d ys__n%d\n", si.in1, si.in2, si.id);
 			fprintf(f, "01 1\n");
 			fprintf(f, "10 1\n");
 		} else if (si.type == G(XNOR)) {
-			fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d ys__n%d\n", si.in1, si.in2, si.id);
 			fprintf(f, "00 1\n");
 			fprintf(f, "11 1\n");
 		} else if (si.type == G(ANDNOT)) {
-			fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d ys__n%d\n", si.in1, si.in2, si.id);
 			fprintf(f, "10 1\n");
 		} else if (si.type == G(ORNOT)) {
-			fprintf(f, ".names n%d n%d n%d\n", si.in1, si.in2, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d ys__n%d\n", si.in1, si.in2, si.id);
 			fprintf(f, "1- 1\n");
 			fprintf(f, "-0 1\n");
 		} else if (si.type == G(MUX)) {
-			fprintf(f, ".names n%d n%d n%d n%d\n", si.in1, si.in2, si.in3, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d ys__n%d ys__n%d\n", si.in1, si.in2, si.in3, si.id);
 			fprintf(f, "1-0 1\n");
 			fprintf(f, "-11 1\n");
 		} else if (si.type == G(AOI3)) {
-			fprintf(f, ".names n%d n%d n%d n%d\n", si.in1, si.in2, si.in3, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d ys__n%d ys__n%d\n", si.in1, si.in2, si.in3, si.id);
 			fprintf(f, "-00 1\n");
 			fprintf(f, "0-0 1\n");
 		} else if (si.type == G(OAI3)) {
-			fprintf(f, ".names n%d n%d n%d n%d\n", si.in1, si.in2, si.in3, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d ys__n%d ys__n%d\n", si.in1, si.in2, si.in3, si.id);
 			fprintf(f, "00- 1\n");
 			fprintf(f, "--0 1\n");
 		} else if (si.type == G(AOI4)) {
-			fprintf(f, ".names n%d n%d n%d n%d n%d\n", si.in1, si.in2, si.in3, si.in4, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d ys__n%d ys__n%d ys__n%d\n", si.in1, si.in2, si.in3, si.in4, si.id);
 			fprintf(f, "-0-0 1\n");
 			fprintf(f, "-00- 1\n");
 			fprintf(f, "0--0 1\n");
 			fprintf(f, "0-0- 1\n");
 		} else if (si.type == G(OAI4)) {
-			fprintf(f, ".names n%d n%d n%d n%d n%d\n", si.in1, si.in2, si.in3, si.in4, si.id);
+			fprintf(f, ".names ys__n%d ys__n%d ys__n%d ys__n%d ys__n%d\n", si.in1, si.in2, si.in3, si.in4, si.id);
 			fprintf(f, "00-- 1\n");
 			fprintf(f, "--00 1\n");
 		} else if (si.type == G(FF)) {
 			if (si.init == State::S0 || si.init == State::S1) {
-				fprintf(f, ".latch n%d n%d %d\n", si.in1, si.id, si.init == State::S1 ? 1 : 0);
+				fprintf(f, ".latch ys__n%d ys__n%d %d\n", si.in1, si.id, si.init == State::S1 ? 1 : 0);
 				recover_init = true;
 			} else
-				fprintf(f, ".latch n%d n%d 2\n", si.in1, si.id);
+				fprintf(f, ".latch ys__n%d ys__n%d 2\n", si.in1, si.id);
 		} else if (si.type != G(NONE))
 			log_abort();
 		if (si.type != G(NONE))
@@ -889,7 +902,6 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 	log("Extracted %d gates and %d wires to a netlist network with %d inputs and %d outputs.\n",
 			count_gates, GetSize(signal_list), count_input, count_output);
 	log_push();
-
 	if (count_output > 0)
 	{
 		log_header(design, "Executing ABC.\n");
@@ -1213,7 +1225,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 		for (auto &si : signal_list)
 			if (si.is_port) {
 				char buffer[100];
-				snprintf(buffer, 100, "\\n%d", si.id);
+				snprintf(buffer, 100, "\\ys__n%d", si.id);
 				RTLIL::SigSig conn;
 				if (si.type != G(NONE)) {
 					conn.first = si.bit;
@@ -1407,6 +1419,11 @@ struct AbcPass : public Pass {
 		log("        this attribute is a unique integer for each ABC process started. This\n");
 		log("        is useful for debugging the partitioning of clock domains.\n");
 		log("\n");
+		log("    -dress\n");
+		log("        run the 'dress' command after all other ABC commands. This aims to\n");
+		log("        preserve naming by an equivalence check between the original and post-ABC\n");
+		log("        netlists (experimental).\n");
+		log("\n");
 		log("When neither -liberty nor -lut is used, the Yosys standard cell library is\n");
 		log("loaded into ABC before the ABC script is executed.\n");
 		log("\n");
@@ -1441,6 +1458,7 @@ struct AbcPass : public Pass {
 		std::string delay_target, sop_inputs, sop_products, lutin_shared = "-S 1";
 		bool fast_mode = false, dff_mode = false, keepff = false, cleanup = true;
 		bool show_tempdir = false, sop_mode = false;
+		bool abc_dress = false;
 		vector<int> lut_costs;
 		markgroups = false;
 
@@ -1555,6 +1573,10 @@ struct AbcPass : public Pass {
 				map_mux16 = true;
 				continue;
 			}
+			if (arg == "-dress") {
+				abc_dress = true;
+				continue;
+			}
 			if (arg == "-g" && argidx+1 < args.size()) {
 				for (auto g : split_tokens(args[++argidx], ",")) {
 					vector<string> gate_list;
@@ -1704,7 +1726,7 @@ struct AbcPass : public Pass {
 
 			if (!dff_mode || !clk_str.empty()) {
 				abc_module(design, mod, script_file, exe_file, liberty_file, constr_file, cleanup, lut_costs, dff_mode, clk_str, keepff,
-						delay_target, sop_inputs, sop_products, lutin_shared, fast_mode, mod->selected_cells(), show_tempdir, sop_mode);
+						delay_target, sop_inputs, sop_products, lutin_shared, fast_mode, mod->selected_cells(), show_tempdir, sop_mode, abc_dress);
 				continue;
 			}
 
@@ -1849,7 +1871,7 @@ struct AbcPass : public Pass {
 				en_polarity = std::get<2>(it.first);
 				en_sig = assign_map(std::get<3>(it.first));
 				abc_module(design, mod, script_file, exe_file, liberty_file, constr_file, cleanup, lut_costs, !clk_sig.empty(), "$",
-						keepff, delay_target, sop_inputs, sop_products, lutin_shared, fast_mode, it.second, show_tempdir, sop_mode);
+						keepff, delay_target, sop_inputs, sop_products, lutin_shared, fast_mode, it.second, show_tempdir, sop_mode, abc_dress);
 				assign_map.set(mod);
 			}
 		}
diff --git a/passes/techmap/deminout.cc b/passes/techmap/deminout.cc
index 9f0c7bf67..47d0ff416 100644
--- a/passes/techmap/deminout.cc
+++ b/passes/techmap/deminout.cc
@@ -83,9 +83,9 @@ struct DeminoutPass : public Pass {
 						for (auto bit : sigmap(conn.second))
 							bits_used.insert(bit);
 
-					if (conn.first == "\\Y" && cell->type.in("$mux", "$pmux", "$_MUX_", "$_TBUF_"))
+					if (conn.first == "\\Y" && cell->type.in("$mux", "$pmux", "$_MUX_", "$_TBUF_", "$tribuf"))
 					{
-						bool tribuf = (cell->type == "$_TBUF_");
+						bool tribuf = (cell->type == "$_TBUF_" || cell->type == "$tribuf");
 
 						if (!tribuf) {
 							for (auto &c : cell->connections()) {
@@ -113,7 +113,8 @@ struct DeminoutPass : public Pass {
 						{
 							if (bits_numports[bit] > 1 || bits_inout.count(bit))
 								new_input = true, new_output = true;
-
+							if (bit == State::S0 || bit == State::S1)
+								new_output = true;
 							if (bits_written.count(bit)) {
 								new_output = true;
 								if (bits_tribuf.count(bit))
diff --git a/passes/techmap/lut2mux.cc b/passes/techmap/lut2mux.cc
index d32bbff14..a4ed79550 100644
--- a/passes/techmap/lut2mux.cc
+++ b/passes/techmap/lut2mux.cc
@@ -32,7 +32,7 @@ int lut2mux(Cell *cell)
 
 	if (GetSize(sig_a) == 1)
 	{
-		cell->module->addMuxGate(NEW_ID, lut[0], lut[1], sig_a, sig_y);
+		cell->module->addMuxGate(NEW_ID, lut.extract(0)[0], lut.extract(1)[0], sig_a, sig_y);
 	}
 	else
 	{
diff --git a/techlibs/ice40/cells_sim.v b/techlibs/ice40/cells_sim.v
index e0a07af32..38ed45981 100644
--- a/techlibs/ice40/cells_sim.v
+++ b/techlibs/ice40/cells_sim.v
@@ -409,6 +409,7 @@ module SB_RAM40_4K (
 
 	initial begin
 		for (i=0; i<16; i=i+1) begin
+`ifdef YOSYS
 			memory[ 0*16 + i] <= INIT_0[16*i +: 16];
 			memory[ 1*16 + i] <= INIT_1[16*i +: 16];
 			memory[ 2*16 + i] <= INIT_2[16*i +: 16];
@@ -425,6 +426,24 @@ module SB_RAM40_4K (
 			memory[13*16 + i] <= INIT_D[16*i +: 16];
 			memory[14*16 + i] <= INIT_E[16*i +: 16];
 			memory[15*16 + i] <= INIT_F[16*i +: 16];
+`else
+			memory[ 0*16 + i] = INIT_0[16*i +: 16];
+			memory[ 1*16 + i] = INIT_1[16*i +: 16];
+			memory[ 2*16 + i] = INIT_2[16*i +: 16];
+			memory[ 3*16 + i] = INIT_3[16*i +: 16];
+			memory[ 4*16 + i] = INIT_4[16*i +: 16];
+			memory[ 5*16 + i] = INIT_5[16*i +: 16];
+			memory[ 6*16 + i] = INIT_6[16*i +: 16];
+			memory[ 7*16 + i] = INIT_7[16*i +: 16];
+			memory[ 8*16 + i] = INIT_8[16*i +: 16];
+			memory[ 9*16 + i] = INIT_9[16*i +: 16];
+			memory[10*16 + i] = INIT_A[16*i +: 16];
+			memory[11*16 + i] = INIT_B[16*i +: 16];
+			memory[12*16 + i] = INIT_C[16*i +: 16];
+			memory[13*16 + i] = INIT_D[16*i +: 16];
+			memory[14*16 + i] = INIT_E[16*i +: 16];
+			memory[15*16 + i] = INIT_F[16*i +: 16];
+`endif
 		end
 	end
 
@@ -928,6 +947,7 @@ module SB_SPRAM256KA (
 	output reg [15:0] DATAOUT
 );
 `ifndef BLACKBOX
+`ifndef EQUIV
 	reg [15:0] mem [0:16383];
 	wire off = SLEEP || !POWEROFF;
 	integer i;
@@ -954,6 +974,7 @@ module SB_SPRAM256KA (
 		end
 	end
 `endif
+`endif
 endmodule
 
 (* blackbox *)
diff --git a/techlibs/ice40/ice40_ffssr.cc b/techlibs/ice40/ice40_ffssr.cc
index 668df09dd..a7649d7a0 100644
--- a/techlibs/ice40/ice40_ffssr.cc
+++ b/techlibs/ice40/ice40_ffssr.cc
@@ -81,6 +81,9 @@ struct Ice40FfssrPass : public Pass {
 
 			for (auto cell : ff_cells)
 			{
+				if (cell->get_bool_attribute("\\dont_touch"))
+					continue;
+
 				SigSpec sig_d = cell->getPort("\\D");
 
 				if (GetSize(sig_d) < 1)
diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc
index 931a190e7..c2aed873b 100644
--- a/techlibs/ice40/synth_ice40.cc
+++ b/techlibs/ice40/synth_ice40.cc
@@ -235,11 +235,15 @@ struct SynthIce40Pass : public ScriptPass
 			run("techmap -map +/ice40/brams_map.v");
 		}
 
-		if (check_label("fine"))
+		if (check_label("map"))
 		{
 			run("opt -fast -mux_undef -undriven -fine");
 			run("memory_map");
 			run("opt -undriven -fine");
+		}
+
+		if (check_label("map_gates"))
+		{
 			if (nocarry)
 				run("techmap");
 			else
diff --git a/tests/lut/check_map.ys b/tests/lut/check_map.ys
index 6d659891f..dc0aaffc2 100644
--- a/tests/lut/check_map.ys
+++ b/tests/lut/check_map.ys
@@ -1,13 +1,4 @@
-design -save preopt
-
 simplemap
-techmap -map +/gate2lut.v -D LUT_WIDTH=4
+equiv_opt -assert techmap -map +/gate2lut.v -D LUT_WIDTH=4
+design -load postopt
 select -assert-count 1 t:$lut
-design -stash postopt
-
-design -copy-from preopt -as preopt top
-design -copy-from postopt -as postopt top
-equiv_make preopt postopt equiv
-prep -flatten -top equiv
-equiv_induct
-equiv_status -assert
diff --git a/tests/opt/ice40_carry.v b/tests/opt/ice40_carry.v
deleted file mode 100644
index ed938932a..000000000
--- a/tests/opt/ice40_carry.v
+++ /dev/null
@@ -1,3 +0,0 @@
-module SB_CARRY (output CO, input I0, I1, CI);
-    assign CO = (I0 && I1) || ((I0 || I1) && CI);
-endmodule
diff --git a/tests/opt/opt_lut.ys b/tests/opt/opt_lut.ys
index 86ad93bb3..59b12c351 100644
--- a/tests/opt/opt_lut.ys
+++ b/tests/opt/opt_lut.ys
@@ -1,15 +1,4 @@
 read_verilog opt_lut.v
 synth_ice40
 ice40_unlut
-design -save preopt
-
-opt_lut -dlogic SB_CARRY:I0=1:I1=2:CI=3
-design -stash postopt
-
-design -copy-from preopt -as preopt top
-design -copy-from postopt -as postopt top
-equiv_make preopt postopt equiv
-techmap -map ice40_carry.v
-prep -flatten -top equiv
-equiv_induct
-equiv_status -assert
+equiv_opt -map +/ice40/cells_sim.v -assert opt_lut -dlogic SB_CARRY:I0=1:I1=2:CI=3