From edd297fb1cb2d02a01b433327cb513399a171062 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 15 May 2018 13:13:43 +0200
Subject: [PATCH 01/45] Fix iopadmap for cases where IO pins already have
 buffers on them

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 passes/techmap/iopadmap.cc | 36 +++++++++++++++++++++++++++++++++++-
 1 file changed, 35 insertions(+), 1 deletion(-)

diff --git a/passes/techmap/iopadmap.cc b/passes/techmap/iopadmap.cc
index 4acbf7c0d..c20081c64 100644
--- a/passes/techmap/iopadmap.cc
+++ b/passes/techmap/iopadmap.cc
@@ -146,10 +146,34 @@ struct IopadmapPass : public Pass {
 		for (auto module : design->selected_modules())
 		{
 			dict<IdString, pool<int>> skip_wires;
+			pool<SigBit> skip_wire_bits;
+			SigMap sigmap(module);
+
+			for (auto cell : module->cells())
+			{
+				if (cell->type == RTLIL::escape_id(inpad_celltype) && cell->hasPort(RTLIL::escape_id(inpad_portname2)))
+					for (auto bit : sigmap(cell->getPort(RTLIL::escape_id(inpad_portname2))))
+						skip_wire_bits.insert(bit);
+
+				if (cell->type == RTLIL::escape_id(outpad_celltype) && cell->hasPort(RTLIL::escape_id(outpad_portname2)))
+					for (auto bit : sigmap(cell->getPort(RTLIL::escape_id(outpad_portname2))))
+						skip_wire_bits.insert(bit);
+
+				if (cell->type == RTLIL::escape_id(inoutpad_celltype) && cell->hasPort(RTLIL::escape_id(inoutpad_portname2)))
+					for (auto bit : sigmap(cell->getPort(RTLIL::escape_id(inoutpad_portname2))))
+						skip_wire_bits.insert(bit);
+
+				if (cell->type == RTLIL::escape_id(toutpad_celltype) && cell->hasPort(RTLIL::escape_id(toutpad_portname3)))
+					for (auto bit : sigmap(cell->getPort(RTLIL::escape_id(toutpad_portname3))))
+						skip_wire_bits.insert(bit);
+
+				if (cell->type == RTLIL::escape_id(tinoutpad_celltype) && cell->hasPort(RTLIL::escape_id(tinoutpad_portname4)))
+					for (auto bit : sigmap(cell->getPort(RTLIL::escape_id(tinoutpad_portname4))))
+						skip_wire_bits.insert(bit);
+			}
 
 			if (!toutpad_celltype.empty() || !tinoutpad_celltype.empty())
 			{
-				SigMap sigmap(module);
 				dict<SigBit, pair<IdString, pool<IdString>>> tbuf_bits;
 
 				for (auto cell : module->cells())
@@ -177,6 +201,9 @@ struct IopadmapPass : public Pass {
 						if (tbuf_bits.count(mapped_wire_bit) == 0)
 							continue;
 
+						if (skip_wire_bits.count(mapped_wire_bit))
+							continue;
+
 						auto &tbuf_cache = tbuf_bits.at(mapped_wire_bit);
 						Cell *tbuf_cell = module->cell(tbuf_cache.first);
 
@@ -272,6 +299,13 @@ struct IopadmapPass : public Pass {
 					skip_bit_indices = skip_wires.at(wire->name);
 				}
 
+				for (int i = 0; i < GetSize(wire); i++)
+					if (skip_wire_bits.count(sigmap(SigBit(wire, i))))
+						skip_bit_indices.insert(i);
+
+				if (GetSize(wire) == GetSize(skip_bit_indices))
+					continue;
+
 				if (wire->port_input && !wire->port_output) {
 					if (inpad_celltype.empty()) {
 						log("Don't map input port %s.%s: Missing option -inpad.\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(wire->name));

From fe80b39f56fb650cc67bed09f29ea42e0e5f6e52 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 15 May 2018 14:02:27 +0200
Subject: [PATCH 02/45] Fix iopadmap for loops between tristate IO buffers

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 passes/techmap/iopadmap.cc | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

diff --git a/passes/techmap/iopadmap.cc b/passes/techmap/iopadmap.cc
index c20081c64..690ba87ed 100644
--- a/passes/techmap/iopadmap.cc
+++ b/passes/techmap/iopadmap.cc
@@ -175,6 +175,8 @@ struct IopadmapPass : public Pass {
 			if (!toutpad_celltype.empty() || !tinoutpad_celltype.empty())
 			{
 				dict<SigBit, pair<IdString, pool<IdString>>> tbuf_bits;
+				pool<pair<IdString, IdString>> norewrites;
+				SigMap rewrites;
 
 				for (auto cell : module->cells())
 					if (cell->type == "$_TBUF_") {
@@ -246,6 +248,9 @@ struct IopadmapPass : public Pass {
 
 							module->remove(tbuf_cell);
 							skip_wires[wire->name].insert(i);
+
+							norewrites.insert(make_pair(cell->name, RTLIL::escape_id(tinoutpad_portname4)));
+							rewrites.add(sigmap(wire_bit), owire);
 							continue;
 						}
 
@@ -283,6 +288,22 @@ struct IopadmapPass : public Pass {
 						}
 					}
 				}
+
+				if (GetSize(norewrites))
+				{
+					for (auto cell : module->cells())
+					for (auto port : cell->connections())
+					{
+						if (norewrites.count(make_pair(cell->name, port.first)))
+							continue;
+
+						SigSpec orig_sig = sigmap(port.second);
+						SigSpec new_sig = rewrites(orig_sig);
+
+						if (orig_sig != new_sig)
+							cell->setPort(port.first, new_sig);
+					}
+				}
 			}
 
 			for (auto wire : module->selected_wires())

From 4b6c0e331d0ef4188f8fa2443f8f7999231af052 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 15 May 2018 14:19:05 +0200
Subject: [PATCH 03/45] Remove mercurial from build instructions

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 README.md | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/README.md b/README.md
index d5184bd7d..704948e2d 100644
--- a/README.md
+++ b/README.md
@@ -52,19 +52,19 @@ For example on Ubuntu Linux 16.04 LTS the following commands will install all
 prerequisites for building yosys:
 
 	$ sudo apt-get install build-essential clang bison flex \
-		libreadline-dev gawk tcl-dev libffi-dev git mercurial \
+		libreadline-dev gawk tcl-dev libffi-dev git \
 		graphviz xdot pkg-config python3
 
 Similarily, on Mac OS X MacPorts or Homebrew can be used to install dependencies:
 
 	$ brew tap Homebrew/bundle && brew bundle
 	$ sudo port install bison flex readline gawk libffi \
-		git mercurial graphviz pkgconfig python36
+		git graphviz pkgconfig python36
 
 On FreeBSD use the following command to install all prerequisites:
 
 	# pkg install bison flex readline gawk libffi\
-		git mercurial graphviz pkgconfig python3 python36 tcl-wrapper
+		git graphviz pkgconfig python3 python36 tcl-wrapper
 
 On FreeBSD system use gmake instead of make. To run tests use:
     % MAKE=gmake CC=cc gmake test

From a7281930c5877b34e072d90d5ca013f8fda7e2cc Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 15 May 2018 19:27:00 +0200
Subject: [PATCH 04/45] Fix handling of anyconst/anyseq attrs in VHDL code via
 Verific

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verific.cc | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index ee09c7523..624c04be9 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -871,22 +871,22 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 		const char *allconst_attr = net->GetAttValue("allconst");
 		const char *allseq_attr = net->GetAttValue("allseq");
 
-		if (rand_const_attr != nullptr && !strcmp(rand_const_attr, "1"))
+		if (rand_const_attr != nullptr && (!strcmp(rand_const_attr, "1") || !strcmp(rand_const_attr, "'1'")))
 			anyconst_nets.insert(net);
 
-		else if (rand_attr != nullptr && !strcmp(rand_attr, "1"))
+		else if (rand_attr != nullptr && (!strcmp(rand_attr, "1") || !strcmp(rand_attr, "'1'")))
 			anyseq_nets.insert(net);
 
-		else if (anyconst_attr != nullptr && !strcmp(anyconst_attr, "1"))
+		else if (anyconst_attr != nullptr && (!strcmp(anyconst_attr, "1") || !strcmp(anyconst_attr, "'1'")))
 			anyconst_nets.insert(net);
 
-		else if (anyseq_attr != nullptr && !strcmp(anyseq_attr, "1"))
+		else if (anyseq_attr != nullptr && (!strcmp(anyseq_attr, "1") || !strcmp(anyseq_attr, "'1'")))
 			anyseq_nets.insert(net);
 
-		else if (allconst_attr != nullptr && !strcmp(allconst_attr, "1"))
+		else if (allconst_attr != nullptr && (!strcmp(allconst_attr, "1") || !strcmp(allconst_attr, "'1'")))
 			allconst_nets.insert(net);
 
-		else if (allseq_attr != nullptr && !strcmp(allseq_attr, "1"))
+		else if (allseq_attr != nullptr && (!strcmp(allseq_attr, "1") || !strcmp(allseq_attr, "'1'")))
 			allseq_nets.insert(net);
 
 		if (net_map.count(net)) {

From 872d8d49e98fc5a4090ce20d902afbd0090c8c84 Mon Sep 17 00:00:00 2001
From: Jim Paris <jim@jtan.com>
Date: Thu, 17 May 2018 00:06:49 -0400
Subject: [PATCH 05/45] Skip spaces around macro arguments

---
 frontends/verilog/preproc.cc | 1 +
 1 file changed, 1 insertion(+)

diff --git a/frontends/verilog/preproc.cc b/frontends/verilog/preproc.cc
index c43ff4e3a..00124cb42 100644
--- a/frontends/verilog/preproc.cc
+++ b/frontends/verilog/preproc.cc
@@ -244,6 +244,7 @@ static bool try_expand_macro(std::set<std::string> &defines_with_args,
 				args.push_back(std::string());
 				while (1)
 				{
+					skip_spaces();
 					tok = next_token(true);
 					if (tok == ")" || tok == "}" || tok == "]")
 						level--;

From 4a229e5b953c15ecb31945258e0ca2f7bffe8a3e Mon Sep 17 00:00:00 2001
From: Jim Paris <jim@jtan.com>
Date: Thu, 17 May 2018 00:09:56 -0400
Subject: [PATCH 06/45] Support SystemVerilog `` extension for macros

---
 frontends/verilog/preproc.cc | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

diff --git a/frontends/verilog/preproc.cc b/frontends/verilog/preproc.cc
index 00124cb42..dea22ee8a 100644
--- a/frontends/verilog/preproc.cc
+++ b/frontends/verilog/preproc.cc
@@ -183,8 +183,9 @@ static std::string next_token(bool pass_newline = false)
 		const char *ok = "abcdefghijklmnopqrstuvwxyz_ABCDEFGHIJKLMNOPQRSTUVWXYZ$0123456789";
 		if (ch == '`' || strchr(ok, ch) != NULL)
 		{
+			char first = ch;
 			ch = next_char();
-			if (ch == '"') {
+			if (first == '`' && (ch == '"' || ch == '`')) {
 				token += ch;
 			} else do {
 					if (strchr(ok, ch) == NULL) {
@@ -265,6 +266,9 @@ static bool try_expand_macro(std::set<std::string> &defines_with_args,
 			}
 			insert_input(defines_map[name]);
 			return true;
+	} else if (tok == "``") {
+		// Swallow `` in macro expansion
+		return true;
 	} else return false;
 }
 

From faac2c559565a25e58ce95a7ea873df0c30375dc Mon Sep 17 00:00:00 2001
From: Olof Kindgren <olof.kindgren@gmail.com>
Date: Thu, 17 May 2018 13:54:40 +0200
Subject: [PATCH 07/45] Avoid mixing module port declaration styles in ice40
 cells_sim.v

The current code requires workarounds for several simulators
For modelsim, the file must be compiled with -mixedansiports and
xsim needs --relax.
---
 techlibs/ice40/cells_sim.v | 66 +++++++++++++-------------------------
 1 file changed, 23 insertions(+), 43 deletions(-)

diff --git a/techlibs/ice40/cells_sim.v b/techlibs/ice40/cells_sim.v
index 814895e70..45a02111f 100644
--- a/techlibs/ice40/cells_sim.v
+++ b/techlibs/ice40/cells_sim.v
@@ -1,6 +1,6 @@
 
-`define SB_DFF_REG reg Q = 0;
-// `define SB_DFF_REG reg Q;
+`define SB_DFF_REG reg Q = 0
+// `define SB_DFF_REG reg Q
 
 // SiliconBlue IO Cells
 
@@ -132,21 +132,18 @@ endmodule
 
 // Positive Edge SiliconBlue FF Cells
 
-module SB_DFF (output Q, input C, D);
-	`SB_DFF_REG
+module SB_DFF (output `SB_DFF_REG, input C, D);
 	always @(posedge C)
 		Q <= D;
 endmodule
 
-module SB_DFFE (output Q, input C, E, D);
-	`SB_DFF_REG
+module SB_DFFE (output `SB_DFF_REG, input C, E, D);
 	always @(posedge C)
 		if (E)
 			Q <= D;
 endmodule
 
-module SB_DFFSR (output Q, input C, R, D);
-	`SB_DFF_REG
+module SB_DFFSR (output `SB_DFF_REG, input C, R, D);
 	always @(posedge C)
 		if (R)
 			Q <= 0;
@@ -154,8 +151,7 @@ module SB_DFFSR (output Q, input C, R, D);
 			Q <= D;
 endmodule
 
-module SB_DFFR (output Q, input C, R, D);
-	`SB_DFF_REG
+module SB_DFFR (output `SB_DFF_REG, input C, R, D);
 	always @(posedge C, posedge R)
 		if (R)
 			Q <= 0;
@@ -163,8 +159,7 @@ module SB_DFFR (output Q, input C, R, D);
 			Q <= D;
 endmodule
 
-module SB_DFFSS (output Q, input C, S, D);
-	`SB_DFF_REG
+module SB_DFFSS (output `SB_DFF_REG, input C, S, D);
 	always @(posedge C)
 		if (S)
 			Q <= 1;
@@ -172,8 +167,7 @@ module SB_DFFSS (output Q, input C, S, D);
 			Q <= D;
 endmodule
 
-module SB_DFFS (output Q, input C, S, D);
-	`SB_DFF_REG
+module SB_DFFS (output `SB_DFF_REG, input C, S, D);
 	always @(posedge C, posedge S)
 		if (S)
 			Q <= 1;
@@ -181,8 +175,7 @@ module SB_DFFS (output Q, input C, S, D);
 			Q <= D;
 endmodule
 
-module SB_DFFESR (output Q, input C, E, R, D);
-	`SB_DFF_REG
+module SB_DFFESR (output `SB_DFF_REG, input C, E, R, D);
 	always @(posedge C)
 		if (E) begin
 			if (R)
@@ -192,8 +185,7 @@ module SB_DFFESR (output Q, input C, E, R, D);
 		end
 endmodule
 
-module SB_DFFER (output Q, input C, E, R, D);
-	`SB_DFF_REG
+module SB_DFFER (output `SB_DFF_REG, input C, E, R, D);
 	always @(posedge C, posedge R)
 		if (R)
 			Q <= 0;
@@ -201,8 +193,7 @@ module SB_DFFER (output Q, input C, E, R, D);
 			Q <= D;
 endmodule
 
-module SB_DFFESS (output Q, input C, E, S, D);
-	`SB_DFF_REG
+module SB_DFFESS (output `SB_DFF_REG, input C, E, S, D);
 	always @(posedge C)
 		if (E) begin
 			if (S)
@@ -212,8 +203,7 @@ module SB_DFFESS (output Q, input C, E, S, D);
 		end
 endmodule
 
-module SB_DFFES (output Q, input C, E, S, D);
-	`SB_DFF_REG
+module SB_DFFES (output `SB_DFF_REG, input C, E, S, D);
 	always @(posedge C, posedge S)
 		if (S)
 			Q <= 1;
@@ -223,21 +213,18 @@ endmodule
 
 // Negative Edge SiliconBlue FF Cells
 
-module SB_DFFN (output Q, input C, D);
-	`SB_DFF_REG
+module SB_DFFN (output `SB_DFF_REG, input C, D);
 	always @(negedge C)
 		Q <= D;
 endmodule
 
-module SB_DFFNE (output Q, input C, E, D);
-	`SB_DFF_REG
+module SB_DFFNE (output `SB_DFF_REG, input C, E, D);
 	always @(negedge C)
 		if (E)
 			Q <= D;
 endmodule
 
-module SB_DFFNSR (output Q, input C, R, D);
-	`SB_DFF_REG
+module SB_DFFNSR (output `SB_DFF_REG, input C, R, D);
 	always @(negedge C)
 		if (R)
 			Q <= 0;
@@ -245,8 +232,7 @@ module SB_DFFNSR (output Q, input C, R, D);
 			Q <= D;
 endmodule
 
-module SB_DFFNR (output Q, input C, R, D);
-	`SB_DFF_REG
+module SB_DFFNR (output `SB_DFF_REG, input C, R, D);
 	always @(negedge C, posedge R)
 		if (R)
 			Q <= 0;
@@ -254,8 +240,7 @@ module SB_DFFNR (output Q, input C, R, D);
 			Q <= D;
 endmodule
 
-module SB_DFFNSS (output Q, input C, S, D);
-	`SB_DFF_REG
+module SB_DFFNSS (output `SB_DFF_REG, input C, S, D);
 	always @(negedge C)
 		if (S)
 			Q <= 1;
@@ -263,8 +248,7 @@ module SB_DFFNSS (output Q, input C, S, D);
 			Q <= D;
 endmodule
 
-module SB_DFFNS (output Q, input C, S, D);
-	`SB_DFF_REG
+module SB_DFFNS (output `SB_DFF_REG, input C, S, D);
 	always @(negedge C, posedge S)
 		if (S)
 			Q <= 1;
@@ -272,8 +256,7 @@ module SB_DFFNS (output Q, input C, S, D);
 			Q <= D;
 endmodule
 
-module SB_DFFNESR (output Q, input C, E, R, D);
-	`SB_DFF_REG
+module SB_DFFNESR (output `SB_DFF_REG, input C, E, R, D);
 	always @(negedge C)
 		if (E) begin
 			if (R)
@@ -283,8 +266,7 @@ module SB_DFFNESR (output Q, input C, E, R, D);
 		end
 endmodule
 
-module SB_DFFNER (output Q, input C, E, R, D);
-	`SB_DFF_REG
+module SB_DFFNER (output `SB_DFF_REG, input C, E, R, D);
 	always @(negedge C, posedge R)
 		if (R)
 			Q <= 0;
@@ -292,8 +274,7 @@ module SB_DFFNER (output Q, input C, E, R, D);
 			Q <= D;
 endmodule
 
-module SB_DFFNESS (output Q, input C, E, S, D);
-	`SB_DFF_REG
+module SB_DFFNESS (output `SB_DFF_REG, input C, E, S, D);
 	always @(negedge C)
 		if (E) begin
 			if (S)
@@ -303,8 +284,7 @@ module SB_DFFNESS (output Q, input C, E, S, D);
 		end
 endmodule
 
-module SB_DFFNES (output Q, input C, E, S, D);
-	`SB_DFF_REG
+module SB_DFFNES (output `SB_DFF_REG, input C, E, S, D);
 	always @(negedge C, posedge S)
 		if (S)
 			Q <= 1;
@@ -677,7 +657,7 @@ module ICESTORM_LC (
 	parameter [0:0] SET_NORESET  = 0;
 	parameter [0:0] ASYNC_SR     = 0;
 
-	wire COUT = CARRY_ENABLE ? (I1 && I2) || ((I1 || I2) && CIN) : 1'bx;
+	assign COUT = CARRY_ENABLE ? (I1 && I2) || ((I1 || I2) && CIN) : 1'bx;
 
 	wire [7:0] lut_s3 = I3 ? LUT_INIT[15:8] : LUT_INIT[7:0];
 	wire [3:0] lut_s2 = I2 ?   lut_s3[ 7:4] :   lut_s3[3:0];

From 1b210dbfb78469b477ad8e6da795d2c5ea3f8507 Mon Sep 17 00:00:00 2001
From: Robert Ou <rqou@robertou.com>
Date: Fri, 18 May 2018 22:01:25 -0700
Subject: [PATCH 08/45] Makefile: Make abc always use stdint.h

---
 Makefile | 12 ++++++++----
 1 file changed, 8 insertions(+), 4 deletions(-)

diff --git a/Makefile b/Makefile
index 1caa0038b..13caaab8b 100644
--- a/Makefile
+++ b/Makefile
@@ -126,6 +126,7 @@ ifeq ($(CONFIG),clang)
 CXX = clang
 LD = clang++
 CXXFLAGS += -std=c++11 -Os
+ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H"
 
 ifneq ($(SANITIZER),)
 $(info [Clang Sanitizer] $(SANITIZER))
@@ -148,16 +149,19 @@ else ifeq ($(CONFIG),gcc)
 CXX = gcc
 LD = gcc
 CXXFLAGS += -std=c++11 -Os
+ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H"
 
 else ifeq ($(CONFIG),gcc-4.8)
 CXX = gcc-4.8
 LD = gcc-4.8
 CXXFLAGS += -std=c++11 -Os
+ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H"
 
 else ifeq ($(CONFIG),emcc)
 CXX = emcc
 LD = emcc
 CXXFLAGS := -std=c++11 $(filter-out -fPIC -ggdb,$(CXXFLAGS))
+ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H"
 EMCCFLAGS := -Os -Wno-warn-absolute-paths
 EMCCFLAGS += --memory-init-file 0 --embed-file share -s NO_EXIT_RUNTIME=1
 EMCCFLAGS += -s EXPORTED_FUNCTIONS="['_main','_run','_prompt','_errmsg']"
@@ -192,8 +196,8 @@ CXXFLAGS += -std=c++11 -Os -D_POSIX_SOURCE -DYOSYS_MXE_HACKS -Wno-attributes
 CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS))
 LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s
 LDLIBS := $(filter-out -lrt,$(LDLIBS))
-ABCMKARGS += ARCHFLAGS="-DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4 -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w"
-ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" ABC_USE_NO_READLINE=1 CC="$(CXX)" CXX="$(CXX)"
+ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w"
+ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" ABC_USE_NO_READLINE=1
 EXE = .exe
 
 else ifeq ($(CONFIG),msys2)
@@ -203,8 +207,8 @@ CXXFLAGS += -std=c++11 -Os -D_POSIX_SOURCE -DYOSYS_WIN32_UNIX_DIR
 CXXFLAGS := $(filter-out -fPIC,$(CXXFLAGS))
 LDFLAGS := $(filter-out -rdynamic,$(LDFLAGS)) -s
 LDLIBS := $(filter-out -lrt,$(LDLIBS))
-ABCMKARGS += ARCHFLAGS="-DSIZEOF_VOID_P=4 -DSIZEOF_LONG=4 -DSIZEOF_INT=4 -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w"
-ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" ABC_USE_NO_READLINE=0 CC="i686-w64-mingw32-gcc" CXX="$(CXX)"
+ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DWIN32_NO_DLL -DHAVE_STRUCT_TIMESPEC -fpermissive -w"
+ABCMKARGS += LIBS="lib/x86/pthreadVC2.lib -s" ABC_USE_NO_READLINE=0
 EXE = .exe
 
 else ifneq ($(CONFIG),none)

From bfce3a74791e68a194e5c5908429334dfea3738b Mon Sep 17 00:00:00 2001
From: Robert Ou <rqou@robertou.com>
Date: Tue, 14 Nov 2017 02:19:21 -0800
Subject: [PATCH 09/45] Add an option to statically link abc into yosys

This is currently incomplete because the output filter no longer works.
---
 Makefile              | 22 ++++++++++++++++++----
 passes/techmap/abc.cc | 20 ++++++++++++++++++++
 2 files changed, 38 insertions(+), 4 deletions(-)

diff --git a/Makefile b/Makefile
index 13caaab8b..cc42f82d6 100644
--- a/Makefile
+++ b/Makefile
@@ -22,6 +22,7 @@ ENABLE_DEBUG := 0
 ENABLE_NDEBUG := 0
 LINK_CURSES := 0
 LINK_TERMCAP := 0
+LINK_ABC := 0
 
 # clang sanitizers
 SANITIZER =
@@ -292,10 +293,15 @@ endif
 
 ifeq ($(ENABLE_ABC),1)
 CXXFLAGS += -DYOSYS_ENABLE_ABC
+ifeq ($(LINK_ABC),1)
+CXXFLAGS += -DYOSYS_LINK_ABC
+LDLIBS += -lpthread
+else
 ifeq ($(ABCEXTERNAL),)
 TARGETS += yosys-abc$(EXE)
 endif
 endif
+endif
 
 ifeq ($(ENABLE_VERIFIC),1)
 VERIFIC_DIR ?= /usr/local/src/verific_lib_eval
@@ -415,6 +421,10 @@ include techlibs/common/Makefile.inc
 
 endif
 
+ifeq ($(LINK_ABC),1)
+OBJS += yosys-libabc.a
+endif
+
 top-all: $(TARGETS) $(EXTRA_TARGETS)
 	@echo ""
 	@echo "  Build successful."
@@ -459,7 +469,7 @@ yosys-config: misc/yosys-config.in
 			-e 's#@BINDIR@#$(strip $(BINDIR))#;' -e 's#@DATDIR@#$(strip $(DATDIR))#;' < $< > yosys-config
 	$(Q) chmod +x yosys-config
 
-abc/abc-$(ABCREV)$(EXE):
+abc/abc-$(ABCREV)$(EXE) abc/libabc-$(ABCREV).a:
 	$(P)
 ifneq ($(ABCREV),default)
 	$(Q) if test -d abc/.hg; then \
@@ -476,15 +486,19 @@ ifneq ($(ABCREV),default)
 	fi
 endif
 	$(Q) rm -f abc/abc-[0-9a-f]*
-	$(Q) cd abc && $(MAKE) $(S) $(ABCMKARGS) PROG="abc-$(ABCREV)$(EXE)" MSG_PREFIX="$(eval P_OFFSET = 5)$(call P_SHOW)$(eval P_OFFSET = 10) ABC: "
+	$(Q) cd abc && $(MAKE) $(S) $(ABCMKARGS) $(if $(filter %.a,$@),PROG="abc-$(ABCREV)",PROG="abc-$(ABCREV)$(EXE)") MSG_PREFIX="$(eval P_OFFSET = 5)$(call P_SHOW)$(eval P_OFFSET = 10) ABC: " $(if $(filter %.a,$@),libabc-$(ABCREV).a)
 
 ifeq ($(ABCREV),default)
 .PHONY: abc/abc-$(ABCREV)$(EXE)
+.PHONY: abc/libabc-$(ABCREV).a
 endif
 
 yosys-abc$(EXE): abc/abc-$(ABCREV)$(EXE)
 	$(P) cp abc/abc-$(ABCREV)$(EXE) yosys-abc$(EXE)
 
+yosys-libabc.a: abc/libabc-$(ABCREV).a
+	$(P) cp abc/libabc-$(ABCREV).a yosys-libabc.a
+
 ifneq ($(SEED),)
 SEEDOPT="-S $(SEED)"
 else
@@ -568,7 +582,7 @@ clean:
 	rm -rf share
 	if test -d manual; then cd manual && sh clean.sh; fi
 	rm -f $(OBJS) $(GENFILES) $(TARGETS) $(EXTRA_TARGETS) $(EXTRA_OBJS)
-	rm -f kernel/version_*.o kernel/version_*.cc abc/abc-[0-9a-f]*
+	rm -f kernel/version_*.o kernel/version_*.cc abc/abc-[0-9a-f]* abc/libabc-[0-9a-f]*.a
 	rm -f libs/*/*.d frontends/*/*.d passes/*/*.d backends/*/*.d kernel/*.d techlibs/*/*.d
 	rm -rf tests/asicworld/*.out tests/asicworld/*.log
 	rm -rf tests/hana/*.out tests/hana/*.log
@@ -581,7 +595,7 @@ clean:
 
 clean-abc:
 	$(MAKE) -C abc DEP= clean
-	rm -f yosys-abc$(EXE) abc/abc-[0-9a-f]*
+	rm -f yosys-abc$(EXE) yosys-libabc.a abc/abc-[0-9a-f]* abc/libabc-[0-9a-f]*.a
 
 mrproper: clean
 	git clean -xdf
diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc
index 009ba6b97..8e1484301 100644
--- a/passes/techmap/abc.cc
+++ b/passes/techmap/abc.cc
@@ -60,6 +60,10 @@
 
 #include "frontends/blif/blifparse.h"
 
+#ifdef YOSYS_LINK_ABC
+extern "C" int Abc_RealMain(int argc, char *argv[]);
+#endif
+
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
@@ -943,8 +947,24 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 		buffer = stringf("%s -s -f %s/abc.script 2>&1", exe_file.c_str(), tempdir_name.c_str());
 		log("Running ABC command: %s\n", replace_tempdir(buffer, tempdir_name, show_tempdir).c_str());
 
+#ifndef YOSYS_LINK_ABC
 		abc_output_filter filt(tempdir_name, show_tempdir);
 		int ret = run_command(buffer, std::bind(&abc_output_filter::next_line, filt, std::placeholders::_1));
+#else
+		// These needs to be mutable, supposedly due to getopt
+		char *abc_argv[5];
+		string tmp_script_name = stringf("%s/abc.script", tempdir_name.c_str());
+		abc_argv[0] = strdup(exe_file.c_str());
+		abc_argv[1] = strdup("-s");
+		abc_argv[2] = strdup("-f");
+		abc_argv[3] = strdup(tmp_script_name.c_str());
+		abc_argv[4] = 0;
+		int ret = Abc_RealMain(4, abc_argv);
+		free(abc_argv[0]);
+		free(abc_argv[1]);
+		free(abc_argv[2]);
+		free(abc_argv[3]);
+#endif
 		if (ret != 0)
 			log_error("ABC: execution of command \"%s\" failed: return code %d.\n", buffer.c_str(), ret);
 

From 93f79299a5138c966512f9ed2d140f16b1735b70 Mon Sep 17 00:00:00 2001
From: Robert Ou <rqou@robertou.com>
Date: Fri, 18 May 2018 22:42:24 -0700
Subject: [PATCH 10/45] Add options to disable abc's usage of pthreads and
 readline

---
 Makefile | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/Makefile b/Makefile
index cc42f82d6..b664cafc4 100644
--- a/Makefile
+++ b/Makefile
@@ -23,6 +23,8 @@ ENABLE_NDEBUG := 0
 LINK_CURSES := 0
 LINK_TERMCAP := 0
 LINK_ABC := 0
+# Needed for environments that don't have proper thread support (i.e. emscripten)
+DISABLE_ABC_THREADS := 0
 
 # clang sanitizers
 SANITIZER =
@@ -241,9 +243,15 @@ else
 ifeq ($(ENABLE_EDITLINE),1)
 CXXFLAGS += -DYOSYS_ENABLE_EDITLINE
 LDLIBS += -ledit -ltinfo -lbsd
+else
+ABCMKARGS += "ABC_USE_NO_READLINE=1"
 endif
 endif
 
+ifeq ($(DISABLE_ABC_THREADS),1)
+ABCMKARGS += "ABC_USE_NO_PTHREADS=1"
+endif
+
 ifeq ($(ENABLE_PLUGINS),1)
 CXXFLAGS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --cflags libffi) -DYOSYS_ENABLE_PLUGINS
 LDLIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs libffi || echo -lffi)
@@ -295,7 +303,9 @@ ifeq ($(ENABLE_ABC),1)
 CXXFLAGS += -DYOSYS_ENABLE_ABC
 ifeq ($(LINK_ABC),1)
 CXXFLAGS += -DYOSYS_LINK_ABC
+ifeq ($(DISABLE_ABC_THREADS),0)
 LDLIBS += -lpthread
+endif
 else
 ifeq ($(ABCEXTERNAL),)
 TARGETS += yosys-abc$(EXE)

From bd87462b47fdd8d7885269246ec1f7b685c6f86f Mon Sep 17 00:00:00 2001
From: Robert Ou <rqou@robertou.com>
Date: Tue, 14 Nov 2017 04:08:07 -0800
Subject: [PATCH 11/45] Fix reading techlibs under emscripten

---
 kernel/yosys.cc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/kernel/yosys.cc b/kernel/yosys.cc
index aa5901271..750a154e6 100644
--- a/kernel/yosys.cc
+++ b/kernel/yosys.cc
@@ -739,7 +739,7 @@ std::string proc_self_dirname()
 #ifdef EMSCRIPTEN
 std::string proc_share_dirname()
 {
-	return "/share";
+	return "/share/";
 }
 #else
 std::string proc_share_dirname()

From 9763e4d830fa85aeb1577cab4dec9f4becc28f03 Mon Sep 17 00:00:00 2001
From: Robert Ou <rqou@robertou.com>
Date: Tue, 14 Nov 2017 04:08:36 -0800
Subject: [PATCH 12/45] Fix infinite loop in abc command under emscripten

---
 passes/techmap/abc.cc | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc
index 8e1484301..18868c6d7 100644
--- a/passes/techmap/abc.cc
+++ b/passes/techmap/abc.cc
@@ -550,11 +550,13 @@ std::string replace_tempdir(std::string text, std::string tempdir_name, bool sho
 	}
 
 	std::string  selfdir_name = proc_self_dirname();
-	while (1) {
-		size_t pos = text.find(selfdir_name);
-		if (pos == std::string::npos)
-			break;
-		text = text.substr(0, pos) + "<yosys-exe-dir>/" + text.substr(pos + GetSize(selfdir_name));
+	if (selfdir_name != "/") {
+		while (1) {
+			size_t pos = text.find(selfdir_name);
+			if (pos == std::string::npos)
+				break;
+			text = text.substr(0, pos) + "<yosys-exe-dir>/" + text.substr(pos + GetSize(selfdir_name));
+		}
 	}
 
 	return text;

From d9ef793430cf6bec2daeed20fbe44c3b060c435a Mon Sep 17 00:00:00 2001
From: Robert Ou <rqou@robertou.com>
Date: Sat, 31 Mar 2018 14:50:21 -0700
Subject: [PATCH 13/45] Force abc to be linked statically and without threads
 in emscripten

---
 Makefile | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/Makefile b/Makefile
index b664cafc4..1a17bb857 100644
--- a/Makefile
+++ b/Makefile
@@ -178,6 +178,11 @@ EXE = .js
 TARGETS := $(filter-out yosys-config,$(TARGETS))
 EXTRA_TARGETS += yosysjs-$(YOSYS_VER).zip
 
+ifeq ($(ENABLE_ABC),1)
+LINK_ABC := 1
+DISABLE_ABC_THREADS := 1
+endif
+
 viz.js:
 	wget -O viz.js.part https://github.com/mdaines/viz.js/releases/download/0.0.3/viz.js
 	mv viz.js.part viz.js

From 0abe7c6c77cdb4017cf5d8c34766e43806ce4876 Mon Sep 17 00:00:00 2001
From: Robert Ou <rqou@robertou.com>
Date: Tue, 14 Nov 2017 04:09:32 -0800
Subject: [PATCH 14/45] Modify emscripten main to mount nodefs and to run arg
 as a script

---
 kernel/driver.cc | 19 ++++++++++++++++++-
 1 file changed, 18 insertions(+), 1 deletion(-)

diff --git a/kernel/driver.cc b/kernel/driver.cc
index bec872c24..178641101 100644
--- a/kernel/driver.cc
+++ b/kernel/driver.cc
@@ -85,20 +85,37 @@ USING_YOSYS_NAMESPACE
 #ifdef EMSCRIPTEN
 #  include <sys/stat.h>
 #  include <sys/types.h>
+#  include <emscripten.h>
 
 extern "C" int main(int, char**);
 extern "C" void run(const char*);
 extern "C" const char *errmsg();
 extern "C" const char *prompt();
 
-int main(int, char**)
+int main(int argc, char **argv)
 {
+	EM_ASM(
+		if (ENVIRONMENT_IS_NODE)
+		{
+			FS.mkdir('/hostcwd');
+			FS.mount(NODEFS, { root: '.' }, '/hostcwd');
+			FS.mkdir('/hostfs');
+			FS.mount(NODEFS, { root: '/' }, '/hostfs');
+		}
+	);
+
 	mkdir("/work", 0777);
 	chdir("/work");
 	log_files.push_back(stdout);
 	log_error_stderr = true;
 	yosys_banner();
 	yosys_setup();
+
+	if (argc == 2)
+	{
+		// Run the first argument as a script file
+		run_frontend(argv[1], "script", 0, 0, 0);
+	}
 }
 
 void run(const char *command)

From bea71e71ca4f2b756519cd67ec99d24f1e70b53b Mon Sep 17 00:00:00 2001
From: Robert Ou <rqou@robertou.com>
Date: Fri, 18 May 2018 22:45:43 -0700
Subject: [PATCH 15/45] Force abc to align memory to 8 bytes

Apparently abc has a memory pool implementation that by default returns
memory that is unaligned. There is a workaround in the abc makefile that
uses uname to look for "arm" specifically and then sets the alignment.
However, ARM is not the only platform that requires proper alignment
(e.g. emscripten does too). For now, pessimistically force the alignment
for 8 bytes all the time (somehow 4 wasn't enough for fixing emscripten
despite being approximately a 32-bit platform).
---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 1a17bb857..ef838624a 100644
--- a/Makefile
+++ b/Makefile
@@ -164,7 +164,7 @@ else ifeq ($(CONFIG),emcc)
 CXX = emcc
 LD = emcc
 CXXFLAGS := -std=c++11 $(filter-out -fPIC -ggdb,$(CXXFLAGS))
-ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H"
+ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H -DABC_MEMALIGN=8"
 EMCCFLAGS := -Os -Wno-warn-absolute-paths
 EMCCFLAGS += --memory-init-file 0 --embed-file share -s NO_EXIT_RUNTIME=1
 EMCCFLAGS += -s EXPORTED_FUNCTIONS="['_main','_run','_prompt','_errmsg']"

From 4d645f0fce9e3af857cb292eca719c22141d379b Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 24 May 2018 17:07:06 +0200
Subject: [PATCH 16/45] Fix verific handling of anyconst/anyseq attributes

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verific.cc | 41 +++++++++++++++++++++++-------------
 frontends/verific/verific.h  |  3 ++-
 2 files changed, 28 insertions(+), 16 deletions(-)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 624c04be9..7ebcbca04 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -189,12 +189,12 @@ RTLIL::SigSpec VerificImporter::operatorInport(Instance *inst, const char *portn
 	}
 }
 
-RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst)
+RTLIL::SigSpec VerificImporter::operatorOutput(Instance *inst, const pool<Net*, hash_ptr_ops> *any_all_nets)
 {
 	RTLIL::SigSpec sig;
 	RTLIL::Wire *dummy_wire = NULL;
 	for (int i = int(inst->OutputSize())-1; i >= 0; i--)
-		if (inst->GetOutputBit(i)) {
+		if (inst->GetOutputBit(i) && (!any_all_nets || !any_all_nets->count(inst->GetOutputBit(i)))) {
 			sig.append(net_map_at(inst->GetOutputBit(i)));
 			dummy_wire = NULL;
 		} else {
@@ -394,6 +394,7 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
 	#define IN1 operatorInput1(inst)
 	#define IN2 operatorInput2(inst)
 	#define OUT operatorOutput(inst)
+	#define FILTERED_OUT operatorOutput(inst, &any_all_nets)
 	#define SIGNED inst->View()->IsSigned()
 
 	if (inst->Type() == OPER_ADDER) {
@@ -525,7 +526,7 @@ bool VerificImporter::import_netlist_instance_cells(Instance *inst, RTLIL::IdStr
 	}
 
 	if (inst->Type() == OPER_WIDE_BUF) {
-		module->addPos(inst_name, IN, OUT, SIGNED);
+		module->addPos(inst_name, IN, FILTERED_OUT, SIGNED);
 		return true;
 	}
 
@@ -791,6 +792,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 	dict<Net*, char, hash_ptr_ops> init_nets;
 	pool<Net*, hash_ptr_ops> anyconst_nets, anyseq_nets;
 	pool<Net*, hash_ptr_ops> allconst_nets, allseq_nets;
+	any_all_nets.clear();
 
 	FOREACH_NET_OF_NETLIST(nl, mi, net)
 	{
@@ -871,23 +873,30 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 		const char *allconst_attr = net->GetAttValue("allconst");
 		const char *allseq_attr = net->GetAttValue("allseq");
 
-		if (rand_const_attr != nullptr && (!strcmp(rand_const_attr, "1") || !strcmp(rand_const_attr, "'1'")))
+		if (rand_const_attr != nullptr && (!strcmp(rand_const_attr, "1") || !strcmp(rand_const_attr, "'1'"))) {
 			anyconst_nets.insert(net);
-
-		else if (rand_attr != nullptr && (!strcmp(rand_attr, "1") || !strcmp(rand_attr, "'1'")))
+			any_all_nets.insert(net);
+		}
+		else if (rand_attr != nullptr && (!strcmp(rand_attr, "1") || !strcmp(rand_attr, "'1'"))) {
 			anyseq_nets.insert(net);
-
-		else if (anyconst_attr != nullptr && (!strcmp(anyconst_attr, "1") || !strcmp(anyconst_attr, "'1'")))
+			any_all_nets.insert(net);
+		}
+		else if (anyconst_attr != nullptr && (!strcmp(anyconst_attr, "1") || !strcmp(anyconst_attr, "'1'"))) {
 			anyconst_nets.insert(net);
-
-		else if (anyseq_attr != nullptr && (!strcmp(anyseq_attr, "1") || !strcmp(anyseq_attr, "'1'")))
+			any_all_nets.insert(net);
+		}
+		else if (anyseq_attr != nullptr && (!strcmp(anyseq_attr, "1") || !strcmp(anyseq_attr, "'1'"))) {
 			anyseq_nets.insert(net);
-
-		else if (allconst_attr != nullptr && (!strcmp(allconst_attr, "1") || !strcmp(allconst_attr, "'1'")))
+			any_all_nets.insert(net);
+		}
+		else if (allconst_attr != nullptr && (!strcmp(allconst_attr, "1") || !strcmp(allconst_attr, "'1'"))) {
 			allconst_nets.insert(net);
-
-		else if (allseq_attr != nullptr && (!strcmp(allseq_attr, "1") || !strcmp(allseq_attr, "'1'")))
+			any_all_nets.insert(net);
+		}
+		else if (allseq_attr != nullptr && (!strcmp(allseq_attr, "1") || !strcmp(allseq_attr, "'1'"))) {
 			allseq_nets.insert(net);
+			any_all_nets.insert(net);
+		}
 
 		if (net_map.count(net)) {
 			if (verific_verbose)
@@ -1064,7 +1073,9 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 		}
 
 		if (inst->Type() == PRIM_BUF) {
-			module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+			auto outnet = inst->GetOutput();
+			if (!anyconst_nets.count(outnet) && !anyseq_nets.count(outnet) && !allconst_nets.count(outnet) && !allseq_nets.count(outnet))
+				module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet));
 			continue;
 		}
 
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 2dd688e0d..714b7c82a 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -65,6 +65,7 @@ struct VerificImporter
 
 	std::map<Verific::Net*, RTLIL::SigBit> net_map;
 	std::map<Verific::Net*, Verific::Net*> sva_posedge_map;
+	pool<Verific::Net*, hash_ptr_ops> any_all_nets;
 
 	bool mode_gates, mode_keep, mode_nosva, mode_names, mode_verific;
 	bool mode_autocover;
@@ -79,7 +80,7 @@ struct VerificImporter
 	RTLIL::SigSpec operatorInput1(Verific::Instance *inst);
 	RTLIL::SigSpec operatorInput2(Verific::Instance *inst);
 	RTLIL::SigSpec operatorInport(Verific::Instance *inst, const char *portname);
-	RTLIL::SigSpec operatorOutput(Verific::Instance *inst);
+	RTLIL::SigSpec operatorOutput(Verific::Instance *inst, const pool<Verific::Net*, hash_ptr_ops> *any_all_nets = nullptr);
 
 	bool import_netlist_instance_gates(Verific::Instance *inst, RTLIL::IdString inst_name);
 	bool import_netlist_instance_cells(Verific::Instance *inst, RTLIL::IdString inst_name);

From 251562a4918576bd485bcdcc908c0ac780689a77 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 24 May 2018 18:13:38 +0200
Subject: [PATCH 17/45] Fix VerificClocking for cases where Verific generates
 chains of PRIM_SVA_POSEDGE

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verific.cc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 7ebcbca04..19273c69a 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1393,7 +1393,7 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a
 			return;
 	}
 
-	if (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
+	while (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
 	{
 		net = inst->GetInput();
 		inst = net->Driver();;

From 001c9f1d45749535452d082a7c92a17954b603b8 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 25 May 2018 15:41:45 +0200
Subject: [PATCH 18/45] Fix Verific handling of single-bit anyseq/anyconst
 wires

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verific.cc | 6 ++++--
 1 file changed, 4 insertions(+), 2 deletions(-)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 19273c69a..60fa6db3b 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -244,7 +244,9 @@ bool VerificImporter::import_netlist_instance_gates(Instance *inst, RTLIL::IdStr
 	}
 
 	if (inst->Type() == PRIM_BUF) {
-		module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(inst->GetOutput()));
+		auto outnet = inst->GetOutput();
+		if (!any_all_nets.count(outnet))
+			module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet));
 		return true;
 	}
 
@@ -1074,7 +1076,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se
 
 		if (inst->Type() == PRIM_BUF) {
 			auto outnet = inst->GetOutput();
-			if (!anyconst_nets.count(outnet) && !anyseq_nets.count(outnet) && !allconst_nets.count(outnet) && !allseq_nets.count(outnet))
+			if (!any_all_nets.count(outnet))
 				module->addBufGate(inst_name, net_map_at(inst->GetInput()), net_map_at(outnet));
 			continue;
 		}

From 9a946c207fd4f5e18ce464e39d7d180c29ce5c23 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 28 May 2018 13:36:35 +0200
Subject: [PATCH 19/45] Add comment to VIPER #13453 work-around

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verific.cc | 1 +
 1 file changed, 1 insertion(+)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 60fa6db3b..12f2fdd7f 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1395,6 +1395,7 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a
 			return;
 	}
 
+	// Use while() instead of if() to work around VIPER #13453
 	while (inst != nullptr && inst->Type() == PRIM_SVA_POSEDGE)
 	{
 		net = inst->GetInput();

From 74efafc1cfd94949cc368b3ac5fa1476ce950f03 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 28 May 2018 16:42:06 +0200
Subject: [PATCH 20/45] Add some cleanup code to memory_nordff

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 passes/memory/memory_nordff.cc | 66 +++++++++++++++++++---------------
 1 file changed, 38 insertions(+), 28 deletions(-)

diff --git a/passes/memory/memory_nordff.cc b/passes/memory/memory_nordff.cc
index 5f87e8b79..87ab7c623 100644
--- a/passes/memory/memory_nordff.cc
+++ b/passes/memory/memory_nordff.cc
@@ -61,49 +61,59 @@ struct MemoryNordffPass : public Pass {
 
 			SigSpec rd_addr = cell->getPort("\\RD_ADDR");
 			SigSpec rd_data = cell->getPort("\\RD_DATA");
+			SigSpec rd_clk = cell->getPort("\\RD_CLK");
+			SigSpec rd_en = cell->getPort("\\RD_EN");
 			Const rd_clk_enable = cell->getParam("\\RD_CLK_ENABLE");
+			Const rd_clk_polarity = cell->getParam("\\RD_CLK_POLARITY");
 
 			for (int i = 0; i < rd_ports; i++)
 			{
 				bool clk_enable = rd_clk_enable[i] == State::S1;
 
-				if (!clk_enable)
-					continue;
-
-				bool clk_polarity = cell->getParam("\\RD_CLK_POLARITY")[i] == State::S1;
-				bool transparent = cell->getParam("\\RD_TRANSPARENT")[i] == State::S1;
-
-				SigSpec clk = cell->getPort("\\RD_CLK")[i] ;
-				SigSpec en = cell->getPort("\\RD_EN")[i];
-				Cell *c;
-
-				if (transparent)
+				if (clk_enable)
 				{
-					SigSpec sig_q = module->addWire(NEW_ID, abits);
-					SigSpec sig_d = rd_addr.extract(abits * i, abits);
-					rd_addr.replace(abits * i, sig_q);
-					if (en != State::S1)
-						sig_d = module->Mux(NEW_ID, sig_q, sig_d, en);
-					c = module->addDff(NEW_ID, clk, sig_d, sig_q, clk_polarity);
-				}
-				else
-				{
-					SigSpec sig_d = module->addWire(NEW_ID, width);
-					SigSpec sig_q = rd_data.extract(width * i, width);
-					rd_data.replace(width *i, sig_d);
-					if (en != State::S1)
-						sig_d = module->Mux(NEW_ID, sig_q, sig_d, en);
-					c = module->addDff(NEW_ID, clk, sig_d, sig_q, clk_polarity);
+					bool clk_polarity = cell->getParam("\\RD_CLK_POLARITY")[i] == State::S1;
+					bool transparent = cell->getParam("\\RD_TRANSPARENT")[i] == State::S1;
+
+					SigSpec clk = cell->getPort("\\RD_CLK")[i] ;
+					SigSpec en = cell->getPort("\\RD_EN")[i];
+					Cell *c;
+
+					if (transparent)
+					{
+						SigSpec sig_q = module->addWire(NEW_ID, abits);
+						SigSpec sig_d = rd_addr.extract(abits * i, abits);
+						rd_addr.replace(abits * i, sig_q);
+						if (en != State::S1)
+							sig_d = module->Mux(NEW_ID, sig_q, sig_d, en);
+						c = module->addDff(NEW_ID, clk, sig_d, sig_q, clk_polarity);
+					}
+					else
+					{
+						SigSpec sig_d = module->addWire(NEW_ID, width);
+						SigSpec sig_q = rd_data.extract(width * i, width);
+						rd_data.replace(width *i, sig_d);
+						if (en != State::S1)
+							sig_d = module->Mux(NEW_ID, sig_q, sig_d, en);
+						c = module->addDff(NEW_ID, clk, sig_d, sig_q, clk_polarity);
+					}
+
+					log("Extracted %s FF from read port %d of %s.%s: %s\n", transparent ? "addr" : "data",
+							i, log_id(module), log_id(cell), log_id(c));
 				}
 
-				log("Extracted %s FF from read port %d of %s.%s: %s\n", transparent ? "addr" : "data",
-						i, log_id(module), log_id(cell), log_id(c));
+				rd_en[i] = State::S1;
+				rd_clk[i] = State::S0;
 				rd_clk_enable[i] = State::S0;
+				rd_clk_polarity[i] = State::S1;
 			}
 
 			cell->setPort("\\RD_ADDR", rd_addr);
 			cell->setPort("\\RD_DATA", rd_data);
+			cell->setPort("\\RD_CLK", rd_clk);
+			cell->setPort("\\RD_EN", rd_en);
 			cell->setParam("\\RD_CLK_ENABLE", rd_clk_enable);
+			cell->setParam("\\RD_CLK_POLARITY", rd_clk_polarity);
 		}
 	}
 } MemoryNordffPass;

From cee4b1e6bc11fff1d2d97985a96e6990afc57950 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 28 May 2018 17:16:15 +0200
Subject: [PATCH 21/45] Disable memory_dff for initialized FFs

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 passes/memory/memory_dff.cc | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/passes/memory/memory_dff.cc b/passes/memory/memory_dff.cc
index 40691d160..6e036397d 100644
--- a/passes/memory/memory_dff.cc
+++ b/passes/memory/memory_dff.cc
@@ -33,8 +33,20 @@ struct MemoryDffWorker
 	dict<SigBit, int> sigbit_users_count;
 	dict<SigSpec, Cell*> mux_cells_a, mux_cells_b;
 	pool<Cell*> forward_merged_dffs, candidate_dffs;
+	pool<SigBit> init_bits;
 
-	MemoryDffWorker(Module *module) : module(module), sigmap(module) { }
+	MemoryDffWorker(Module *module) : module(module), sigmap(module)
+	{
+		for (auto wire : module->wires()) {
+			if (wire->attributes.count("\\init") == 0)
+				continue;
+			SigSpec sig = sigmap(wire);
+			Const initval = wire->attributes.count("\\init");
+			for (int i = 0; i < GetSize(sig) && i < GetSize(initval); i++)
+				if (initval[i] == State::S0 || initval[i] == State::S1)
+					init_bits.insert(sig[i]);
+		}
+	}
 
 	bool find_sig_before_dff(RTLIL::SigSpec &sig, RTLIL::SigSpec &clk, bool &clk_polarity, bool after = false)
 	{
@@ -45,6 +57,9 @@ struct MemoryDffWorker
 			if (bit.wire == NULL)
 				continue;
 
+			if (!after && init_bits.count(sigmap(bit)))
+				return false;
+
 			for (auto cell : dff_cells)
 			{
 				if (after && forward_merged_dffs.count(cell))
@@ -72,6 +87,9 @@ struct MemoryDffWorker
 				if (d.size() != 1)
 					continue;
 
+				if (after && init_bits.count(d))
+					return false;
+
 				bit = d;
 				clk = this_clk;
 				clk_polarity = this_clk_polarity;

From a77e27ab1579ed0f89bff898d0a0ea7ae0c13701 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 30 May 2018 13:04:40 +0200
Subject: [PATCH 22/45] Update ABC to git rev 6df1396

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index ef838624a..2db6612a7 100644
--- a/Makefile
+++ b/Makefile
@@ -106,7 +106,7 @@ OBJS = kernel/version_$(GIT_REV).o
 # is just a symlink to your actual ABC working directory, as 'make mrproper'
 # will remove the 'abc' directory and you do not want to accidentally
 # delete your work on ABC..
-ABCREV = f23ea8e
+ABCREV = 6df1396
 ABCPULL = 1
 ABCURL ?= https://github.com/berkeley-abc/abc
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1

From 7fecc3c199e6cfe4b474431d54027d699bc8d343 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 30 May 2018 13:17:09 +0200
Subject: [PATCH 23/45] Make -nordff the default in "prep"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 techlibs/common/prep.cc | 22 +++++++++++++---------
 1 file changed, 13 insertions(+), 9 deletions(-)

diff --git a/techlibs/common/prep.cc b/techlibs/common/prep.cc
index 3dfc60383..cc977f97e 100644
--- a/techlibs/common/prep.cc
+++ b/techlibs/common/prep.cc
@@ -55,13 +55,14 @@ struct PrepPass : public ScriptPass
 		log("\n");
 		log("    -memx\n");
 		log("        simulate verilog simulation behavior for out-of-bounds memory accesses\n");
-		log("        using the 'memory_memx' pass. This option implies -nordff.\n");
+		log("        using the 'memory_memx' pass.\n");
 		log("\n");
 		log("    -nomem\n");
 		log("        do not run any of the memory_* passes\n");
 		log("\n");
-		log("    -nordff\n");
-		log("        passed to 'memory_dff'. prohibits merging of FFs into memory read ports\n");
+		log("    -rdff\n");
+		log("        do not pass -nordff to 'memory_dff'. This enables merging of FFs into\n");
+		log("        memory read ports.\n");
 		log("\n");
 		log("    -nokeepdc\n");
 		log("        do not call opt_* with -keepdc\n");
@@ -77,13 +78,12 @@ struct PrepPass : public ScriptPass
 		log("\n");
 	}
 
-	string top_module, fsm_opts, memory_opts;
-	bool autotop, flatten, ifxmode, memxmode, nomemmode, nokeepdc;
+	string top_module, fsm_opts;
+	bool autotop, flatten, ifxmode, memxmode, nomemmode, nokeepdc, nordff;
 
 	virtual void clear_flags() YS_OVERRIDE
 	{
 		top_module.clear();
-		memory_opts.clear();
 
 		autotop = false;
 		flatten = false;
@@ -91,6 +91,7 @@ struct PrepPass : public ScriptPass
 		memxmode = false;
 		nomemmode = false;
 		nokeepdc = false;
+		nordff = true;
 	}
 
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design) YS_OVERRIDE
@@ -129,7 +130,6 @@ struct PrepPass : public ScriptPass
 			}
 			if (args[argidx] == "-memx") {
 				memxmode = true;
-				memory_opts += " -nordff";
 				continue;
 			}
 			if (args[argidx] == "-nomem") {
@@ -137,7 +137,11 @@ struct PrepPass : public ScriptPass
 				continue;
 			}
 			if (args[argidx] == "-nordff") {
-				memory_opts += " -nordff";
+				nordff = true;
+				continue;
+			}
+			if (args[argidx] == "-rdff") {
+				nordff = false;
 				continue;
 			}
 			if (args[argidx] == "-nokeepdc") {
@@ -196,7 +200,7 @@ struct PrepPass : public ScriptPass
 					run(memxmode ? "wreduce -memx" : "wreduce");
 			}
 			if (!nomemmode) {
-				run("memory_dff" + (help_mode ? " [-nordff]" : memory_opts));
+				run(string("memory_dff") + (help_mode ? " [-nordff]" : nordff ? " -nordff" : ""));
 				if (help_mode || memxmode)
 					run("memory_memx", "(if -memx)");
 				run("opt_clean");

From 7f0548c16f64bd0c4e3bd85744cfdcf9494b4829 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 30 May 2018 14:17:36 +0200
Subject: [PATCH 24/45] Update examples/cmos/counter.ys to use "synth" command

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 examples/cmos/counter.ys | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

diff --git a/examples/cmos/counter.ys b/examples/cmos/counter.ys
index a784f3465..d0b093667 100644
--- a/examples/cmos/counter.ys
+++ b/examples/cmos/counter.ys
@@ -1,11 +1,12 @@
-
 read_verilog counter.v
 read_verilog -lib cmos_cells.v
 
-proc;; memory;; techmap;;
-
+synth
 dfflibmap -liberty cmos_cells.lib
-abc -liberty cmos_cells.lib;;
+abc -liberty cmos_cells.lib
+opt_clean
+
+stat -liberty cmos_cells.lib
 
 # http://vlsiarch.ecen.okstate.edu/flows/MOSIS_SCMOS/latest/cadence/lib/tsmc025/signalstorm/osu025_stdcells.lib
 # dfflibmap -liberty osu025_stdcells.lib
@@ -13,4 +14,3 @@ abc -liberty cmos_cells.lib;;
 
 write_verilog synth.v
 write_spice synth.sp
-

From 3ab79a231b1b31f1177df2c1351643eda4e9553b Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 31 May 2018 18:09:31 +0200
Subject: [PATCH 25/45] Bugfix in handling of array instances with empty ports

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 passes/hierarchy/hierarchy.cc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index 18dfa7184..bfb8e7f95 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -258,7 +258,7 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
 			if (mod->wires_.count(portname) == 0)
 				log_error("Array cell `%s.%s' connects to unknown port `%s'.\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(cell->name), RTLIL::id2cstr(conn.first));
 			int port_size = mod->wires_.at(portname)->width;
-			if (conn_size == port_size)
+			if (conn_size == port_size || conn_size == 0)
 				continue;
 			if (conn_size != port_size*num)
 				log_error("Array cell `%s.%s' has invalid port vs. signal size for port `%s'.\n", RTLIL::id2cstr(module->name), RTLIL::id2cstr(cell->name), RTLIL::id2cstr(conn.first));

From 4cd6d5556ade3a6da64d3639e6b6e547222820e8 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 1 Jun 2018 11:49:58 +0200
Subject: [PATCH 26/45] Add "setundef -anyconst"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 passes/cmds/setundef.cc | 61 +++++++++++++++++++++++++++--------------
 1 file changed, 41 insertions(+), 20 deletions(-)

diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc
index c11ddbdc1..be26c3fd4 100644
--- a/passes/cmds/setundef.cc
+++ b/passes/cmds/setundef.cc
@@ -23,6 +23,13 @@
 #include "kernel/rtlil.h"
 #include "kernel/log.h"
 
+#define MODE_ZERO     0
+#define MODE_ONE      1
+#define MODE_UNDEF    2
+#define MODE_RANDOM   3
+#define MODE_ANYSEQ   4
+#define MODE_ANYCONST 5
+
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
@@ -34,30 +41,32 @@ struct SetundefWorker
 
 	RTLIL::State next_bit()
 	{
-		if (next_bit_mode == 0)
+		if (next_bit_mode == MODE_ZERO)
 			return RTLIL::State::S0;
 
-		if (next_bit_mode == 1)
+		if (next_bit_mode == MODE_ONE)
 			return RTLIL::State::S1;
 
-		if (next_bit_mode == 2)
-			log_abort();
-
-		if (next_bit_mode == 4)
+		if (next_bit_mode == MODE_UNDEF)
 			return RTLIL::State::Sx;
 
-		// xorshift32
-		next_bit_state ^= next_bit_state << 13;
-		next_bit_state ^= next_bit_state >> 17;
-		next_bit_state ^= next_bit_state << 5;
-		log_assert(next_bit_state != 0);
+		if (next_bit_mode == MODE_RANDOM)
+		{
+			// xorshift32
+			next_bit_state ^= next_bit_state << 13;
+			next_bit_state ^= next_bit_state >> 17;
+			next_bit_state ^= next_bit_state << 5;
+			log_assert(next_bit_state != 0);
 
-		return ((next_bit_state >> (next_bit_state & 15)) & 16) ? RTLIL::State::S0 : RTLIL::State::S1;
+			return ((next_bit_state >> (next_bit_state & 15)) & 16) ? RTLIL::State::S0 : RTLIL::State::S1;
+		}
+
+		log_abort();
 	}
 
 	void operator()(RTLIL::SigSpec &sig)
 	{
-		if (next_bit_mode == 2) {
+		if (next_bit_mode == MODE_ANYSEQ || next_bit_mode == MODE_ANYCONST) {
 			siglist.push_back(&sig);
 			return;
 		}
@@ -93,6 +102,9 @@ struct SetundefPass : public Pass {
 		log("    -anyseq\n");
 		log("        replace with $anyseq drivers (for formal)\n");
 		log("\n");
+		log("    -anyconst\n");
+		log("        replace with $anyconst drivers (for formal)\n");
+		log("\n");
 		log("    -random <seed>\n");
 		log("        replace with random bits using the specified integer als seed\n");
 		log("        value for the random number generator.\n");
@@ -119,25 +131,31 @@ struct SetundefPass : public Pass {
 			}
 			if (args[argidx] == "-zero") {
 				got_value = true;
-				worker.next_bit_mode = 0;
+				worker.next_bit_mode = MODE_ZERO;
 				worker.next_bit_state = 0;
 				continue;
 			}
 			if (args[argidx] == "-one") {
 				got_value = true;
-				worker.next_bit_mode = 1;
+				worker.next_bit_mode = MODE_ONE;
 				worker.next_bit_state = 0;
 				continue;
 			}
 			if (args[argidx] == "-anyseq") {
 				got_value = true;
-				worker.next_bit_mode = 2;
+				worker.next_bit_mode = MODE_ANYSEQ;
+				worker.next_bit_state = 0;
+				continue;
+			}
+			if (args[argidx] == "-anyconst") {
+				got_value = true;
+				worker.next_bit_mode = MODE_ANYCONST;
 				worker.next_bit_state = 0;
 				continue;
 			}
 			if (args[argidx] == "-undef") {
 				got_value = true;
-				worker.next_bit_mode = 4;
+				worker.next_bit_mode = MODE_UNDEF;
 				worker.next_bit_state = 0;
 				continue;
 			}
@@ -147,7 +165,7 @@ struct SetundefPass : public Pass {
 			}
 			if (args[argidx] == "-random" && !got_value && argidx+1 < args.size()) {
 				got_value = true;
-				worker.next_bit_mode = 3;
+				worker.next_bit_mode = MODE_RANDOM;
 				worker.next_bit_state = atoi(args[++argidx].c_str()) + 1;
 				for (int i = 0; i < 10; i++)
 					worker.next_bit();
@@ -274,7 +292,7 @@ struct SetundefPass : public Pass {
 
 			module->rewrite_sigspecs(worker);
 
-			if (worker.next_bit_mode == 2)
+			if (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST)
 			{
 				vector<SigSpec*> siglist;
 				siglist.swap(worker.siglist);
@@ -291,7 +309,10 @@ struct SetundefPass : public Pass {
 							width++;
 
 						if (width > 0) {
-							sig.replace(cursor, module->Anyseq(NEW_ID, width));
+							if (worker.next_bit_mode == MODE_ANYSEQ)
+								sig.replace(cursor, module->Anyseq(NEW_ID, width));
+							else
+								sig.replace(cursor, module->Anyconst(NEW_ID, width));
 							cursor += width;
 						} else {
 							cursor++;

From f273291dfe5de460192ef2a63a121b3c2e8b9a62 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 1 Jun 2018 11:57:28 +0200
Subject: [PATCH 27/45] Add setundef -anyseq / -anyconst support to -undriven
 mode

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 passes/cmds/setundef.cc | 14 +++++++++++---
 1 file changed, 11 insertions(+), 3 deletions(-)

diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc
index be26c3fd4..3a3ebedf1 100644
--- a/passes/cmds/setundef.cc
+++ b/passes/cmds/setundef.cc
@@ -176,7 +176,10 @@ struct SetundefPass : public Pass {
 		extra_args(args, argidx, design);
 
 		if (!got_value)
-			log_cmd_error("One of the options -zero, -one, -anyseq, or -random <seed> must be specified.\n");
+			log_cmd_error("One of the options -zero, -one, -anyseq, -anyconst, or -random <seed> must be specified.\n");
+
+		if (init_mode && (worker.next_bit_mode == MODE_ANYSEQ || worker.next_bit_mode == MODE_ANYCONST))
+			log_cmd_error("The options -init and -anyseq / -anyconst are exclusive.\n");
 
 		for (auto module : design->selected_modules())
 		{
@@ -204,8 +207,13 @@ struct SetundefPass : public Pass {
 				RTLIL::SigSpec sig = undriven_signals.export_all();
 				for (auto &c : sig.chunks()) {
 					RTLIL::SigSpec bits;
-					for (int i = 0; i < c.width; i++)
-						bits.append(worker.next_bit());
+					if (worker.next_bit_mode == MODE_ANYSEQ)
+						bits = module->Anyseq(NEW_ID, c.width);
+					else if (worker.next_bit_mode == MODE_ANYCONST)
+						bits = module->Anyconst(NEW_ID, c.width);
+					else
+						for (int i = 0; i < c.width; i++)
+							bits.append(worker.next_bit());
 					module->connect(RTLIL::SigSig(c, bits));
 				}
 			}

From 4372cf690d829755279a6a5778023e5e0a4493b2 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 1 Jun 2018 13:25:42 +0200
Subject: [PATCH 28/45] Add (* gclk *) attribute support

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 README.md                    |  4 +++-
 frontends/ast/genrtlil.cc    |  9 +++++++++
 frontends/verific/verific.cc | 10 ++++++++++
 frontends/verific/verific.h  |  1 +
 4 files changed, 23 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index 704948e2d..c02691d94 100644
--- a/README.md
+++ b/README.md
@@ -418,7 +418,9 @@ Non-standard or SystemVerilog features for formal verification
   supported in any clocked block.
 
 - The syntax ``@($global_clock)`` can be used to create FFs that have no
-  explicit clock input ($ff cells).
+  explicit clock input ($ff cells). The same can be achieved by using
+  ``@(posedge <netname>)`` or ``@(negedge <netname>)`` when ``<netname>``
+  is marked with the ``(* gclk *)`` Verilog attribute.
 
 
 Supported features from SystemVerilog
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 57ba9668d..40cbbc2a3 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -223,12 +223,18 @@ struct AST_INTERNAL::ProcessGenerator
 		bool found_global_syncs = false;
 		bool found_anyedge_syncs = false;
 		for (auto child : always->children)
+		{
+			if ((child->type == AST_POSEDGE || child->type == AST_NEGEDGE) && GetSize(child->children) == 1 && child->children.at(0)->type == AST_IDENTIFIER &&
+					child->children.at(0)->id2ast && child->children.at(0)->id2ast->type == AST_WIRE && child->children.at(0)->id2ast->get_bool_attribute("\\gclk")) {
+				found_global_syncs = true;
+			}
 			if (child->type == AST_EDGE) {
 				if (GetSize(child->children) == 1 && child->children.at(0)->type == AST_IDENTIFIER && child->children.at(0)->str == "\\$global_clock")
 					found_global_syncs = true;
 				else
 					found_anyedge_syncs = true;
 			}
+		}
 
 		if (found_anyedge_syncs) {
 			if (found_global_syncs)
@@ -242,6 +248,9 @@ struct AST_INTERNAL::ProcessGenerator
 		bool found_clocked_sync = false;
 		for (auto child : always->children)
 			if (child->type == AST_POSEDGE || child->type == AST_NEGEDGE) {
+				if (GetSize(child->children) == 1 && child->children.at(0)->type == AST_IDENTIFIER && child->children.at(0)->id2ast &&
+						child->children.at(0)->id2ast->type == AST_WIRE && child->children.at(0)->id2ast->get_bool_attribute("\\gclk"))
+					continue;
 				found_clocked_sync = true;
 				if (found_global_syncs || found_anyedge_syncs)
 					log_error("Found non-synthesizable event list at %s:%d!\n", always->filename.c_str(), always->linenum);
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 12f2fdd7f..f67337754 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1470,6 +1470,10 @@ VerificClocking::VerificClocking(VerificImporter *importer, Net *net, bool sva_a
 
 	clock_net = net;
 	clock_sig = importer->net_map_at(clock_net);
+
+	const char *gclk_attr = clock_net->GetAttValue("gclk");
+	if (gclk_attr != nullptr && (!strcmp(gclk_attr, "1") || !strcmp(gclk_attr, "'1'")))
+		gclk = true;
 }
 
 Cell *VerificClocking::addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const init_value)
@@ -1492,15 +1496,20 @@ Cell *VerificClocking::addDff(IdString name, SigSpec sig_d, SigSpec sig_q, Const
 		sig_d = module->Mux(NEW_ID, sig_q, sig_d, enable_sig);
 
 	if (disable_sig != State::S0) {
+		log_assert(gclk == false);
 		log_assert(GetSize(sig_q) == GetSize(init_value));
 		return module->addAdff(name, clock_sig, disable_sig, sig_d, sig_q, init_value, posedge);
 	}
 
+	if (gclk)
+		return module->addFf(name, sig_d, sig_q);
+
 	return module->addDff(name, clock_sig, sig_d, sig_q, posedge);
 }
 
 Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec sig_d, SigSpec sig_q, Const arst_value)
 {
+	log_assert(gclk == false);
 	log_assert(disable_sig == State::S0);
 
 	if (enable_sig != State::S1)
@@ -1511,6 +1520,7 @@ Cell *VerificClocking::addAdff(IdString name, RTLIL::SigSpec sig_arst, SigSpec s
 
 Cell *VerificClocking::addDffsr(IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, SigSpec sig_d, SigSpec sig_q)
 {
+	log_assert(gclk == false);
 	log_assert(disable_sig == State::S0);
 
 	if (enable_sig != State::S1)
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 714b7c82a..86a743ea1 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -40,6 +40,7 @@ struct VerificClocking {
 	SigBit enable_sig = State::S1;
 	SigBit disable_sig = State::S0;
 	bool posedge = true;
+	bool gclk = false;
 
 	VerificClocking() { }
 	VerificClocking(VerificImporter *importer, Verific::Net *net, bool sva_at_only = false);

From 106af19b69c1a62531655d35f5a8f3f7eda838e7 Mon Sep 17 00:00:00 2001
From: Udi Finkelstein <github@udifink.com>
Date: Tue, 5 Jun 2018 17:52:36 +0300
Subject: [PATCH 29/45] Fixed typo (sikp -> skip)

---
 tests/tools/autotest.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/tools/autotest.sh b/tests/tools/autotest.sh
index 31a6ae8ab..d6216244f 100755
--- a/tests/tools/autotest.sh
+++ b/tests/tools/autotest.sh
@@ -100,7 +100,7 @@ do
 		echo -n "Test: $bn "
 	fi
 
-	rm -f ${bn}.{err,log,sikp}
+	rm -f ${bn}.{err,log,skip}
 	mkdir -p ${bn}.out
 	rm -rf ${bn}.out/*
 

From 83631555dd5d57e2a3d3b7175f77baf0ad67ccd9 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 11 Jun 2018 18:10:12 +0200
Subject: [PATCH 30/45] Fix ice40_opt for cases where a port is connected to a
 signal with width != 1

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 techlibs/ice40/ice40_opt.cc | 34 +++++++++++++++++++++++++---------
 1 file changed, 25 insertions(+), 9 deletions(-)

diff --git a/techlibs/ice40/ice40_opt.cc b/techlibs/ice40/ice40_opt.cc
index ae72f5d64..7af60f297 100644
--- a/techlibs/ice40/ice40_opt.cc
+++ b/techlibs/ice40/ice40_opt.cc
@@ -26,6 +26,13 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+static SigBit get_bit_or_zero(const SigSpec &sig)
+{
+	if (GetSize(sig) == 0)
+		return State::S0;
+	return sig[0];
+}
+
 static void run_ice40_opts(Module *module, bool unlut_mode)
 {
 	pool<SigBit> optimized_co;
@@ -45,7 +52,11 @@ static void run_ice40_opts(Module *module, bool unlut_mode)
 			SigSpec non_const_inputs, replacement_output;
 			int count_zeros = 0, count_ones = 0;
 
-			SigBit inbit[3] = {cell->getPort("\\I0"), cell->getPort("\\I1"), cell->getPort("\\CI")};
+			SigBit inbit[3] = {
+				get_bit_or_zero(cell->getPort("\\I0")),
+				get_bit_or_zero(cell->getPort("\\I1")),
+				get_bit_or_zero(cell->getPort("\\CI"))
+			};
 			for (int i = 0; i < 3; i++)
 				if (inbit[i].wire == nullptr) {
 					if (inbit[i] == State::S1)
@@ -63,8 +74,8 @@ static void run_ice40_opts(Module *module, bool unlut_mode)
 				replacement_output = non_const_inputs;
 
 			if (GetSize(replacement_output)) {
-				optimized_co.insert(sigmap(cell->getPort("\\CO")));
-				module->connect(cell->getPort("\\CO"), replacement_output);
+				optimized_co.insert(sigmap(cell->getPort("\\CO")[0]));
+				module->connect(cell->getPort("\\CO")[0], replacement_output);
 				module->design->scratchpad_set_bool("opt.did_something", true);
 				log("Optimized away SB_CARRY cell %s.%s: CO=%s\n",
 						log_id(module), log_id(cell), log_signal(replacement_output));
@@ -78,10 +89,10 @@ static void run_ice40_opts(Module *module, bool unlut_mode)
 	{
 		SigSpec inbits;
 
-		inbits.append(cell->getPort("\\I0"));
-		inbits.append(cell->getPort("\\I1"));
-		inbits.append(cell->getPort("\\I2"));
-		inbits.append(cell->getPort("\\I3"));
+		inbits.append(get_bit_or_zero(cell->getPort("\\I0")));
+		inbits.append(get_bit_or_zero(cell->getPort("\\I1")));
+		inbits.append(get_bit_or_zero(cell->getPort("\\I2")));
+		inbits.append(get_bit_or_zero(cell->getPort("\\I3")));
 		sigmap.apply(inbits);
 
 		if (unlut_mode)
@@ -104,8 +115,13 @@ static void run_ice40_opts(Module *module, bool unlut_mode)
 		cell->setParam("\\LUT", cell->getParam("\\LUT_INIT"));
 		cell->unsetParam("\\LUT_INIT");
 
-		cell->setPort("\\A", SigSpec({cell->getPort("\\I3"), cell->getPort("\\I2"), cell->getPort("\\I1"), cell->getPort("\\I0")}));
-		cell->setPort("\\Y", cell->getPort("\\O"));
+		cell->setPort("\\A", SigSpec({
+			get_bit_or_zero(cell->getPort("\\I3")),
+			get_bit_or_zero(cell->getPort("\\I2")),
+			get_bit_or_zero(cell->getPort("\\I1")),
+			get_bit_or_zero(cell->getPort("\\I0"))
+		}));
+		cell->setPort("\\Y", cell->getPort("\\O")[0]);
 		cell->unsetPort("\\I0");
 		cell->unsetPort("\\I1");
 		cell->unsetPort("\\I2");

From 57fc8dd58229d309ba56b374223802936444ecd4 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 13 Jun 2018 13:35:10 +0200
Subject: [PATCH 31/45] Add "synth_ice40 -json"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 techlibs/ice40/synth_ice40.cc | 31 ++++++++++++++++++++++---------
 1 file changed, 22 insertions(+), 9 deletions(-)

diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc
index 177581d53..abd890a56 100644
--- a/techlibs/ice40/synth_ice40.cc
+++ b/techlibs/ice40/synth_ice40.cc
@@ -45,7 +45,11 @@ struct SynthIce40Pass : public ScriptPass
 		log("        is omitted if this parameter is not specified.\n");
 		log("\n");
 		log("    -edif <file>\n");
-		log("        write the design to the specified edif file. writing of an output file\n");
+		log("        write the design to the specified EDIF file. writing of an output file\n");
+		log("        is omitted if this parameter is not specified.\n");
+		log("\n");
+		log("    -json <file>\n");
+		log("        write the design to the specified JSON file. writing of an output file\n");
 		log("        is omitted if this parameter is not specified.\n");
 		log("\n");
 		log("    -run <from_label>:<to_label>\n");
@@ -81,7 +85,7 @@ struct SynthIce40Pass : public ScriptPass
 		log("\n");
 	}
 
-	string top_opt, blif_file, edif_file;
+	string top_opt, blif_file, edif_file, json_file;
 	bool nocarry, nodffe, nobram, flatten, retime, abc2, vpr;
 
 	virtual void clear_flags() YS_OVERRIDE
@@ -89,6 +93,7 @@ struct SynthIce40Pass : public ScriptPass
 		top_opt = "-auto-top";
 		blif_file = "";
 		edif_file = "";
+		json_file = "";
 		nocarry = false;
 		nodffe = false;
 		nobram = false;
@@ -118,6 +123,10 @@ struct SynthIce40Pass : public ScriptPass
 				edif_file = args[++argidx];
 				continue;
 			}
+			if (args[argidx] == "-json" && argidx+1 < args.size()) {
+				json_file = args[++argidx];
+				continue;
+			}
 			if (args[argidx] == "-run" && argidx+1 < args.size()) {
 				size_t pos = args[argidx+1].find(':');
 				if (pos == std::string::npos)
@@ -260,17 +269,15 @@ struct SynthIce40Pass : public ScriptPass
 			if (!blif_file.empty() || help_mode) {
 				if (vpr || help_mode) {
 					run(stringf("opt_clean -purge"),
-						"                                        "
-						" (vpr mode)");
+							"                                 (vpr mode)");
 					run(stringf("write_blif -attr -cname -conn -param %s",
-								help_mode ? "<file-name>" : blif_file.c_str()),
-						" (vpr mode)");
+							help_mode ? "<file-name>" : blif_file.c_str()),
+							" (vpr mode)");
 				}
 				if (!vpr)
 					run(stringf("write_blif -gates -attr -param %s",
-								help_mode ? "<file-name>" : blif_file.c_str()),
-						"              "
-						" (non-vpr mode)");
+							help_mode ? "<file-name>" : blif_file.c_str()),
+							"       (non-vpr mode)");
 			}
 		}
 
@@ -279,6 +286,12 @@ struct SynthIce40Pass : public ScriptPass
 			if (!edif_file.empty() || help_mode)
 				run(stringf("write_edif %s", help_mode ? "<file-name>" : edif_file.c_str()));
 		}
+
+		if (check_label("json"))
+		{
+			if (!json_file.empty() || help_mode)
+				run(stringf("write_json %s", help_mode ? "<file-name>" : json_file.c_str()));
+		}
 	}
 } SynthIce40Pass;
 

From 0ff0ce4973db6f91b717b3771d8a9ca4cdb3a191 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 15 Jun 2018 18:56:44 +0200
Subject: [PATCH 32/45] Bugfix in liberty parser (as suggested by aiju in #569)

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/liberty/liberty.cc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/frontends/liberty/liberty.cc b/frontends/liberty/liberty.cc
index c9b6a54b2..b9e53a4be 100644
--- a/frontends/liberty/liberty.cc
+++ b/frontends/liberty/liberty.cc
@@ -148,7 +148,7 @@ static bool parse_func_reduce(RTLIL::Module *module, std::vector<token_t> &stack
 	}
 
 	if (0 <= top && stack[top].type == 2) {
-		if (next_token.type == '*' || next_token.type == '&' || next_token.type == 0 || next_token.type == '(')
+		if (next_token.type == '*' || next_token.type == '&' || next_token.type == 0 || next_token.type == '(' || next_token.type == '!')
 			return false;
 		stack[top].type = 3;
 		return true;

From d89560a0ba6402a8d13177909cc2c1f3b8b7c3e2 Mon Sep 17 00:00:00 2001
From: Edmond Cote <edmond.cote@gmail.com>
Date: Mon, 18 Jun 2018 17:29:01 -0700
Subject: [PATCH 33/45] Include module name for area summary stats

The PR prints the name of the module when displaying the final area count.

Pros:
- Easier for the user to `grep` for area information about a specific module

Cons:
- Arguably more verbose, less "pretty" than author desires

Verification:
~~~~
30c30
<    Chip area for this module: 20616.349000
---
>    Chip area for module '$paramod$d1738fc0bb353d517bc2caf8fef2abb20bced034\picorv32': 20616.349000
70c70
<    Chip area for this module: 88.697700
---
>    Chip area for module '\picorv32_axi_adapter': 88.697700
102c102
<    Chip area for this module: 20705.046700
---
>    Chip area for top module '\picorv32_axi': 20705.046700
~~~~
---
 passes/cmds/stat.cc | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc
index e52a192db..f1d958a1a 100644
--- a/passes/cmds/stat.cc
+++ b/passes/cmds/stat.cc
@@ -142,7 +142,7 @@ struct statdata_t
 		}
 	}
 
-	void log_data()
+	void log_data(RTLIL::IdString mod_name, bool top_mod)
 	{
 		log("   Number of wires:             %6d\n", num_wires);
 		log("   Number of wire bits:         %6d\n", num_wire_bits);
@@ -163,7 +163,7 @@ struct statdata_t
 
 		if (area != 0) {
 			log("\n");
-			log("   Chip area for this module: %f\n", area);
+			log("   Chip area for %smodule '%s': %f\n", (top_mod) ? "top " : "", mod_name.c_str(), area);
 		}
 	}
 };
@@ -275,7 +275,7 @@ struct StatPass : public Pass {
 			log("\n");
 			log("=== %s%s ===\n", RTLIL::id2cstr(mod->name), design->selected_whole_module(mod->name) ? "" : " (partially selected)");
 			log("\n");
-			data.log_data();
+			data.log_data(mod->name, false);
 		}
 
 		if (top_mod != NULL && GetSize(mod_stat) > 1)
@@ -288,7 +288,7 @@ struct StatPass : public Pass {
 			statdata_t data = hierarchy_worker(mod_stat, top_mod->name, 0);
 
 			log("\n");
-			data.log_data();
+			data.log_data(top_mod->name, true);
 		}
 
 		log("\n");

From 675a44b41a2df2c02ceccda2434bc3efac3e5e2f Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 19 Jun 2018 14:29:38 +0200
Subject: [PATCH 34/45] Be slightly less aggressive in "deminout" pass

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 passes/techmap/deminout.cc | 32 ++++++++++++++++++++++++++++----
 1 file changed, 28 insertions(+), 4 deletions(-)

diff --git a/passes/techmap/deminout.cc b/passes/techmap/deminout.cc
index ed4e45762..0b8fd5246 100644
--- a/passes/techmap/deminout.cc
+++ b/passes/techmap/deminout.cc
@@ -57,7 +57,7 @@ struct DeminoutPass : public Pass {
 			for (auto module : design->selected_modules())
 			{
 				SigMap sigmap(module);
-				pool<SigBit> bits_written, bits_used, bits_inout;
+				pool<SigBit> bits_written, bits_used, bits_inout, bits_tribuf;
 				dict<SigBit, int> bits_numports;
 
 				for (auto wire : module->wires())
@@ -82,6 +82,25 @@ struct DeminoutPass : public Pass {
 					if (cellport_in)
 						for (auto bit : sigmap(conn.second))
 							bits_used.insert(bit);
+
+					if (conn.first == "\\Y" && cell->type.in("$mux", "$pmux", "$_MUX_", "$_TBUF_"))
+					{
+						bool tribuf = (cell->type == "$_TBUF_");
+
+						if (!tribuf) {
+							for (auto &c : cell->connections()) {
+								if (!c.first.in("\\A", "\\B"))
+									continue;
+								for (auto b : sigmap(c.second))
+									if (b == State::Sz)
+										tribuf = true;
+							}
+						}
+
+						if (tribuf)
+							for (auto bit : sigmap(conn.second))
+								bits_tribuf.insert(bit);
+					}
 				}
 
 				for (auto wire : module->selected_wires())
@@ -95,10 +114,15 @@ struct DeminoutPass : public Pass {
 							if (bits_numports[bit] > 1 || bits_inout.count(bit))
 								new_input = true, new_output = true;
 
-							if (bits_written.count(bit))
+							if (bits_written.count(bit)) {
 								new_output = true;
-							else if (bits_used.count(bit))
-								new_input = true;
+								if (bits_tribuf.count(bit))
+									goto tribuf_bit;
+							} else {
+						tribuf_bit:
+								if (bits_used.count(bit))
+									new_input = true;
+							}
 						}
 
 						if (new_input != new_output) {

From 53e9a1549c503492820b3672331950fd0a580ef0 Mon Sep 17 00:00:00 2001
From: Serge Bazanski <q3k@symbioticeda.com>
Date: Tue, 19 Jun 2018 13:34:56 +0100
Subject: [PATCH 35/45] Add Protobuf backend

Signed-off-by: Serge Bazanski <q3k@symbioticeda.com>
---
 Makefile                       |   5 +
 backends/protobuf/.gitignore   |   2 +
 backends/protobuf/Makefile.inc |   8 +
 backends/protobuf/protobuf.cc  | 370 +++++++++++++++++++++++++++++++++
 misc/yosys.proto               | 175 ++++++++++++++++
 5 files changed, 560 insertions(+)
 create mode 100644 backends/protobuf/.gitignore
 create mode 100644 backends/protobuf/Makefile.inc
 create mode 100644 backends/protobuf/protobuf.cc
 create mode 100644 misc/yosys.proto

diff --git a/Makefile b/Makefile
index 2db6612a7..11803ec0a 100644
--- a/Makefile
+++ b/Makefile
@@ -15,6 +15,7 @@ ENABLE_EDITLINE := 0
 ENABLE_VERIFIC := 0
 ENABLE_COVER := 1
 ENABLE_LIBYOSYS := 0
+ENABLE_PROTOBUF := 0
 
 # other configuration flags
 ENABLE_GPROF := 0
@@ -325,6 +326,10 @@ CXXFLAGS += $(patsubst %,-I$(VERIFIC_DIR)/%,$(VERIFIC_COMPONENTS)) -DYOSYS_ENABL
 LDLIBS += $(patsubst %,$(VERIFIC_DIR)/%/*-linux.a,$(VERIFIC_COMPONENTS)) -lz
 endif
 
+ifeq ($(ENABLE_PROTOBUF),1)
+LDLIBS += $(shell pkg-config --cflags --libs protobuf)
+endif
+
 ifeq ($(ENABLE_COVER),1)
 CXXFLAGS += -DYOSYS_ENABLE_COVER
 endif
diff --git a/backends/protobuf/.gitignore b/backends/protobuf/.gitignore
new file mode 100644
index 000000000..849b38d45
--- /dev/null
+++ b/backends/protobuf/.gitignore
@@ -0,0 +1,2 @@
+yosys.pb.cc
+yosys.pb.h
diff --git a/backends/protobuf/Makefile.inc b/backends/protobuf/Makefile.inc
new file mode 100644
index 000000000..a6e3c5ab7
--- /dev/null
+++ b/backends/protobuf/Makefile.inc
@@ -0,0 +1,8 @@
+ifeq ($(ENABLE_PROTOBUF),1)
+
+backends/protobuf/yosys.pb.cc backends/protobuf/yosys.pb.h: share/yosys.proto
+	$(Q) cd misc && protoc --cpp_out "../backends/protobuf" yosys.proto
+
+OBJS += backends/protobuf/protobuf.o backends/protobuf/yosys.pb.o
+
+endif
diff --git a/backends/protobuf/protobuf.cc b/backends/protobuf/protobuf.cc
new file mode 100644
index 000000000..9a6fedee7
--- /dev/null
+++ b/backends/protobuf/protobuf.cc
@@ -0,0 +1,370 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
+ *  Copyright (C) 2018  Serge Bazanski <q3k@symbioticeda.com>
+ *
+ *  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 <google/protobuf/text_format.h>
+
+#include "kernel/rtlil.h"
+#include "kernel/register.h"
+#include "kernel/sigtools.h"
+#include "kernel/celltypes.h"
+#include "kernel/cellaigs.h"
+#include "kernel/log.h"
+#include "yosys.pb.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct ProtobufDesignSerializer
+{
+	bool aig_mode_;
+	bool use_selection_;
+	yosys::pb::Design *pb_;
+
+	Design *design_;
+	Module *module_;
+
+	SigMap sigmap_;
+	int sigidcounter_;
+	dict<SigBit, uint64_t> sigids_;
+	pool<Aig> aig_models_;
+
+
+	ProtobufDesignSerializer(bool use_selection, bool aig_mode) :
+			aig_mode_(aig_mode), use_selection_(use_selection) { }
+	
+	string get_name(IdString name)
+	{
+		return RTLIL::unescape_id(name);
+	}
+
+
+	void serialize_parameters(google::protobuf::Map<std::string, yosys::pb::Parameter> *out,
+		const dict<IdString, Const> &parameters)
+	{
+		for (auto &param : parameters) {
+			std::string key = get_name(param.first);
+			
+
+			yosys::pb::Parameter pb_param;
+
+			if ((param.second.flags & RTLIL::ConstFlags::CONST_FLAG_STRING) != 0) {
+				pb_param.set_str(param.second.decode_string());
+			} else if (GetSize(param.second.bits) > 64) {
+				pb_param.set_str(param.second.as_string());
+			} else {
+				pb_param.set_int_(param.second.as_int());
+			}
+
+			(*out)[key] = pb_param;
+		}
+	}
+
+	void get_bits(yosys::pb::BitVector *out, SigSpec sig)
+	{
+		for (auto bit : sigmap_(sig)) {
+			auto sig = out->add_signal();
+
+			// Constant driver.
+			if (bit.wire == nullptr) {
+				if (bit == State::S0) sig->set_constant(sig->CONSTANT_DRIVER_LOW);
+				else if (bit == State::S1) sig->set_constant(sig->CONSTANT_DRIVER_HIGH);
+				else if (bit == State::Sz) sig->set_constant(sig->CONSTANT_DRIVER_Z);
+				else sig->set_constant(sig->CONSTANT_DRIVER_X);
+				continue;
+			}
+
+			// Signal - give it a unique identifier.
+			if (sigids_.count(bit) == 0) {
+				sigids_[bit] = sigidcounter_++;
+			}
+			sig->set_id(sigids_[bit]);
+		}
+	}
+
+	void serialize_module(yosys::pb::Module* out, Module *module)
+	{
+		module_ = module;
+		log_assert(module_->design == design_);
+		sigmap_.set(module_);
+		sigids_.clear();
+		sigidcounter_ = 0;
+
+		serialize_parameters(out->mutable_attribute(), module_->attributes);
+
+		for (auto n : module_->ports) {
+			Wire *w = module->wire(n);
+			if (use_selection_ && !module_->selected(w))
+				continue;
+
+			yosys::pb::Module::Port pb_port;
+			pb_port.set_direction(w->port_input ? w->port_output ?
+				yosys::pb::DIRECTION_INOUT : yosys::pb::DIRECTION_INPUT : yosys::pb::DIRECTION_OUTPUT);
+			get_bits(pb_port.mutable_bits(), w);
+			(*out->mutable_port())[get_name(n)] = pb_port;
+		}
+
+		for (auto c : module_->cells()) {
+			if (use_selection_ && !module_->selected(c))
+				continue;
+
+			yosys::pb::Module::Cell pb_cell;
+			pb_cell.set_hide_name(c->name[0] == '$');
+			pb_cell.set_type(get_name(c->type));
+
+			if (aig_mode_) {
+				Aig aig(c);
+				if (aig.name.empty())
+					continue;
+				pb_cell.set_model(aig.name);
+				aig_models_.insert(aig);
+			}
+			serialize_parameters(pb_cell.mutable_parameter(), c->parameters);
+			serialize_parameters(pb_cell.mutable_attribute(), c->attributes);
+
+			if (c->known()) {
+				for (auto &conn : c->connections()) {
+					yosys::pb::Direction direction = yosys::pb::DIRECTION_OUTPUT;
+					if (c->input(conn.first))
+						direction = c->output(conn.first) ? yosys::pb::DIRECTION_INOUT : yosys::pb::DIRECTION_INPUT;
+					(*pb_cell.mutable_port_direction())[get_name(conn.first)] = direction;
+				}
+			}
+			for (auto &conn : c->connections()) {
+				yosys::pb::BitVector vec;
+				get_bits(&vec, conn.second);
+				(*pb_cell.mutable_connection())[get_name(conn.first)] = vec;
+			}
+
+			(*out->mutable_cell())[get_name(c->name)] = pb_cell;
+		}
+
+		for (auto w : module_->wires()) {
+			if (use_selection_ && !module_->selected(w))
+				continue;
+
+			auto netname = out->add_netname();
+			netname->set_hide_name(w->name[0] == '$');
+			get_bits(netname->mutable_bits(), w);
+			serialize_parameters(netname->mutable_attributes(), w->attributes);
+		}
+	}
+
+
+	void serialize_models(google::protobuf::Map<string, yosys::pb::Model> *models)
+	{
+		for (auto &aig : aig_models_) {
+			yosys::pb::Model pb_model;
+			for (auto &node : aig.nodes) {
+				auto pb_node = pb_model.add_node();
+				if (node.portbit >= 0) {
+					if (node.inverter) {
+						pb_node->set_type(pb_node->TYPE_NPORT);
+					} else {
+						pb_node->set_type(pb_node->TYPE_PORT);
+					}
+					auto port = pb_node->mutable_port();
+					port->set_portname(log_id(node.portname));
+					port->set_bitindex(node.portbit);
+				} else if (node.left_parent < 0 && node.right_parent < 0) {
+					if (node.inverter) {
+						pb_node->set_type(pb_node->TYPE_TRUE);
+					} else {
+						pb_node->set_type(pb_node->TYPE_FALSE);
+					}
+				} else {
+					if (node.inverter) {
+						pb_node->set_type(pb_node->TYPE_NAND);
+					} else {
+						pb_node->set_type(pb_node->TYPE_AND);
+					}
+					auto gate = pb_node->mutable_gate();
+					gate->set_left(node.left_parent);
+					gate->set_right(node.right_parent);
+				}
+				for (auto &op : node.outports) {
+					auto pb_op = pb_node->add_out_port();
+					pb_op->set_name(log_id(op.first));
+					pb_op->set_bit_index(op.second);
+				}
+			}
+			(*models)[aig.name] = pb_model;
+		}
+	}
+	
+	void serialize_design(yosys::pb::Design *pb, Design *design)
+	{
+		GOOGLE_PROTOBUF_VERIFY_VERSION;
+		pb_ = pb;
+		pb_->Clear();
+		pb_->set_creator(yosys_version_str);
+
+		design_ = design;
+		design_->sort();
+
+		auto modules = use_selection_ ? design_->selected_modules() : design_->modules();
+		for (auto mod : modules) {
+			yosys::pb::Module pb_mod;
+			serialize_module(&pb_mod, mod);
+			(*pb->mutable_modules())[mod->name.str()] = pb_mod;
+		}
+
+		serialize_models(pb_->mutable_models());
+	}
+};
+
+struct ProtobufBackend : public Backend {
+	ProtobufBackend(): Backend("protobuf", "write design to a Protocol Buffer file") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    write_protobuf [options] [filename]\n");
+		log("\n");
+		log("Write a JSON netlist of the current design.\n");
+		log("\n");
+		log("    -aig\n");
+		log("        include AIG models for the different gate types\n");
+		log("\n");
+		log("    -text\n");
+		log("        output protobuf in Text/ASCII representation\n");
+		log("\n");
+		log("The schema of the output Protocol Buffer is defined in misc/yosys.pb in the\n");
+		log("Yosys source code distribution.\n");
+		log("\n");
+	}
+	virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
+	{
+		bool aig_mode = false;
+		bool text_mode = false;
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-aig") {
+				aig_mode = true;
+				continue;
+			}
+			if (args[argidx] == "-text") {
+				text_mode = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(f, filename, args, argidx);
+
+		log_header(design, "Executing Protobuf backend.\n");
+
+		yosys::pb::Design pb;
+		ProtobufDesignSerializer serializer(false, aig_mode);
+		serializer.serialize_design(&pb, design);
+
+		if (text_mode) {
+			string out;
+			google::protobuf::TextFormat::PrintToString(pb, &out);
+			*f << out;
+		} else {
+			pb.SerializeToOstream(f);
+		}
+	}
+} ProtobufBackend;
+
+struct ProtobufPass : public Pass {
+	ProtobufPass() : Pass("protobuf", "write design in Protobuf format") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    protobuf [options] [selection]\n");
+		log("\n");
+		log("Write a JSON netlist of all selected objects.\n");
+		log("\n");
+		log("    -o <filename>\n");
+		log("        write to the specified file.\n");
+		log("\n");
+		log("    -aig\n");
+		log("        include AIG models for the different gate types\n");
+		log("\n");
+		log("    -text\n");
+		log("        output protobuf in Text/ASCII representation\n");
+		log("\n");
+		log("The schema of the output Protocol Buffer is defined in misc/yosys.pb in the\n");
+		log("Yosys source code distribution.\n");
+		log("\n");
+	}
+	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+	{
+		std::string filename;
+		bool aig_mode = false;
+		bool text_mode = false;
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++)
+		{
+			if (args[argidx] == "-o" && argidx+1 < args.size()) {
+				filename = args[++argidx];
+				continue;
+			}
+			if (args[argidx] == "-aig") {
+				aig_mode = true;
+				continue;
+			}
+			if (args[argidx] == "-text") {
+				text_mode = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(args, argidx, design);
+
+		std::ostream *f;
+		std::stringstream buf;
+
+		if (!filename.empty()) {
+			std::ofstream *ff = new std::ofstream;
+			ff->open(filename.c_str(), std::ofstream::trunc);
+			if (ff->fail()) {
+				delete ff;
+				log_error("Can't open file `%s' for writing: %s\n", filename.c_str(), strerror(errno));
+			}
+			f = ff;
+		} else {
+			f = &buf;
+		}
+
+		yosys::pb::Design pb;
+		ProtobufDesignSerializer serializer(true, aig_mode);
+		serializer.serialize_design(&pb, design);
+
+		if (text_mode) {
+			string out;
+			google::protobuf::TextFormat::PrintToString(pb, &out);
+			*f << out;
+		} else {
+			pb.SerializeToOstream(f);
+		}
+
+		if (!filename.empty()) {
+			delete f;
+		} else {
+			log("%s", buf.str().c_str());
+		}
+	}
+} ProtobufPass;
+
+PRIVATE_NAMESPACE_END;
diff --git a/misc/yosys.proto b/misc/yosys.proto
new file mode 100644
index 000000000..2870176cb
--- /dev/null
+++ b/misc/yosys.proto
@@ -0,0 +1,175 @@
+//
+// yosys -- Yosys Open SYnthesis Suite
+// 
+// Copyright (C) 2018  Serge Bazanski <q3k@symbioticeda.com>
+// 
+// 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.
+//
+
+/// Protobuf definition of Yosys RTLIL dump/restore format for RTL designs.
+
+syntax = "proto3";
+
+package yosys.pb;
+
+// Port direction.
+enum Direction {
+    DIRECTION_INVALID = 0;
+    DIRECTION_INPUT = 1;
+    DIRECTION_OUTPUT = 2;
+    DIRECTION_INOUT = 3;
+}
+
+// A freeform parameter/attribute value.
+message Parameter {
+    oneof value {
+        int64 int = 1;
+        string str = 2;
+    }
+}
+
+// A signal in the design - either a unique identifier for one, or a constant
+// driver (low or high).
+message Signal {
+    // A constant signal driver in the design.
+    enum ConstantDriver {
+        CONSTANT_DRIVER_INVALID = 0;
+        CONSTANT_DRIVER_LOW = 1;
+        CONSTANT_DRIVER_HIGH = 2;
+        CONSTANT_DRIVER_Z = 3;
+        CONSTANT_DRIVER_X = 4;
+    }
+    oneof type {
+        // Signal uniquely identified by ID number.
+        int64 id = 1;
+        // Constant driver.
+        ConstantDriver constant = 2;
+    }
+}
+
+// A vector of signals.
+message BitVector {
+    repeated Signal signal = 1;
+}
+
+// A netlist module.
+message Module {
+    // Freeform attributes.
+    map<string, Parameter> attribute = 1;
+
+    // Named ports in this module.
+    message Port {
+        Direction direction = 1;
+        BitVector bits = 2;
+    }
+    map<string, Port> port = 2;
+    
+    // Named cells in this module.
+    message Cell {
+        // Set to true when the name of this cell is automatically created and
+        // likely not of interest for a regular user.
+        bool hide_name = 1;
+        string type = 2;
+        // Set if this module has an AIG model available.
+        string model = 3;
+        // Freeform parameters.
+        map<string, Parameter> parameter = 4;
+        // Freeform attributes.
+        map<string, Parameter> attribute = 5;
+
+        /// Ports of the cell.
+        // Direction of the port, if interface is known.
+        map<string, Direction> port_direction = 6;
+        // Connection of named port to signal(s).
+        map<string, BitVector> connection = 7;
+    }
+    map<string, Cell> cell = 3;
+
+    // Nets in this module.
+    message Netname {
+        // Set to true when the name of this net is automatically created and
+        // likely not of interest for a regular user.
+        bool hide_name = 1;
+        // Signal(s) that make up this net.
+        BitVector bits = 2;
+        // Freeform attributes.
+        map<string, Parameter> attributes = 3;
+    }
+    repeated Netname netname = 4;
+}
+
+// And-Inverter-Graph model.
+message Model {
+    message Node {
+        // Type of AIG node - or, what its' value is.
+        enum Type {
+            TYPE_INVALID = 0;
+            // The node's value is the value of the specified input port bit.
+            TYPE_PORT = 1;
+            // The node's value is the inverted value of the specified input
+            // port bit.
+            TYPE_NPORT = 2;
+            // The node's value is the ANDed value of specified nodes.
+            TYPE_AND = 3;
+            // The node's value is the NANDed value of specified nodes.
+            TYPE_NAND = 4;
+            // The node's value is a constant 1.
+            TYPE_TRUE = 5;
+            // The node's value is a constant 0.
+            TYPE_FALSE = 6;
+        };
+        Type type = 1;
+    
+        message Port {
+            // Name of port.
+            string portname = 1;
+            // Bit index in port.
+            int64 bitindex = 2;
+        }
+        message Gate {
+            // Node index of left side of operation.
+            int64 left = 1;
+            // Node index of right side of operation.
+            int64 right = 2;
+        }
+        oneof node {
+            // Set for PORT, NPORT
+            Port port = 2;
+            // Set for AND, NAND.
+            Gate gate = 3;
+        }
+    
+        // Set when the node drives given output port(s).
+        message OutPort {
+            // Name of port.
+            string name = 1;
+            // Bit index in port.
+            int64 bit_index = 2;
+        }
+        repeated OutPort out_port = 4;
+    }
+
+    // List of  AIG nodes - each is explicitely numbered by its' index in this
+    // array.
+    repeated Node node = 1;
+}
+
+// A Yosys design netlist dumped from RTLIL.
+message Design {
+    // Human-readable freeform 'remark' string.
+    string creator = 1;
+    // List of named modules in design.
+    map<string, Module> modules = 2;
+    // List of named AIG models in design (if AIG export enabled).
+    map<string, Model> models = 3;
+}

From 1690dafde135c1077d84cb14c1275d74a2f7424d Mon Sep 17 00:00:00 2001
From: Sergiusz Bazanski <q3k@q3k.org>
Date: Wed, 20 Jun 2018 19:28:43 +0100
Subject: [PATCH 36/45] Fix protobuf build

---
 backends/protobuf/Makefile.inc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/backends/protobuf/Makefile.inc b/backends/protobuf/Makefile.inc
index a6e3c5ab7..834cad42c 100644
--- a/backends/protobuf/Makefile.inc
+++ b/backends/protobuf/Makefile.inc
@@ -1,6 +1,6 @@
 ifeq ($(ENABLE_PROTOBUF),1)
 
-backends/protobuf/yosys.pb.cc backends/protobuf/yosys.pb.h: share/yosys.proto
+backends/protobuf/yosys.pb.cc backends/protobuf/yosys.pb.h: misc/yosys.proto
 	$(Q) cd misc && protoc --cpp_out "../backends/protobuf" yosys.proto
 
 OBJS += backends/protobuf/protobuf.o backends/protobuf/yosys.pb.o

From 5f2bc1ce7672324370ce5570f41ebd74f670b26e Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 20 Jun 2018 23:45:01 +0200
Subject: [PATCH 37/45] Add automatic verific import in hierarchy command

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verific.cc  | 53 +++++++++++++++++++++++++++++++++++
 frontends/verific/verific.h   |  3 ++
 passes/hierarchy/hierarchy.cc | 20 ++++++++++++-
 3 files changed, 75 insertions(+), 1 deletion(-)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index f67337754..ab5c545a1 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -62,6 +62,7 @@ using namespace Verific;
 YOSYS_NAMESPACE_BEGIN
 
 int verific_verbose;
+bool verific_import_pending;
 string verific_error_msg;
 
 void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
@@ -1613,6 +1614,52 @@ struct VerificExtNets
 	}
 };
 
+void verific_import(Design *design, std::string top)
+{
+	std::set<Netlist*> nl_todo, nl_done;
+
+	{
+		VhdlLibrary *vhdl_lib = vhdl_file::GetLibrary("work", 1);
+		VeriLibrary *veri_lib = veri_file::GetLibrary("work", 1);
+
+		Array veri_libs, vhdl_libs;
+		if (vhdl_lib) vhdl_libs.InsertLast(vhdl_lib);
+		if (veri_lib) veri_libs.InsertLast(veri_lib);
+
+		Array *netlists = hier_tree::ElaborateAll(&veri_libs, &vhdl_libs);
+		Netlist *nl;
+		int i;
+
+		FOREACH_ARRAY_ITEM(netlists, i, nl) {
+			if (top.empty() || nl->Owner()->Name() == top)
+				nl_todo.insert(nl);
+		}
+
+		delete netlists;
+	}
+
+	if (!verific_error_msg.empty())
+		log_error("%s\n", verific_error_msg.c_str());
+
+	while (!nl_todo.empty()) {
+		Netlist *nl = *nl_todo.begin();
+		if (nl_done.count(nl) == 0) {
+			VerificImporter importer(false, false, false, false, false, false);
+			importer.import_netlist(design, nl, nl_todo);
+		}
+		nl_todo.erase(nl);
+		nl_done.insert(nl);
+	}
+
+	veri_file::Reset();
+	vhdl_file::Reset();
+	Libset::Reset();
+	verific_import_pending = false;
+
+	if (!verific_error_msg.empty())
+		log_error("%s\n", verific_error_msg.c_str());
+}
+
 YOSYS_NAMESPACE_END
 #endif /* YOSYS_ENABLE_VERIFIC */
 
@@ -1789,6 +1836,7 @@ struct VerificPass : public Pass {
 			if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, "work", veri_file::MFCU))
 					log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n");
 
+			verific_import_pending = true;
 			goto check_error;
 		}
 
@@ -1797,6 +1845,7 @@ struct VerificPass : public Pass {
 			for (argidx++; argidx < GetSize(args); argidx++)
 				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_87))
 					log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", args[argidx].c_str());
+			verific_import_pending = true;
 			goto check_error;
 		}
 
@@ -1805,6 +1854,7 @@ struct VerificPass : public Pass {
 			for (argidx++; argidx < GetSize(args); argidx++)
 				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_93))
 					log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", args[argidx].c_str());
+			verific_import_pending = true;
 			goto check_error;
 		}
 
@@ -1813,6 +1863,7 @@ struct VerificPass : public Pass {
 			for (argidx++; argidx < GetSize(args); argidx++)
 				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_2K))
 					log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", args[argidx].c_str());
+			verific_import_pending = true;
 			goto check_error;
 		}
 
@@ -1821,6 +1872,7 @@ struct VerificPass : public Pass {
 			for (argidx++; argidx < GetSize(args); argidx++)
 				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_2008))
 					log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", args[argidx].c_str());
+			verific_import_pending = true;
 			goto check_error;
 		}
 
@@ -2031,6 +2083,7 @@ struct VerificPass : public Pass {
 			veri_file::Reset();
 			vhdl_file::Reset();
 			Libset::Reset();
+			verific_import_pending = false;
 			goto check_error;
 		}
 
diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h
index 86a743ea1..cbd9314db 100644
--- a/frontends/verific/verific.h
+++ b/frontends/verific/verific.h
@@ -25,6 +25,9 @@ YOSYS_NAMESPACE_BEGIN
 
 extern int verific_verbose;
 
+extern bool verific_import_pending;
+extern void verific_import(Design *design, std::string top = std::string());
+
 extern pool<int> verific_sva_prims;
 
 struct VerificImporter;
diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index bfb8e7f95..e61851481 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -18,6 +18,7 @@
  */
 
 #include "kernel/yosys.h"
+#include "frontends/verific/verific.h"
 #include <stdlib.h>
 #include <stdio.h>
 #include <set>
@@ -421,6 +422,7 @@ struct HierarchyPass : public Pass {
 		bool flag_simcheck = false;
 		bool purge_lib = false;
 		RTLIL::Module *top_mod = NULL;
+		std::string load_top_mod;
 		std::vector<std::string> libdirs;
 
 		bool auto_top_mode = false;
@@ -511,7 +513,7 @@ struct HierarchyPass : public Pass {
 					top_mod = design->modules_.count(RTLIL::escape_id(args[argidx])) ? design->modules_.at(RTLIL::escape_id(args[argidx])) : NULL;
 				}
 				if (top_mod == NULL)
-					log_cmd_error("Module `%s' not found!\n", args[argidx].c_str());
+					load_top_mod = args[argidx];
 				continue;
 			}
 			if (args[argidx] == "-auto-top") {
@@ -522,6 +524,22 @@ struct HierarchyPass : public Pass {
 		}
 		extra_args(args, argidx, design, false);
 
+		if (!load_top_mod.empty()) {
+#ifdef YOSYS_ENABLE_VERIFIC
+			if (verific_import_pending) {
+				verific_import(design, load_top_mod);
+				top_mod = design->module(RTLIL::escape_id(load_top_mod));
+			}
+#endif
+			if (top_mod == NULL)
+				log_cmd_error("Module `%s' not found!\n", load_top_mod.c_str());
+		} else {
+#ifdef YOSYS_ENABLE_VERIFIC
+			if (verific_import_pending)
+				verific_import(design);
+#endif
+		}
+
 		if (generate_mode) {
 			generate(design, generate_cells, generate_ports);
 			return;

From d412b17259ad7c2003dc14ec452a2a0a6fc3ba91 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 21 Jun 2018 16:56:55 +0200
Subject: [PATCH 38/45] Add simplified "read" command, enable extnets in
 implicit Verific import

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verific.cc | 84 ++++++++++++++++++++++++++++++++++++
 1 file changed, 84 insertions(+)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index ab5c545a1..3c6566f62 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1641,6 +1641,10 @@ void verific_import(Design *design, std::string top)
 	if (!verific_error_msg.empty())
 		log_error("%s\n", verific_error_msg.c_str());
 
+	VerificExtNets worker;
+	for (auto nl : nl_todo)
+		worker.run(nl);
+
 	while (!nl_todo.empty()) {
 		Netlist *nl = *nl_todo.begin();
 		if (nl_done.count(nl) == 0) {
@@ -2101,5 +2105,85 @@ struct VerificPass : public Pass {
 #endif
 } VerificPass;
 
+struct ReadPass : public Pass {
+	ReadPass() : Pass("read", "load HDL designs") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>..\n");
+		log("\n");
+		log("Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support\n");
+		log("is only available via Verific.)\n");
+		log("\n");
+		log("\n");
+		log("    read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
+		log("\n");
+		log("Load the specified VHDL files. (Requires Verific.)\n");
+		log("\n");
+		log("\n");
+		log("    read -define <macro>[=<value>]..\n");
+		log("\n");
+		log("Set global Verilog/SystemVerilog defines.\n");
+		log("\n");
+	}
+	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+	{
+		if (args.size() < 2)
+			log_cmd_error("Missing mode parameter.\n");
+
+		if (args.size() < 3)
+			log_cmd_error("Missing file name parameter.\n");
+
+		if (args[1] == "-vlog95" || args[1] == "-vlog2k") {
+#ifdef YOSYS_ENABLE_VERIFIC
+			args[0] = "verific";
+#else
+			args[0] = "read_verilog";
+			args.erase(args.begin()+1, args.begin()+2);
+#endif
+			Pass::call(design, args);
+			return;
+		}
+
+		if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv") {
+#ifdef YOSYS_ENABLE_VERIFIC
+			args[0] = "verific";
+#else
+			args[0] = "read_verilog";
+			args[1] = "-sv";
+#endif
+			Pass::call(design, args);
+			return;
+		}
+
+		if (args[1] == "-vhdl87" || args[1] == "-vhdl93" || args[1] == "-vhdl2k" || args[1] == "-vhdl2008" || args[1] == "-vhdl") {
+#ifdef YOSYS_ENABLE_VERIFIC
+			args[0] = "verific";
+#else
+			log_cmd_error("This version of Yosys is built without Verific support.\n");
+#endif
+			Pass::call(design, args);
+			return;
+		}
+
+		if (args[1] == "-define") {
+#ifdef YOSYS_ENABLE_VERIFIC
+			args[0] = "verific";
+			args[1] = "-vlog-define";
+			Pass::call(design, args);
+#endif
+			args[0] = "verilog_defines";
+			args.erase(args.begin()+1, args.begin()+2);
+			for (int i = 1; i < GetSize(args); i++)
+				args[i] = "-D" + args[i];
+			Pass::call(design, args);
+			return;
+		}
+
+		log_cmd_error("Missing or unsupported mode parameter.\n");
+	}
+} ReadPass;
+
 PRIVATE_NAMESPACE_END
 

From 848c3c5c889945f64ddefc8fe45342a4338dc769 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 22 Jun 2018 20:40:22 +0200
Subject: [PATCH 39/45] Add YOSYS_NOVERIFIC env variable for temporarily
 disabling verific

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verific.cc | 62 +++++++++++++++++++++++-------------
 1 file changed, 40 insertions(+), 22 deletions(-)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 3c6566f62..fb27810dd 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1669,6 +1669,16 @@ YOSYS_NAMESPACE_END
 
 PRIVATE_NAMESPACE_BEGIN
 
+bool check_noverific_env()
+{
+	const char *e = getenv("YOSYS_NOVERIFIC");
+	if (e == nullptr)
+		return false;
+	if (atoi(e) == 0)
+		return false;
+	return true;
+}
+
 struct VerificPass : public Pass {
 	VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
 	virtual void help()
@@ -1759,6 +1769,9 @@ struct VerificPass : public Pass {
 #ifdef YOSYS_ENABLE_VERIFIC
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
+		if (check_noverific_env())
+			log_cmd_error("This version of Yosys is built without Verific support.\n");
+
 		log_header(design, "Executing VERIFIC (loading SystemVerilog and VHDL designs using Verific).\n");
 
 		Message::SetConsoleOutput(0);
@@ -2135,44 +2148,50 @@ struct ReadPass : public Pass {
 		if (args.size() < 3)
 			log_cmd_error("Missing file name parameter.\n");
 
-		if (args[1] == "-vlog95" || args[1] == "-vlog2k") {
 #ifdef YOSYS_ENABLE_VERIFIC
-			args[0] = "verific";
+		bool use_verific = !check_noverific_env();
 #else
-			args[0] = "read_verilog";
-			args.erase(args.begin()+1, args.begin()+2);
+		bool use_verific = false;
 #endif
+
+		if (args[1] == "-vlog95" || args[1] == "-vlog2k") {
+			if (use_verific) {
+				args[0] = "verific";
+			} else {
+				args[0] = "read_verilog";
+				args.erase(args.begin()+1, args.begin()+2);
+			}
 			Pass::call(design, args);
 			return;
 		}
 
 		if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv") {
-#ifdef YOSYS_ENABLE_VERIFIC
-			args[0] = "verific";
-#else
-			args[0] = "read_verilog";
-			args[1] = "-sv";
-#endif
+			if (use_verific) {
+				args[0] = "verific";
+			} else {
+				args[0] = "read_verilog";
+				args[1] = "-sv";
+			}
 			Pass::call(design, args);
 			return;
 		}
 
 		if (args[1] == "-vhdl87" || args[1] == "-vhdl93" || args[1] == "-vhdl2k" || args[1] == "-vhdl2008" || args[1] == "-vhdl") {
-#ifdef YOSYS_ENABLE_VERIFIC
-			args[0] = "verific";
-#else
-			log_cmd_error("This version of Yosys is built without Verific support.\n");
-#endif
-			Pass::call(design, args);
+			if (use_verific) {
+				args[0] = "verific";
+				Pass::call(design, args);
+			} else {
+				log_cmd_error("This version of Yosys is built without Verific support.\n");
+			}
 			return;
 		}
 
 		if (args[1] == "-define") {
-#ifdef YOSYS_ENABLE_VERIFIC
-			args[0] = "verific";
-			args[1] = "-vlog-define";
-			Pass::call(design, args);
-#endif
+			if (use_verific) {
+				args[0] = "verific";
+				args[1] = "-vlog-define";
+				Pass::call(design, args);
+			}
 			args[0] = "verilog_defines";
 			args.erase(args.begin()+1, args.begin()+2);
 			for (int i = 1; i < GetSize(args); i++)
@@ -2186,4 +2205,3 @@ struct ReadPass : public Pass {
 } ReadPass;
 
 PRIVATE_NAMESPACE_END
-

From fe2ee833e154691ef61cc72833b86e02266039a2 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 28 Jun 2018 16:57:03 +0200
Subject: [PATCH 40/45] Fix handling of signed memories

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/ast/genrtlil.cc | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 40cbbc2a3..d9f0039af 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -1300,6 +1300,9 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 			cell->parameters["\\CLK_POLARITY"] = RTLIL::Const(0);
 			cell->parameters["\\TRANSPARENT"] = RTLIL::Const(0);
 
+			if (!sign_hint)
+				is_signed = false;
+
 			return RTLIL::SigSpec(wire);
 		}
 

From 07e616900c2d6ddf021644f9687954d92ac8109a Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 28 Jun 2018 23:43:38 +0200
Subject: [PATCH 41/45] Add "read -undef"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verific.cc | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index fb27810dd..4fa74df3d 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1715,6 +1715,11 @@ struct VerificPass : public Pass {
 		log("Add Verilog defines. (The macros SYNTHESIS and VERIFIC are defined implicitly.)\n");
 		log("\n");
 		log("\n");
+		log("    verific -vlog-undef <macro>..\n");
+		log("\n");
+		log("Remove Verilog defines previously set with -vlog-define.\n");
+		log("\n");
+		log("\n");
 		log("    verific -import [options] <top-module>..\n");
 		log("\n");
 		log("Elaborate the design for the specified top modules, import to Yosys and\n");
@@ -1828,6 +1833,14 @@ struct VerificPass : public Pass {
 			goto check_error;
 		}
 
+		if (GetSize(args) > argidx && args[argidx] == "-vlog-undef") {
+			for (argidx++; argidx < GetSize(args); argidx++) {
+				string name = args[argidx];
+				veri_file::UndefineMacro(name.c_str());
+			}
+			goto check_error;
+		}
+
 		if (GetSize(args) > argidx && (args[argidx] == "-vlog95" || args[argidx] == "-vlog2k" || args[argidx] == "-sv2005" ||
 				args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv"))
 		{
@@ -2139,6 +2152,11 @@ struct ReadPass : public Pass {
 		log("\n");
 		log("Set global Verilog/SystemVerilog defines.\n");
 		log("\n");
+		log("\n");
+		log("    read -undef <macro>..\n");
+		log("\n");
+		log("Unset global Verilog/SystemVerilog defines.\n");
+		log("\n");
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
 	{
@@ -2200,6 +2218,20 @@ struct ReadPass : public Pass {
 			return;
 		}
 
+		if (args[1] == "-undef") {
+			if (use_verific) {
+				args[0] = "verific";
+				args[1] = "-vlog-undef";
+				Pass::call(design, args);
+			}
+			args[0] = "verilog_defines";
+			args.erase(args.begin()+1, args.begin()+2);
+			for (int i = 1; i < GetSize(args); i++)
+				args[i] = "-U" + args[i];
+			Pass::call(design, args);
+			return;
+		}
+
 		log_cmd_error("Missing or unsupported mode parameter.\n");
 	}
 } ReadPass;

From afedb2d03ee07738025ae77d73d280044c29ec2f Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 28 Jun 2018 23:58:15 +0200
Subject: [PATCH 42/45] Add "read -sv -D" support

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verific.cc | 27 +++++++++++++++++++++++++--
 1 file changed, 25 insertions(+), 2 deletions(-)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 4fa74df3d..c9a071f70 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1693,6 +1693,9 @@ struct VerificPass : public Pass {
 		log("Files passed to different calls to this command are treated as belonging to\n");
 		log("different compilation units.\n");
 		log("\n");
+		log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
+		log("the language version (and before file names) to set additional verilog defines.\n");
+		log("\n");
 		log("\n");
 		log("    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
 		log("\n");
@@ -1860,8 +1863,25 @@ struct VerificPass : public Pass {
 			else
 				log_abort();
 
-			for (argidx++; argidx < GetSize(args); argidx++)
-				file_names.Insert(args[argidx].c_str());
+			for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].substr(0, 2) == "-D"; argidx++) {
+				std::string name = args[argidx].substr(2);
+				if (args[argidx] == "-D") {
+					if (++argidx >= GetSize(args))
+						break;
+					name = args[argidx];
+				}
+				size_t equal = name.find('=');
+				if (equal != std::string::npos) {
+					string value = name.substr(equal+1);
+					name = name.substr(0, equal);
+					veri_file::DefineMacro(name.c_str(), value.c_str());
+				} else {
+					veri_file::DefineMacro(name.c_str());
+				}
+			}
+
+			while (argidx < GetSize(args))
+				file_names.Insert(args[argidx++].c_str());
 
 			if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, "work", veri_file::MFCU))
 					log_cmd_error("Reading Verilog/SystemVerilog sources failed.\n");
@@ -2142,6 +2162,9 @@ struct ReadPass : public Pass {
 		log("Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support\n");
 		log("is only available via Verific.)\n");
 		log("\n");
+		log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
+		log("the language version (and before file names) to set additional verilog defines.\n");
+		log("\n");
 		log("\n");
 		log("    read {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
 		log("\n");

From ebf0f003d3e8d219b396d4c6a3943e1ce54d2879 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 29 Jun 2018 10:02:27 +0200
Subject: [PATCH 43/45] Add "verific -formal" and "read -formal"

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verific.cc | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index c9a071f70..62a8028b8 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -1695,8 +1695,13 @@ struct VerificPass : public Pass {
 		log("\n");
 		log("Additional -D<macro>[=<value>] options may be added after the option indicating\n");
 		log("the language version (and before file names) to set additional verilog defines.\n");
+		log("The macros SYNTHESIS and VERIFIC are defined implicitly.\n");
 		log("\n");
 		log("\n");
+		log("    verific -formal <verilog-file>..\n");
+		log("\n");
+		log("Like -sv, but define FORMAL instead of SYNTHESIS.\n");
+		log("\n");
 		log("    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
 		log("\n");
 		log("Load the specified VHDL files into Verific.\n");
@@ -1715,7 +1720,7 @@ struct VerificPass : public Pass {
 		log("\n");
 		log("    verific -vlog-define <macro>[=<value>]..\n");
 		log("\n");
-		log("Add Verilog defines. (The macros SYNTHESIS and VERIFIC are defined implicitly.)\n");
+		log("Add Verilog defines.\n");
 		log("\n");
 		log("\n");
 		log("    verific -vlog-undef <macro>..\n");
@@ -1790,8 +1795,6 @@ struct VerificPass : public Pass {
 		RuntimeFlags::SetVar("veri_extract_dualport_rams", 0);
 		RuntimeFlags::SetVar("veri_extract_multiport_rams", 1);
 		RuntimeFlags::SetVar("db_infer_wide_operators", 1);
-		veri_file::DefineCmdLineMacro("VERIFIC");
-		veri_file::DefineCmdLineMacro("SYNTHESIS");
 
 		verific_verbose = 0;
 
@@ -1845,7 +1848,7 @@ struct VerificPass : public Pass {
 		}
 
 		if (GetSize(args) > argidx && (args[argidx] == "-vlog95" || args[argidx] == "-vlog2k" || args[argidx] == "-sv2005" ||
-				args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv"))
+				args[argidx] == "-sv2009" || args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal"))
 		{
 			Array file_names;
 			unsigned verilog_mode;
@@ -1858,11 +1861,14 @@ struct VerificPass : public Pass {
 				verilog_mode = veri_file::SYSTEM_VERILOG_2005;
 			else if (args[argidx] == "-sv2009")
 				verilog_mode = veri_file::SYSTEM_VERILOG_2009;
-			else if (args[argidx] == "-sv2012" || args[argidx] == "-sv")
+			else if (args[argidx] == "-sv2012" || args[argidx] == "-sv" || args[argidx] == "-formal")
 				verilog_mode = veri_file::SYSTEM_VERILOG;
 			else
 				log_abort();
 
+			veri_file::DefineMacro("VERIFIC");
+			veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS");
+
 			for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].substr(0, 2) == "-D"; argidx++) {
 				std::string name = args[argidx].substr(2);
 				if (args[argidx] == "-D") {
@@ -2157,7 +2163,7 @@ struct ReadPass : public Pass {
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 		log("\n");
-		log("    read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv} <verilog-file>..\n");
+		log("    read {-vlog95|-vlog2k|-sv2005|-sv2009|-sv2012|-sv|-formal} <verilog-file>..\n");
 		log("\n");
 		log("Load the specified Verilog/SystemVerilog files. (Full SystemVerilog support\n");
 		log("is only available via Verific.)\n");
@@ -2206,11 +2212,13 @@ struct ReadPass : public Pass {
 			return;
 		}
 
-		if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv") {
+		if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv" || args[1] == "-formal") {
 			if (use_verific) {
 				args[0] = "verific";
 			} else {
 				args[0] = "read_verilog";
+				if (args[1] == "-formal")
+					args.insert(args.begin()+1, std::string());
 				args[1] = "-sv";
 			}
 			Pass::call(design, args);

From 0404cf61d5f230de70bc6e6e6bf907bf7b112e0d Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 29 Jun 2018 19:21:04 +0200
Subject: [PATCH 44/45] Add verific support for eventually properties

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verificsva.cc | 110 ++++++++++++++++++++++++++++++--
 1 file changed, 105 insertions(+), 5 deletions(-)

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 4e440b4ca..9312fd6e6 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -980,7 +980,6 @@ struct VerificSvaImporter
 	bool mode_assume = false;
 	bool mode_cover = false;
 	bool mode_trigger = false;
-	bool eventually = false;
 
 	Instance *net_to_ast_driver(Net *n)
 	{
@@ -1487,6 +1486,69 @@ struct VerificSvaImporter
 			fsm.getFirstAcceptReject(accept_p, reject_p);
 	}
 
+	bool eventually_property(Net *&net, SigBit &trig)
+	{
+		if (clocking.cond_net != nullptr)
+			trig = importer->net_map_at(clocking.cond_net);
+		else
+			trig = State::S1;
+
+		Instance *inst = net_to_ast_driver(net);
+
+		if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY)
+		{
+			if (mode_cover || mode_trigger)
+				parser_error(inst);
+
+			net = inst->GetInput();
+			clocking.cond_net = nullptr;
+
+			return true;
+		}
+
+		if (inst->Type() == PRIM_SVA_OVERLAPPED_IMPLICATION ||
+				inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+		{
+			Net *antecedent_net = inst->GetInput1();
+			Net *consequent_net = inst->GetInput2();
+
+			Instance *consequent_inst = net_to_ast_driver(consequent_net);
+
+			if (consequent_inst->Type() != PRIM_SVA_S_EVENTUALLY && consequent_inst->Type() != PRIM_SVA_EVENTUALLY) {
+				return false;
+			}
+
+			if (mode_cover || mode_trigger)
+				parser_error(consequent_inst);
+
+			int node;
+
+			log_dump(trig);
+			SvaFsm antecedent_fsm(clocking, trig);
+			node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
+			if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
+				int next_node = antecedent_fsm.createNode();
+				antecedent_fsm.createEdge(node, next_node);
+				node = next_node;
+			}
+			antecedent_fsm.createLink(node, antecedent_fsm.acceptNode);
+
+			trig = antecedent_fsm.getAccept();
+			net = consequent_inst->GetInput();
+			clocking.cond_net = nullptr;
+
+			if (verific_verbose) {
+				log("    Eventually Antecedent FSM:\n");
+				antecedent_fsm.dump();
+				log_dump(trig);
+			}
+
+			return true;
+		}
+
+		return false;
+	}
+
 	void parse_property(Net *net, SigBit *accept_p, SigBit *reject_p)
 	{
 		Instance *inst = net_to_ast_driver(net);
@@ -1620,10 +1682,48 @@ struct VerificSvaImporter
 			}
 			else
 			{
-				if (mode_assert || mode_assume) {
-					parse_property(clocking.body_net, nullptr, &reject_bit);
-				} else {
-					parse_property(clocking.body_net, &accept_bit, nullptr);
+				Net *net = clocking.body_net;
+				SigBit trig;
+
+				if (eventually_property(net, trig))
+				{
+					SigBit sig_a, sig_en = trig;
+					parse_property(net, &sig_a, nullptr);
+
+					log_dump(trig, sig_a, sig_en);
+
+					// add final FF stage
+
+					SigBit sig_a_q, sig_en_q;
+
+					if (clocking.body_net == nullptr) {
+						sig_a_q = sig_a;
+						sig_en_q = sig_en;
+					} else {
+						sig_a_q = module->addWire(NEW_ID);
+						sig_en_q = module->addWire(NEW_ID);
+						clocking.addDff(NEW_ID, sig_a, sig_a_q, State::S0);
+						clocking.addDff(NEW_ID, sig_en, sig_en_q, State::S0);
+					}
+
+					// generate fair/live cell
+
+					RTLIL::Cell *c = nullptr;
+
+					if (mode_assert) c = module->addLive(root_name, sig_a_q, sig_en_q);
+					if (mode_assume) c = module->addFair(root_name, sig_a_q, sig_en_q);
+
+					importer->import_attributes(c->attributes, root);
+
+					return;
+				}
+				else
+				{
+					if (mode_assert || mode_assume) {
+						parse_property(net, nullptr, &reject_bit);
+					} else {
+						parse_property(net, &accept_bit, nullptr);
+					}
 				}
 			}
 

From 8b92ddb9d2635c30636b17ff3d24bc09a44b8551 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 29 Jun 2018 19:24:58 +0200
Subject: [PATCH 45/45] Fix verific eventually handling

Signed-off-by: Clifford Wolf <clifford@clifford.at>
---
 frontends/verific/verificsva.cc | 11 +++++------
 1 file changed, 5 insertions(+), 6 deletions(-)

diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc
index 9312fd6e6..8e985c3a6 100644
--- a/frontends/verific/verificsva.cc
+++ b/frontends/verific/verificsva.cc
@@ -1488,13 +1488,16 @@ struct VerificSvaImporter
 
 	bool eventually_property(Net *&net, SigBit &trig)
 	{
+		Instance *inst = net_to_ast_driver(net);
+
+		if (inst == nullptr)
+			return false;
+
 		if (clocking.cond_net != nullptr)
 			trig = importer->net_map_at(clocking.cond_net);
 		else
 			trig = State::S1;
 
-		Instance *inst = net_to_ast_driver(net);
-
 		if (inst->Type() == PRIM_SVA_S_EVENTUALLY || inst->Type() == PRIM_SVA_EVENTUALLY)
 		{
 			if (mode_cover || mode_trigger)
@@ -1523,7 +1526,6 @@ struct VerificSvaImporter
 
 			int node;
 
-			log_dump(trig);
 			SvaFsm antecedent_fsm(clocking, trig);
 			node = parse_sequence(antecedent_fsm, antecedent_fsm.createStartNode(), antecedent_net);
 			if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION) {
@@ -1540,7 +1542,6 @@ struct VerificSvaImporter
 			if (verific_verbose) {
 				log("    Eventually Antecedent FSM:\n");
 				antecedent_fsm.dump();
-				log_dump(trig);
 			}
 
 			return true;
@@ -1690,8 +1691,6 @@ struct VerificSvaImporter
 					SigBit sig_a, sig_en = trig;
 					parse_property(net, &sig_a, nullptr);
 
-					log_dump(trig, sig_a, sig_en);
-
 					// add final FF stage
 
 					SigBit sig_a_q, sig_en_q;