From 943389cdd50e8c77d76f64ba9abffa5190e5106a Mon Sep 17 00:00:00 2001
From: C-Elegans <mtnolan2640@gmail.com>
Date: Sun, 15 Jan 2017 09:23:04 -0500
Subject: [PATCH 01/28] Fix issue #269, optimize signed compare with 0

add opt_compare pass and add it to opt
for a < 0:
    if a is signed, replace with a[max_bit-1]
for a >= 0:
    if a is signed, replace with ~a[max_bit-1]
---
 passes/opt/Makefile.inc   |  1 +
 passes/opt/opt.cc         |  2 +
 passes/opt/opt_compare.cc | 78 +++++++++++++++++++++++++++++++++++++++
 3 files changed, 81 insertions(+)
 create mode 100644 passes/opt/opt_compare.cc

diff --git a/passes/opt/Makefile.inc b/passes/opt/Makefile.inc
index a8b1537bb..a15c4184d 100644
--- a/passes/opt/Makefile.inc
+++ b/passes/opt/Makefile.inc
@@ -6,6 +6,7 @@ OBJS += passes/opt/opt_reduce.o
 OBJS += passes/opt/opt_rmdff.o
 OBJS += passes/opt/opt_clean.o
 OBJS += passes/opt/opt_expr.o
+OBJS += passes/opt/opt_compare.o
 
 ifneq ($(SMALL),1)
 OBJS += passes/opt/share.o
diff --git a/passes/opt/opt.cc b/passes/opt/opt.cc
index 021c1a03f..b689be480 100644
--- a/passes/opt/opt.cc
+++ b/passes/opt/opt.cc
@@ -128,6 +128,7 @@ struct OptPass : public Pass {
 		{
 			while (1) {
 				Pass::call(design, "opt_expr" + opt_expr_args);
+				Pass::call(design, "opt_compare");
 				Pass::call(design, "opt_merge" + opt_merge_args);
 				design->scratchpad_unset("opt.did_something");
 				Pass::call(design, "opt_rmdff" + opt_rmdff_args);
@@ -141,6 +142,7 @@ struct OptPass : public Pass {
 		else
 		{
 			Pass::call(design, "opt_expr" + opt_expr_args);
+			Pass::call(design, "opt_compare");
 			Pass::call(design, "opt_merge -nomux" + opt_merge_args);
 			while (1) {
 				design->scratchpad_unset("opt.did_something");
diff --git a/passes/opt/opt_compare.cc b/passes/opt/opt_compare.cc
new file mode 100644
index 000000000..15b547e6f
--- /dev/null
+++ b/passes/opt/opt_compare.cc
@@ -0,0 +1,78 @@
+#include "kernel/yosys.h"
+#include "kernel/sigtools.h"
+#include "kernel/utils.h"
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+void replace_le_cell(Cell* cell, Module* module){
+	RTLIL::SigSpec a = cell->getPort("\\A");
+	RTLIL::SigSpec b = cell->getPort("\\B");
+	RTLIL::SigSpec y(RTLIL::State::S0, cell->parameters["\\Y_WIDTH"].as_int());
+	if(b.is_fully_const() && b.is_fully_zero() ){ 
+		if(cell->parameters["\\A_SIGNED"].as_bool()){
+			// a < 0, can be replaced with a[MAX_BIT]
+			log("Found x < 0 (signed), replacing with the last bit\n");
+			int a_width = cell->parameters["\\A_WIDTH"].as_int();
+			if(a_width > 0){
+				y[0] = a[a_width-1];
+				module->connect(cell->getPort("\\Y"), y);
+				module->remove(cell);
+			}
+		}
+	} 
+}
+void replace_ge_cell(Cell* cell, Module* module){
+	RTLIL::SigSpec a = cell->getPort("\\A");
+	RTLIL::SigSpec b = cell->getPort("\\B");
+	RTLIL::SigSpec y = cell->getPort("\\Y");
+	if(b.is_fully_const() && b.is_fully_zero()){
+		if(cell->parameters["\\A_SIGNED"].as_bool()){
+			log("Found x >= 0 (signed), optimizing\n");
+			RTLIL::SigSpec a_prime(RTLIL::State::S0, cell->parameters["\\Y_WIDTH"].as_int());
+			int a_width = cell->parameters["\\A_WIDTH"].as_int();
+			if(a_width > 0){
+				a_prime[0] = a[a_width-1];
+				module->remove(cell);
+				module->addNot("$not", a_prime, y,false);
+			}
+		}
+	}
+}
+void optimize_compares(Design* design, Module* module){
+	log_header(design, "Executing OPT_COMPARE pass.\n");
+	log_push();
+	TopoSort<RTLIL::Cell*, RTLIL::IdString::compare_ptr_by_name<RTLIL::Cell>> cells;
+	for(auto cell: module->cells())
+		if(design->selected(module,cell) && cell->type[0] == '$'){
+			cells.node(cell);
+		}
+	cells.sort();
+	for (auto cell: cells.sorted){
+		if (cell->type == "$lt"){
+			replace_le_cell(cell,module);
+		}
+		else if(cell->type == "$ge"){
+			replace_ge_cell(cell,module);
+		}
+	}
+
+}
+struct OptCompare : public Pass {
+	OptCompare() : Pass("opt_compare") {}
+	virtual void execute(vector<string>, Design* design){
+		for(auto module: design->selected_modules())
+			optimize_compares(design,module);
+	}
+	virtual void help() {
+		log("\n");
+		log("opt_compare\n");
+		log("\n");
+		log("This pass optimizes some signed compares with 0.\n");
+		log("In particular, it replaces a < 0 with the msb of a,\n");
+		log("and a >= 0 with the inverted msb of a.\n");
+		log("\n");
+
+	}
+} OptCompare;
+
+
+PRIVATE_NAMESPACE_END

From 6781543244105c880eb847dc59d1d801b10bdc4f Mon Sep 17 00:00:00 2001
From: Austin Seipp <aseipp@pobox.com>
Date: Sun, 15 Jan 2017 16:39:12 -0600
Subject: [PATCH 02/28] passes/hierarchy: delete some dead code

Signed-off-by: Austin Seipp <aseipp@pobox.com>
---
 passes/hierarchy/hierarchy.cc | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index 337af7fd7..f1c4a1d3b 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -175,16 +175,12 @@ bool expand_module(RTLIL::Design *design, RTLIL::Module *module, bool flag_check
 			{
 				filename = dir + "/" + RTLIL::unescape_id(cell->type) + ".v";
 				if (check_file_exists(filename)) {
-					std::vector<std::string> args;
-					args.push_back(filename);
 					Frontend::frontend_call(design, NULL, filename, "verilog");
 					goto loaded_module;
 				}
 
 				filename = dir + "/" + RTLIL::unescape_id(cell->type) + ".il";
 				if (check_file_exists(filename)) {
-					std::vector<std::string> args;
-					args.push_back(filename);
 					Frontend::frontend_call(design, NULL, filename, "ilang");
 					goto loaded_module;
 				}

From 84f9cd0025b080c7b1fc2dc86aaacc08a8f88805 Mon Sep 17 00:00:00 2001
From: C-Elegans <mtnolan2640@gmail.com>
Date: Mon, 16 Jan 2017 10:16:03 -0500
Subject: [PATCH 03/28] Optimize compares to powers of 2 Remove opt_compare and
 put comparison pass in opt_expr

assuming a [7:0] is unsigned
a >= (1<<x) becomes |a[7:x]
a <  (1<<x) becomes !a[7:x]

Additionally:
a >= 0 becomes constant true,
a < 0 becomes constant false

delete opt_compare.cc
revert opt.cc to commit b7cfb7dbd (remove opt_compare step)
---
 passes/opt/Makefile.inc   |  1 -
 passes/opt/opt.cc         |  2 -
 passes/opt/opt_compare.cc | 78 ---------------------------------------
 passes/opt/opt_expr.cc    | 61 ++++++++++++++++++++++++++++++
 4 files changed, 61 insertions(+), 81 deletions(-)
 delete mode 100644 passes/opt/opt_compare.cc

diff --git a/passes/opt/Makefile.inc b/passes/opt/Makefile.inc
index a15c4184d..a8b1537bb 100644
--- a/passes/opt/Makefile.inc
+++ b/passes/opt/Makefile.inc
@@ -6,7 +6,6 @@ OBJS += passes/opt/opt_reduce.o
 OBJS += passes/opt/opt_rmdff.o
 OBJS += passes/opt/opt_clean.o
 OBJS += passes/opt/opt_expr.o
-OBJS += passes/opt/opt_compare.o
 
 ifneq ($(SMALL),1)
 OBJS += passes/opt/share.o
diff --git a/passes/opt/opt.cc b/passes/opt/opt.cc
index b689be480..021c1a03f 100644
--- a/passes/opt/opt.cc
+++ b/passes/opt/opt.cc
@@ -128,7 +128,6 @@ struct OptPass : public Pass {
 		{
 			while (1) {
 				Pass::call(design, "opt_expr" + opt_expr_args);
-				Pass::call(design, "opt_compare");
 				Pass::call(design, "opt_merge" + opt_merge_args);
 				design->scratchpad_unset("opt.did_something");
 				Pass::call(design, "opt_rmdff" + opt_rmdff_args);
@@ -142,7 +141,6 @@ struct OptPass : public Pass {
 		else
 		{
 			Pass::call(design, "opt_expr" + opt_expr_args);
-			Pass::call(design, "opt_compare");
 			Pass::call(design, "opt_merge -nomux" + opt_merge_args);
 			while (1) {
 				design->scratchpad_unset("opt.did_something");
diff --git a/passes/opt/opt_compare.cc b/passes/opt/opt_compare.cc
deleted file mode 100644
index 15b547e6f..000000000
--- a/passes/opt/opt_compare.cc
+++ /dev/null
@@ -1,78 +0,0 @@
-#include "kernel/yosys.h"
-#include "kernel/sigtools.h"
-#include "kernel/utils.h"
-USING_YOSYS_NAMESPACE
-PRIVATE_NAMESPACE_BEGIN
-void replace_le_cell(Cell* cell, Module* module){
-	RTLIL::SigSpec a = cell->getPort("\\A");
-	RTLIL::SigSpec b = cell->getPort("\\B");
-	RTLIL::SigSpec y(RTLIL::State::S0, cell->parameters["\\Y_WIDTH"].as_int());
-	if(b.is_fully_const() && b.is_fully_zero() ){ 
-		if(cell->parameters["\\A_SIGNED"].as_bool()){
-			// a < 0, can be replaced with a[MAX_BIT]
-			log("Found x < 0 (signed), replacing with the last bit\n");
-			int a_width = cell->parameters["\\A_WIDTH"].as_int();
-			if(a_width > 0){
-				y[0] = a[a_width-1];
-				module->connect(cell->getPort("\\Y"), y);
-				module->remove(cell);
-			}
-		}
-	} 
-}
-void replace_ge_cell(Cell* cell, Module* module){
-	RTLIL::SigSpec a = cell->getPort("\\A");
-	RTLIL::SigSpec b = cell->getPort("\\B");
-	RTLIL::SigSpec y = cell->getPort("\\Y");
-	if(b.is_fully_const() && b.is_fully_zero()){
-		if(cell->parameters["\\A_SIGNED"].as_bool()){
-			log("Found x >= 0 (signed), optimizing\n");
-			RTLIL::SigSpec a_prime(RTLIL::State::S0, cell->parameters["\\Y_WIDTH"].as_int());
-			int a_width = cell->parameters["\\A_WIDTH"].as_int();
-			if(a_width > 0){
-				a_prime[0] = a[a_width-1];
-				module->remove(cell);
-				module->addNot("$not", a_prime, y,false);
-			}
-		}
-	}
-}
-void optimize_compares(Design* design, Module* module){
-	log_header(design, "Executing OPT_COMPARE pass.\n");
-	log_push();
-	TopoSort<RTLIL::Cell*, RTLIL::IdString::compare_ptr_by_name<RTLIL::Cell>> cells;
-	for(auto cell: module->cells())
-		if(design->selected(module,cell) && cell->type[0] == '$'){
-			cells.node(cell);
-		}
-	cells.sort();
-	for (auto cell: cells.sorted){
-		if (cell->type == "$lt"){
-			replace_le_cell(cell,module);
-		}
-		else if(cell->type == "$ge"){
-			replace_ge_cell(cell,module);
-		}
-	}
-
-}
-struct OptCompare : public Pass {
-	OptCompare() : Pass("opt_compare") {}
-	virtual void execute(vector<string>, Design* design){
-		for(auto module: design->selected_modules())
-			optimize_compares(design,module);
-	}
-	virtual void help() {
-		log("\n");
-		log("opt_compare\n");
-		log("\n");
-		log("This pass optimizes some signed compares with 0.\n");
-		log("In particular, it replaces a < 0 with the msb of a,\n");
-		log("and a >= 0 with the inverted msb of a.\n");
-		log("\n");
-
-	}
-} OptCompare;
-
-
-PRIVATE_NAMESPACE_END
diff --git a/passes/opt/opt_expr.cc b/passes/opt/opt_expr.cc
index b62eae285..b629ed326 100644
--- a/passes/opt/opt_expr.cc
+++ b/passes/opt/opt_expr.cc
@@ -1166,6 +1166,67 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 					}
 			}
 		}
+        //replace a <0  or a >=0 with the top bit of a
+        if(do_fine && (cell->type == "$lt" || cell->type == "$ge"))
+        {
+            bool is_lt = cell->type == "$lt" ? 1 : 0;
+            RTLIL::SigSpec a = cell->getPort("\\A");
+            RTLIL::SigSpec b = cell->getPort("\\B");
+            int a_width = cell->parameters["\\A_WIDTH"].as_int();
+            //replace a(signed) < 0 with the high bit of a
+            if(b.is_fully_const() && b.is_fully_zero() && cell->parameters["\\A_SIGNED"].as_bool() == true){
+                RTLIL::SigSpec a_prime(RTLIL::State::S0, cell->parameters["\\Y_WIDTH"].as_int());
+                a_prime[0] = a[a_width-1];
+                if(is_lt){
+                    log("Optimizing a < 0 with a[%d]\n",a_width - 1);
+                    module->connect(cell->getPort("\\Y"), a_prime);
+                    module->remove(cell);
+                }
+                else{
+                    log("Optimizing a >= 0 with ~a[%d]\n",a_width - 1);
+                    module->addNot("$not", a_prime, cell->getPort("\\Y"));
+                    module->remove(cell);
+                } 
+                did_something = true;
+                goto next_cell;
+            }
+            else if(b.is_fully_const() && b.is_fully_def() && cell->parameters["\\A_SIGNED"].as_bool() == false){
+                int b_value = b.as_int(false);
+                if(b_value == 0){
+                    RTLIL::SigSpec a_prime(RTLIL::State::S0,1);
+                    if(is_lt){
+                        log("replacing a(unsigned) < 0 with constant false\n");
+                        a_prime[0] = RTLIL::State::S0;
+                    }
+                    else{
+                        log("replacing a(unsigned) >= 0 with constant true\n");
+                        a_prime[0] = RTLIL::State::S1;
+                    }
+                    module->connect(cell->getPort("\\Y"), a_prime);
+                    module->remove(cell);
+                    did_something = true;
+                    goto next_cell;
+                }
+                else if((b_value & -b_value) == b_value){ //if b has only 1 bit set
+                    int bit_set = ceil_log2(b_value); 
+                    RTLIL::SigSpec a_prime(RTLIL::State::S0,a_width-bit_set);
+                    for(int i = bit_set; i < a_width; i++){
+                        a_prime[i-bit_set] = a[i];
+                    }
+                    if(is_lt){
+                        log("replacing a < %d with !a[%d:%d]\n",b_value,a_width-1,bit_set);
+                        module->addLogicNot("$logic_not", a_prime,cell->getPort("\\Y"));
+                    }
+                    else{
+                        log("replacing a >= %d with |a[%d:%d]\n",b_value,a_width-1,bit_set);
+                        module->addReduceOr("$reduce_or", a_prime,cell->getPort("\\Y")); 
+                    }
+                    module->remove(cell);
+                    did_something = true;
+                    goto next_cell;
+                }
+            }
+        }
 
 	next_cell:;
 #undef ACTION_DO

From fea528280b9e598ae13178c9ce4ac16e569c46a8 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 17 Jan 2017 17:33:52 +0100
Subject: [PATCH 04/28] Add "enum" and "typedef" lexer support

---
 frontends/verilog/verilog_lexer.l  | 3 +++
 frontends/verilog/verilog_parser.y | 2 +-
 2 files changed, 4 insertions(+), 1 deletion(-)

diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index 405aeb975..c22fdf39c 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -192,6 +192,9 @@ YOSYS_NAMESPACE_END
 "genvar"  { return TOK_GENVAR; }
 "real"    { return TOK_REAL; }
 
+"enum"    { SV_KEYWORD(TOK_ENUM); }
+"typedef" { SV_KEYWORD(TOK_TYPEDEF); }
+
 [0-9][0-9_]* {
 	frontend_verilog_yylval.string = new std::string(yytext);
 	return TOK_CONST;
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 607c48a81..ba47bf2d3 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -114,7 +114,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 %token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE
 %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED
 %token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME
-%token TOK_RESTRICT TOK_PROPERTY
+%token TOK_RESTRICT TOK_PROPERTY TOK_ENUM TOK_TYPEDEF
 
 %type <ast> range range_or_multirange  non_opt_range non_opt_multirange range_or_signed_int
 %type <ast> wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list

From 2fa0fd4a370cddab6bcbd645af5300e14b60a697 Mon Sep 17 00:00:00 2001
From: C-Elegans <mtnolan2640@gmail.com>
Date: Sat, 21 Jan 2017 12:58:26 -0500
Subject: [PATCH 05/28] Do not use b.as_int() in calculation of bit set

---
 passes/opt/opt_expr.cc | 37 +++++++++++++++++++++++++++++--------
 1 file changed, 29 insertions(+), 8 deletions(-)

diff --git a/passes/opt/opt_expr.cc b/passes/opt/opt_expr.cc
index b629ed326..7574f0d74 100644
--- a/passes/opt/opt_expr.cc
+++ b/passes/opt/opt_expr.cc
@@ -258,7 +258,27 @@ bool is_one_or_minus_one(const Const &value, bool is_signed, bool &is_negative)
 
 	return last_bit_one;
 }
-
+int get_onehot_bit_index(RTLIL::SigSpec signal){
+    if(!signal.is_fully_const())
+        return -1;
+    bool bit_set = false;
+    int bit_index = 0;
+    int i = 0;
+    for(auto bit: signal.bits()){
+        if(bit == RTLIL::State::S1){
+            if(bit_set)
+                return -1;
+            bit_index = i;
+            bit_set = true;
+        }
+        i++;
+    }
+    if(bit_set){
+        return bit_index;
+    }else{
+        return -1;
+    }
+}
 void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool consume_x, bool mux_undef, bool mux_bool, bool do_fine, bool keepdc, bool clkinv)
 {
 	if (!design->selected(module))
@@ -1190,9 +1210,9 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
                 did_something = true;
                 goto next_cell;
             }
-            else if(b.is_fully_const() && b.is_fully_def() && cell->parameters["\\A_SIGNED"].as_bool() == false){
-                int b_value = b.as_int(false);
-                if(b_value == 0){
+            else if(b.is_fully_const() && b.is_fully_def() && cell->parameters["\\A_SIGNED"].as_bool() == false){           
+                int b_bit_set = get_onehot_bit_index(b);
+                if(b.is_fully_zero()){
                     RTLIL::SigSpec a_prime(RTLIL::State::S0,1);
                     if(is_lt){
                         log("replacing a(unsigned) < 0 with constant false\n");
@@ -1207,18 +1227,19 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
                     did_something = true;
                     goto next_cell;
                 }
-                else if((b_value & -b_value) == b_value){ //if b has only 1 bit set
-                    int bit_set = ceil_log2(b_value); 
+               
+                else if(b_bit_set >= 0){ //if b has only 1 bit set
+                    int bit_set = b_bit_set;
                     RTLIL::SigSpec a_prime(RTLIL::State::S0,a_width-bit_set);
                     for(int i = bit_set; i < a_width; i++){
                         a_prime[i-bit_set] = a[i];
                     }
                     if(is_lt){
-                        log("replacing a < %d with !a[%d:%d]\n",b_value,a_width-1,bit_set);
+                        log("replacing a < %d with !a[%d:%d]\n",b.as_int(false),a_width-1,bit_set);
                         module->addLogicNot("$logic_not", a_prime,cell->getPort("\\Y"));
                     }
                     else{
-                        log("replacing a >= %d with |a[%d:%d]\n",b_value,a_width-1,bit_set);
+                        log("replacing a >= %d with |a[%d:%d]\n",b.as_int(false),a_width-1,bit_set);
                         module->addReduceOr("$reduce_or", a_prime,cell->getPort("\\Y")); 
                     }
                     module->remove(cell);

From b54972c1120fa6c5f4dc85d58178fb1211547691 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 25 Jan 2017 17:00:59 +0100
Subject: [PATCH 06/28] Fix RTLIL::Memory::start_offset initialization

---
 kernel/rtlil.cc | 1 +
 1 file changed, 1 insertion(+)

diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 40ad8ca13..365bfd9f8 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -2050,6 +2050,7 @@ RTLIL::Memory::Memory()
 	hashidx_ = hashidx_count;
 
 	width = 1;
+	start_offset = 0;
 	size = 0;
 }
 

From 49b816048833d25921e45bfb248643acbf23b8de Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 26 Jan 2017 09:01:26 +0100
Subject: [PATCH 07/28] Add warnings for quickly growing FSM table size in
 fsm_expand

---
 passes/fsm/fsm_expand.cc | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/passes/fsm/fsm_expand.cc b/passes/fsm/fsm_expand.cc
index e7b9dcf90..0a2166b99 100644
--- a/passes/fsm/fsm_expand.cc
+++ b/passes/fsm/fsm_expand.cc
@@ -173,6 +173,16 @@ struct FsmExpand
 		new_ctrl_out.append(output_sig);
 		fsm_cell->setPort("\\CTRL_OUT", new_ctrl_out);
 
+		if (GetSize(input_sig) > 10)
+			log_warning("Cell %s.%s (%s) has %d input bits, merging into FSM %s.%s might be problematic.\n",
+					log_id(cell->module), log_id(cell), log_id(cell->type),
+					GetSize(input_sig), log_id(fsm_cell->module), log_id(fsm_cell));
+
+		if (GetSize(fsm_data.transition_table) > 10000)
+			log_warning("Transition table for FSM %s.%s already has %d rows, merging more cells "
+					"into this FSM might be problematic.\n", log_id(fsm_cell->module), log_id(fsm_cell),
+					GetSize(fsm_data.transition_table));
+
 		std::vector<FsmData::transition_t> new_transition_table;
 		for (auto &tr : fsm_data.transition_table) {
 			for (int i = 0; i < (1 << input_sig.size()); i++) {

From 45e10c1c892a7f3082beb9a15aeaaada52267742 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 26 Jan 2017 09:19:28 +0100
Subject: [PATCH 08/28] Be more conservative with merging large cells into FSMs

---
 passes/fsm/fsm_expand.cc | 20 +++++++++++++++++---
 1 file changed, 17 insertions(+), 3 deletions(-)

diff --git a/passes/fsm/fsm_expand.cc b/passes/fsm/fsm_expand.cc
index 0a2166b99..2c344a1c1 100644
--- a/passes/fsm/fsm_expand.cc
+++ b/passes/fsm/fsm_expand.cc
@@ -54,13 +54,27 @@ struct FsmExpand
 			if (cell->getPort("\\A").size() < 2)
 				return true;
 
+		int in_bits = 0;
 		RTLIL::SigSpec new_signals;
-		if (cell->hasPort("\\A"))
+
+		if (cell->hasPort("\\A")) {
+			in_bits += GetSize(cell->getPort("\\A"));
 			new_signals.append(assign_map(cell->getPort("\\A")));
-		if (cell->hasPort("\\B"))
+		}
+
+		if (cell->hasPort("\\B")) {
+			in_bits += GetSize(cell->getPort("\\B"));
 			new_signals.append(assign_map(cell->getPort("\\B")));
-		if (cell->hasPort("\\S"))
+		}
+
+		if (cell->hasPort("\\S")) {
+			in_bits += GetSize(cell->getPort("\\S"));
 			new_signals.append(assign_map(cell->getPort("\\S")));
+		}
+
+		if (in_bits > 8)
+			return false;
+
 		if (cell->hasPort("\\Y"))
 			new_signals.append(assign_map(cell->getPort("\\Y")));
 

From e54c355b417eb7fa19421176792d01cb7a62d4cb Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 28 Jan 2017 15:14:56 +0100
Subject: [PATCH 09/28] Add "yosys-smtbmc --aig-noheader" and AIGER mem init
 support

---
 backends/smt2/smtbmc.py | 39 +++++++++++++++++++++++++++++++++------
 backends/smt2/smtio.py  | 24 ++++++++++++++++++++++--
 2 files changed, 55 insertions(+), 8 deletions(-)

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index ecee6795e..ab952786e 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -30,6 +30,7 @@ append_steps = 0
 vcdfile = None
 cexfile = None
 aigprefix = None
+aigheader = True
 vlogtbfile = None
 inconstr = list()
 outconstr = None
@@ -73,6 +74,10 @@ yosys-smtbmc [options] <yosys_smt2_output>
         and AIGER witness file. The file names are <prefix>.aim for
         the map file and <prefix>.aiw for the witness file.
 
+    --aig-noheader
+        the AIGER witness file does not include the status and
+        properties lines.
+
     --noinfo
         only run the core proof, do not collect and print any
         additional information (e.g. which assert failed)
@@ -111,7 +116,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
 
 try:
     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igm:", so.longopts +
-            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=",
+            ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader",
              "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo", "append="])
 except:
     usage()
@@ -141,6 +146,8 @@ for o, a in opts:
         cexfile = a
     elif o == "--aig":
         aigprefix = a
+    elif o == "--aig-noheader":
+        aigheader = False
     elif o == "--dump-vcd":
         vcdfile = a
     elif o == "--dump-vlogtb":
@@ -411,6 +418,9 @@ if aigprefix is not None:
         got_ffinit = False
         step = 0
 
+        if not aigheader:
+            got_state = True
+
         for entry in f.read().splitlines():
             if len(entry) == 0 or entry[0] in "bcjfu.":
                 continue
@@ -458,13 +468,30 @@ if aigprefix is not None:
                     bitidx = init_map[i][1]
 
                     path = smt.get_path(topmod, name)
-                    width = smt.net_width(topmod, path)
+
+                    if not smt.net_exists(topmod, path):
+                        match = re.match(r"(.*)\[(\d+)\]$", path[-1])
+                        if match:
+                            path[-1] = match.group(1)
+                            addr = int(match.group(2))
+
+                        if not match or not smt.mem_exists(topmod, path):
+                            print_msg("Ignoring init value for unknown net: %s" % (name))
+                            continue
+
+                        meminfo = smt.mem_info(topmod, path)
+                        smtexpr = "(select [%s] #b%s)" % (".".join(path), bin(addr)[2:].zfill(meminfo[0]))
+                        width = meminfo[1]
+
+                    else:
+                        smtexpr = "[%s]" % name
+                        width = smt.net_width(topmod, path)
 
                     if width == 1:
                         assert bitidx == 0
-                        smtexpr = "(= [%s] %s)" % (name, "true" if value else "false")
+                        smtexpr = "(= %s %s)" % (smtexpr, "true" if value else "false")
                     else:
-                        smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value)
+                        smtexpr = "(= ((_ extract %d %d) %s) #b%d)" % (bitidx, bitidx, smtexpr, value)
 
                     constr_assumes[0].append((cexfile, smtexpr))
 
@@ -569,7 +596,7 @@ def write_vlogtb_trace(steps_start, steps_stop, index):
 
         mems = sorted(smt.hiermems(topmod))
         for mempath in mems:
-            abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath)
+            abits, width, ports = smt.mem_info(topmod, mempath)
             mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath)
 
             addr_expr_list = list()
@@ -630,7 +657,7 @@ def write_constr_trace(steps_start, steps_stop, index):
 
         mems = sorted(smt.hiermems(topmod))
         for mempath in mems:
-            abits, width, ports = smt.mem_info(topmod, "s%d" % steps_start, mempath)
+            abits, width, ports = smt.mem_info(topmod, mempath)
             mem = smt.mem_expr(topmod, "s%d" % steps_start, mempath)
 
             addr_expr_list = list()
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 497b72db8..3946c3423 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -567,6 +567,26 @@ class SmtIo:
         assert net_path[-1] in self.modinfo[mod].wsize
         return self.modinfo[mod].wsize[net_path[-1]]
 
+    def net_exists(self, mod, net_path):
+        for i in range(len(net_path)-1):
+            if mod not in self.modinfo: return False
+            if net_path[i] not in self.modinfo[mod].cells: return False
+            mod = self.modinfo[mod].cells[net_path[i]]
+
+        if mod not in self.modinfo: return False
+        if net_path[-1] not in self.modinfo[mod].wsize: return False
+        return True
+
+    def mem_exists(self, mod, mem_path):
+        for i in range(len(mem_path)-1):
+            if mod not in self.modinfo: return False
+            if mem_path[i] not in self.modinfo[mod].cells: return False
+            mod = self.modinfo[mod].cells[mem_path[i]]
+
+        if mod not in self.modinfo: return False
+        if mem_path[-1] not in self.modinfo[mod].memories: return False
+        return True
+
     def mem_expr(self, mod, base, path, portidx=None, infomode=False):
         if len(path) == 1:
             assert mod in self.modinfo
@@ -582,8 +602,8 @@ class SmtIo:
         nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
         return self.mem_expr(nextmod, nextbase, path[1:], portidx=portidx, infomode=infomode)
 
-    def mem_info(self, mod, base, path):
-        return self.mem_expr(mod, base, path, infomode=True)
+    def mem_info(self, mod, path):
+        return self.mem_expr(mod, "", path, infomode=True)
 
     def get_net(self, mod_name, net_path, state_name):
         return self.get(self.net_expr(mod_name, state_name, net_path))

From fe29869ec5104376d7d061e82a7f7be77673e8f1 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 30 Jan 2017 10:50:38 +0100
Subject: [PATCH 10/28] Add $ff and $_FF_ support to equiv_simple

---
 passes/equiv/equiv_simple.cc | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc
index 49963ed68..270200c34 100644
--- a/passes/equiv/equiv_simple.cc
+++ b/passes/equiv/equiv_simple.cc
@@ -59,7 +59,7 @@ struct EquivSimpleWorker
 		for (auto &conn : cell->connections())
 			if (yosys_celltypes.cell_input(cell->type, conn.first))
 				for (auto bit : sigmap(conn.second)) {
-					if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_")) {
+					if (cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_", "$ff", "$_FF_")) {
 						if (!conn.first.in("\\CLK", "\\C"))
 							next_seed.insert(bit);
 					} else
@@ -329,7 +329,7 @@ struct EquivSimplePass : public Pass {
 					unproven_cells_counter, GetSize(unproven_equiv_cells), log_id(module));
 
 			for (auto cell : module->cells()) {
-				if (!ct.cell_known(cell->type) && !cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_"))
+				if (!ct.cell_known(cell->type) && !cell->type.in("$dff", "$_DFF_P_", "$_DFF_N_", "$ff", "$_FF_"))
 					continue;
 				for (auto &conn : cell->connections())
 					if (yosys_celltypes.cell_output(cell->type, conn.first))

From 18ea65ef04889e5016f007d3a034c8c49709cdb6 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 30 Jan 2017 11:38:43 +0100
Subject: [PATCH 11/28] Add "yosys-smtbmc --aig <aim_filename>:<aiw_filename>"
 support

---
 backends/smt2/smtbmc.py | 19 ++++++++++++++-----
 1 file changed, 14 insertions(+), 5 deletions(-)

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index ab952786e..10875f523 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -29,7 +29,8 @@ num_steps = 20
 append_steps = 0
 vcdfile = None
 cexfile = None
-aigprefix = None
+aimfile = None
+aiwfile = None
 aigheader = True
 vlogtbfile = None
 inconstr = list()
@@ -74,6 +75,10 @@ yosys-smtbmc [options] <yosys_smt2_output>
         and AIGER witness file. The file names are <prefix>.aim for
         the map file and <prefix>.aiw for the witness file.
 
+    --aig <aim_filename>:<aiw_filename>
+        like above, but for map files and witness files that do not
+        share a filename prefix (or use differen file extensions).
+
     --aig-noheader
         the AIGER witness file does not include the status and
         properties lines.
@@ -145,7 +150,11 @@ for o, a in opts:
     elif o == "--cex":
         cexfile = a
     elif o == "--aig":
-        aigprefix = a
+        if ":" in a:
+            aimfile, aiwfile = a.split(":")
+        else:
+            aimfile = a + ".aim"
+            aiwfile = a + ".aiw"
     elif o == "--aig-noheader":
         aigheader = False
     elif o == "--dump-vcd":
@@ -382,7 +391,7 @@ if cexfile is not None:
                 skip_steps = max(skip_steps, step)
                 num_steps = max(num_steps, step+1)
 
-if aigprefix is not None:
+if aimfile is not None:
     input_map = dict()
     init_map = dict()
     latch_map = dict()
@@ -392,7 +401,7 @@ if aigprefix is not None:
         skip_steps = 0
         num_steps = 0
 
-    with open(aigprefix + ".aim", "r") as f:
+    with open(aimfile, "r") as f:
         for entry in f.read().splitlines():
             entry = entry.split()
 
@@ -413,7 +422,7 @@ if aigprefix is not None:
 
             assert False
 
-    with open(aigprefix + ".aiw", "r") as f:
+    with open(aiwfile, "r") as f:
         got_state = False
         got_ffinit = False
         step = 0

From a94c3694d7b8a6c1a1c18aa598e63ab97d525529 Mon Sep 17 00:00:00 2001
From: C-Elegans <mtnolan2640@gmail.com>
Date: Mon, 30 Jan 2017 17:52:16 -0500
Subject: [PATCH 12/28] Refactor and generalize the comparision optimization

Generalizes the optimization to:
a < C,
a >= C,
C > a,
C <= a
---
 passes/opt/opt_expr.cc | 64 +++++++++++++++++++++++++++---------------
 1 file changed, 42 insertions(+), 22 deletions(-)

diff --git a/passes/opt/opt_expr.cc b/passes/opt/opt_expr.cc
index 7574f0d74..9d7248dc6 100644
--- a/passes/opt/opt_expr.cc
+++ b/passes/opt/opt_expr.cc
@@ -258,6 +258,8 @@ bool is_one_or_minus_one(const Const &value, bool is_signed, bool &is_negative)
 
 	return last_bit_one;
 }
+//if the signal has only one bit set, return the index of that bit.
+//otherwise return -1
 int get_onehot_bit_index(RTLIL::SigSpec signal){
     if(!signal.is_fully_const())
         return -1;
@@ -1187,32 +1189,50 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 			}
 		}
         //replace a <0  or a >=0 with the top bit of a
-        if(do_fine && (cell->type == "$lt" || cell->type == "$ge"))
+        if(do_fine && (cell->type == "$lt" || cell->type == "$ge" || cell->type == "$gt" || cell->type == "$le"))
         {
-            bool is_lt = cell->type == "$lt" ? 1 : 0;
-            RTLIL::SigSpec a = cell->getPort("\\A");
-            RTLIL::SigSpec b = cell->getPort("\\B");
-            int a_width = cell->parameters["\\A_WIDTH"].as_int();
+            bool is_lt = false; //used to decide whether the signal needs to be negated
+            RTLIL::SigSpec sigVar; //references the variable signal in the comparison
+            RTLIL::SigSpec sigConst; //references the constant signal in the comparison
+                 //note that this signal must be constant for the optimization 
+                 //to take place, but it is not checked beforehand.
+                 //If new passes are added, this signal must be checked for const-ness
+            int width; //width of the variable port
+            bool var_signed; 
+            if(cell->type == "$lt" || cell->type == "$ge"){
+                is_lt = cell->type == "$lt" ? 1 : 0;
+                sigVar = cell->getPort("\\A");
+                sigConst = cell->getPort("\\B");
+                width = cell->parameters["\\A_WIDTH"].as_int();
+                var_signed = cell->parameters["\\A_SIGNED"].as_bool();
+            }
+            if(cell->type == "$gt" || cell->type == "$le"){
+                is_lt = cell->type == "$gt" ? 1 : 0;  
+                sigVar = cell->getPort("\\B");
+                sigConst = cell->getPort("\\A");
+                width = cell->parameters["\\B_WIDTH"].as_int();
+                var_signed = cell->parameters["\\B_SIGNED"].as_bool();
+            }
             //replace a(signed) < 0 with the high bit of a
-            if(b.is_fully_const() && b.is_fully_zero() && cell->parameters["\\A_SIGNED"].as_bool() == true){
+            if(sigConst.is_fully_const() && sigConst.is_fully_zero() && var_signed == true){
                 RTLIL::SigSpec a_prime(RTLIL::State::S0, cell->parameters["\\Y_WIDTH"].as_int());
-                a_prime[0] = a[a_width-1];
+                a_prime[0] = sigVar[width-1];
                 if(is_lt){
-                    log("Optimizing a < 0 with a[%d]\n",a_width - 1);
+                    log("Optimizing a < 0 with a[%d]\n",width - 1);
                     module->connect(cell->getPort("\\Y"), a_prime);
                     module->remove(cell);
                 }
                 else{
-                    log("Optimizing a >= 0 with ~a[%d]\n",a_width - 1);
-                    module->addNot("$not", a_prime, cell->getPort("\\Y"));
+                    log("Optimizing a >= 0 with ~a[%d]\n",width - 1);
+                    module->addNot(NEW_ID, a_prime, cell->getPort("\\Y"));
                     module->remove(cell);
                 } 
                 did_something = true;
                 goto next_cell;
             }
-            else if(b.is_fully_const() && b.is_fully_def() && cell->parameters["\\A_SIGNED"].as_bool() == false){           
-                int b_bit_set = get_onehot_bit_index(b);
-                if(b.is_fully_zero()){
+            else if(sigConst.is_fully_const() && sigConst.is_fully_def() && var_signed == false){           
+                int const_bit_set = get_onehot_bit_index(sigConst);
+                if(sigConst.is_fully_zero()){
                     RTLIL::SigSpec a_prime(RTLIL::State::S0,1);
                     if(is_lt){
                         log("replacing a(unsigned) < 0 with constant false\n");
@@ -1228,19 +1248,19 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
                     goto next_cell;
                 }
                
-                else if(b_bit_set >= 0){ //if b has only 1 bit set
-                    int bit_set = b_bit_set;
-                    RTLIL::SigSpec a_prime(RTLIL::State::S0,a_width-bit_set);
-                    for(int i = bit_set; i < a_width; i++){
-                        a_prime[i-bit_set] = a[i];
+                else if(const_bit_set >= 0){ //if b has only 1 bit set
+                    int bit_set = const_bit_set;
+                    RTLIL::SigSpec a_prime(RTLIL::State::S0,width-bit_set);
+                    for(int i = bit_set; i < width; i++){
+                        a_prime[i-bit_set] = sigVar[i];
                     }
                     if(is_lt){
-                        log("replacing a < %d with !a[%d:%d]\n",b.as_int(false),a_width-1,bit_set);
-                        module->addLogicNot("$logic_not", a_prime,cell->getPort("\\Y"));
+                        log("replacing a < %d with !a[%d:%d]\n",sigConst.as_int(false),width-1,bit_set);
+                        module->addLogicNot(NEW_ID, a_prime,cell->getPort("\\Y"));
                     }
                     else{
-                        log("replacing a >= %d with |a[%d:%d]\n",b.as_int(false),a_width-1,bit_set);
-                        module->addReduceOr("$reduce_or", a_prime,cell->getPort("\\Y")); 
+                        log("replacing a >= %d with |a[%d:%d]\n",sigConst.as_int(false),width-1,bit_set);
+                        module->addReduceOr(NEW_ID, a_prime,cell->getPort("\\Y")); 
                     }
                     module->remove(cell);
                     did_something = true;

From 7481ba4750b5c65c9dc2c64ae29027f328f25bfe Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 31 Jan 2017 10:15:04 +0100
Subject: [PATCH 13/28] Improve opt_rmdff support for $dlatch cells

---
 passes/opt/opt_rmdff.cc | 26 ++++++++++++++++++++++----
 1 file changed, 22 insertions(+), 4 deletions(-)

diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index 922f086f1..00094738c 100644
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -41,9 +41,27 @@ void remove_init_attr(SigSpec sig)
 
 bool handle_dlatch(RTLIL::Module *mod, RTLIL::Cell *dlatch)
 {
-	SigSpec sig_e = dlatch->getPort("\\EN");
+	SigSpec sig_e;
+	State on_state, off_state;
 
-	if (sig_e == State::S0)
+	if (dlatch->type == "$dlatch") {
+		sig_e = assign_map(dlatch->getPort("\\EN"));
+		on_state = dlatch->getParam("\\EN_POLARITY").as_bool() ? State::S1 : State::S0;
+		off_state = dlatch->getParam("\\EN_POLARITY").as_bool() ? State::S0 : State::S1;
+	} else
+	if (dlatch->type == "$_DLATCH_P_") {
+		sig_e = assign_map(dlatch->getPort("\\E"));
+		on_state = State::S1;
+		off_state = State::S0;
+	} else
+	if (dlatch->type == "$_DLATCH_N_") {
+		sig_e = assign_map(dlatch->getPort("\\E"));
+		on_state = State::S0;
+		off_state = State::S1;
+	} else
+		log_abort();
+
+	if (sig_e == off_state)
 	{
 		RTLIL::Const val_init;
 		for (auto bit : dff_init_map(dlatch->getPort("\\Q")))
@@ -52,7 +70,7 @@ bool handle_dlatch(RTLIL::Module *mod, RTLIL::Cell *dlatch)
 		goto delete_dlatch;
 	}
 
-	if (sig_e == State::S1)
+	if (sig_e == on_state)
 	{
 		mod->connect(dlatch->getPort("\\Q"), dlatch->getPort("\\D"));
 		goto delete_dlatch;
@@ -268,7 +286,7 @@ struct OptRmdffPass : public Pass {
 						"$ff", "$dff", "$adff"))
 					dff_list.push_back(cell->name);
 
-				if (cell->type == "$dlatch")
+				if (cell->type.in("$dlatch", "$_DLATCH_P_", "$_DLATCH_N_"))
 					dlatch_list.push_back(cell->name);
 			}
 

From ffbe8d41f35f36cb08defdc4260f465e0a19de65 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Tue, 31 Jan 2017 16:20:56 +0100
Subject: [PATCH 14/28] Fix indenting and log messages in code merged from
 opt_compare_pr

---
 passes/opt/opt_expr.cc | 222 ++++++++++++++++++++++-------------------
 1 file changed, 120 insertions(+), 102 deletions(-)

diff --git a/passes/opt/opt_expr.cc b/passes/opt/opt_expr.cc
index 9d7248dc6..b3f2e87ed 100644
--- a/passes/opt/opt_expr.cc
+++ b/passes/opt/opt_expr.cc
@@ -258,29 +258,30 @@ bool is_one_or_minus_one(const Const &value, bool is_signed, bool &is_negative)
 
 	return last_bit_one;
 }
-//if the signal has only one bit set, return the index of that bit.
-//otherwise return -1
-int get_onehot_bit_index(RTLIL::SigSpec signal){
-    if(!signal.is_fully_const())
-        return -1;
-    bool bit_set = false;
-    int bit_index = 0;
-    int i = 0;
-    for(auto bit: signal.bits()){
-        if(bit == RTLIL::State::S1){
-            if(bit_set)
-                return -1;
-            bit_index = i;
-            bit_set = true;
-        }
-        i++;
-    }
-    if(bit_set){
-        return bit_index;
-    }else{
-        return -1;
-    }
+
+// if the signal has only one bit set, return the index of that bit.
+// otherwise return -1
+int get_onehot_bit_index(RTLIL::SigSpec signal)
+{
+	int bit_index = -1;
+
+	for (int i = 0; i < GetSize(signal); i++)
+	{
+		if (signal[i] == RTLIL::State::S0)
+			continue;
+
+		if (signal[i] != RTLIL::State::S1)
+			return -1;
+
+		if (bit_index != -1)
+			return -1;
+
+		bit_index = i;
+	}
+
+	return bit_index;
 }
+
 void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool consume_x, bool mux_undef, bool mux_bool, bool do_fine, bool keepdc, bool clkinv)
 {
 	if (!design->selected(module))
@@ -1188,86 +1189,103 @@ void replace_const_cells(RTLIL::Design *design, RTLIL::Module *module, bool cons
 					}
 			}
 		}
-        //replace a <0  or a >=0 with the top bit of a
-        if(do_fine && (cell->type == "$lt" || cell->type == "$ge" || cell->type == "$gt" || cell->type == "$le"))
-        {
-            bool is_lt = false; //used to decide whether the signal needs to be negated
-            RTLIL::SigSpec sigVar; //references the variable signal in the comparison
-            RTLIL::SigSpec sigConst; //references the constant signal in the comparison
-                 //note that this signal must be constant for the optimization 
-                 //to take place, but it is not checked beforehand.
-                 //If new passes are added, this signal must be checked for const-ness
-            int width; //width of the variable port
-            bool var_signed; 
-            if(cell->type == "$lt" || cell->type == "$ge"){
-                is_lt = cell->type == "$lt" ? 1 : 0;
-                sigVar = cell->getPort("\\A");
-                sigConst = cell->getPort("\\B");
-                width = cell->parameters["\\A_WIDTH"].as_int();
-                var_signed = cell->parameters["\\A_SIGNED"].as_bool();
-            }
-            if(cell->type == "$gt" || cell->type == "$le"){
-                is_lt = cell->type == "$gt" ? 1 : 0;  
-                sigVar = cell->getPort("\\B");
-                sigConst = cell->getPort("\\A");
-                width = cell->parameters["\\B_WIDTH"].as_int();
-                var_signed = cell->parameters["\\B_SIGNED"].as_bool();
-            }
-            //replace a(signed) < 0 with the high bit of a
-            if(sigConst.is_fully_const() && sigConst.is_fully_zero() && var_signed == true){
-                RTLIL::SigSpec a_prime(RTLIL::State::S0, cell->parameters["\\Y_WIDTH"].as_int());
-                a_prime[0] = sigVar[width-1];
-                if(is_lt){
-                    log("Optimizing a < 0 with a[%d]\n",width - 1);
-                    module->connect(cell->getPort("\\Y"), a_prime);
-                    module->remove(cell);
-                }
-                else{
-                    log("Optimizing a >= 0 with ~a[%d]\n",width - 1);
-                    module->addNot(NEW_ID, a_prime, cell->getPort("\\Y"));
-                    module->remove(cell);
-                } 
-                did_something = true;
-                goto next_cell;
-            }
-            else if(sigConst.is_fully_const() && sigConst.is_fully_def() && var_signed == false){           
-                int const_bit_set = get_onehot_bit_index(sigConst);
-                if(sigConst.is_fully_zero()){
-                    RTLIL::SigSpec a_prime(RTLIL::State::S0,1);
-                    if(is_lt){
-                        log("replacing a(unsigned) < 0 with constant false\n");
-                        a_prime[0] = RTLIL::State::S0;
-                    }
-                    else{
-                        log("replacing a(unsigned) >= 0 with constant true\n");
-                        a_prime[0] = RTLIL::State::S1;
-                    }
-                    module->connect(cell->getPort("\\Y"), a_prime);
-                    module->remove(cell);
-                    did_something = true;
-                    goto next_cell;
-                }
-               
-                else if(const_bit_set >= 0){ //if b has only 1 bit set
-                    int bit_set = const_bit_set;
-                    RTLIL::SigSpec a_prime(RTLIL::State::S0,width-bit_set);
-                    for(int i = bit_set; i < width; i++){
-                        a_prime[i-bit_set] = sigVar[i];
-                    }
-                    if(is_lt){
-                        log("replacing a < %d with !a[%d:%d]\n",sigConst.as_int(false),width-1,bit_set);
-                        module->addLogicNot(NEW_ID, a_prime,cell->getPort("\\Y"));
-                    }
-                    else{
-                        log("replacing a >= %d with |a[%d:%d]\n",sigConst.as_int(false),width-1,bit_set);
-                        module->addReduceOr(NEW_ID, a_prime,cell->getPort("\\Y")); 
-                    }
-                    module->remove(cell);
-                    did_something = true;
-                    goto next_cell;
-                }
-            }
-        }
+
+		// replace a<0 or a>=0 with the top bit of a
+		if (do_fine && (cell->type == "$lt" || cell->type == "$ge" || cell->type == "$gt" || cell->type == "$le"))
+		{
+			//used to decide whether the signal needs to be negated
+			bool is_lt = false;
+
+			//references the variable signal in the comparison
+			RTLIL::SigSpec sigVar;
+
+			//references the constant signal in the comparison
+			RTLIL::SigSpec sigConst;
+
+			// note that this signal must be constant for the optimization 
+			// to take place, but it is not checked beforehand.
+			// If new passes are added, this signal must be checked for const-ness
+
+			//width of the variable port
+			int width;
+
+			bool var_signed;
+
+			if (cell->type == "$lt" || cell->type == "$ge") {
+				is_lt = cell->type == "$lt" ? 1 : 0;
+				sigVar = cell->getPort("\\A");
+				sigConst = cell->getPort("\\B");
+				width = cell->parameters["\\A_WIDTH"].as_int();
+				var_signed = cell->parameters["\\A_SIGNED"].as_bool();
+			} else
+			if (cell->type == "$gt" || cell->type == "$le") {
+				is_lt = cell->type == "$gt" ? 1 : 0;
+				sigVar = cell->getPort("\\B");
+				sigConst = cell->getPort("\\A");
+				width = cell->parameters["\\B_WIDTH"].as_int();
+				var_signed = cell->parameters["\\B_SIGNED"].as_bool();
+			}
+
+			// replace a(signed) < 0 with the high bit of a
+			if (sigConst.is_fully_const() && sigConst.is_fully_zero() && var_signed == true)
+			{
+				RTLIL::SigSpec a_prime(RTLIL::State::S0, cell->parameters["\\Y_WIDTH"].as_int());
+				a_prime[0] = sigVar[width - 1];
+				if (is_lt) {
+					log("Replacing %s cell `%s' (implementing X<0) with X[%d]: %s\n",
+							log_id(cell->type), log_id(cell), width-1, log_signal(a_prime));
+					module->connect(cell->getPort("\\Y"), a_prime);
+					module->remove(cell);
+				} else {
+					log("Replacing %s cell `%s' (implementing X>=0) with ~X[%d]: %s\n",
+							log_id(cell->type), log_id(cell), width-1, log_signal(a_prime));
+					module->addNot(NEW_ID, a_prime, cell->getPort("\\Y"));
+					module->remove(cell);
+				}
+				did_something = true;
+				goto next_cell;
+			} else
+			if (sigConst.is_fully_const() && sigConst.is_fully_def() && var_signed == false)
+			{
+				if (sigConst.is_fully_zero()) {
+					RTLIL::SigSpec a_prime(RTLIL::State::S0, 1);
+					if (is_lt) {
+						log("Replacing %s cell `%s' (implementing unsigned X<0) with constant false.\n",
+								log_id(cell->type), log_id(cell));
+						a_prime[0] = RTLIL::State::S0;
+					} else {
+						log("Replacing %s cell `%s' (implementing unsigned X>=0) with constant true.\n",
+								log_id(cell->type), log_id(cell));
+						a_prime[0] = RTLIL::State::S1;
+					}
+					module->connect(cell->getPort("\\Y"), a_prime);
+					module->remove(cell);
+					did_something = true;
+					goto next_cell;
+				}
+
+				int const_bit_set = get_onehot_bit_index(sigConst);
+				if (const_bit_set >= 0) {
+					int bit_set = const_bit_set;
+					RTLIL::SigSpec a_prime(RTLIL::State::S0, width - bit_set);
+					for (int i = bit_set; i < width; i++) {
+						a_prime[i - bit_set] = sigVar[i];
+					}
+					if (is_lt) {
+						log("Replacing %s cell `%s' (implementing unsigned X<%s) with !X[%d:%d]: %s.\n",
+								log_id(cell->type), log_id(cell), log_signal(sigConst), width - 1, bit_set, log_signal(a_prime));
+						module->addLogicNot(NEW_ID, a_prime, cell->getPort("\\Y"));
+					} else {
+						log("Replacing %s cell `%s' (implementing unsigned X>=%s) with |X[%d:%d]: %s.\n",
+								log_id(cell->type), log_id(cell), log_signal(sigConst), width - 1, bit_set, log_signal(a_prime));
+						module->addReduceOr(NEW_ID, a_prime, cell->getPort("\\Y"));
+					}
+					module->remove(cell);
+					did_something = true;
+					goto next_cell;
+				}
+			}
+		}
 
 	next_cell:;
 #undef ACTION_DO

From 8927e19b138f41786cf37a10c95956440971c8e6 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 1 Feb 2017 11:14:20 +0100
Subject: [PATCH 15/28] Update ABC scripts to use "&nf" instead of "map"

---
 passes/techmap/abc.cc | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc
index 9b829f435..a1cea3aaf 100644
--- a/passes/techmap/abc.cc
+++ b/passes/techmap/abc.cc
@@ -29,11 +29,11 @@
 // Kahn, Arthur B. (1962), "Topological sorting of large networks", Communications of the ACM 5 (11): 558-562, doi:10.1145/368996.369025
 // http://en.wikipedia.org/wiki/Topological_sorting
 
-#define ABC_COMMAND_LIB "strash; ifraig; scorr; dc2; dretime; strash; dch -f; map {D}"
-#define ABC_COMMAND_CTR "strash; ifraig; scorr; dc2; dretime; strash; dch -f; map {D}; buffer; upsize {D}; dnsize {D}; stime -p"
+#define ABC_COMMAND_LIB "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put"
+#define ABC_COMMAND_CTR "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put; buffer; upsize {D}; dnsize {D}; stime -p"
 #define ABC_COMMAND_LUT "strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2"
 #define ABC_COMMAND_SOP "strash; ifraig; scorr; dc2; dretime; strash; dch -f; cover {I} {P}"
-#define ABC_COMMAND_DFL "strash; ifraig; scorr; dc2; dretime; strash; dch -f; map"
+#define ABC_COMMAND_DFL "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put"
 
 #define ABC_FAST_COMMAND_LIB "strash; dretime; map {D}"
 #define ABC_FAST_COMMAND_CTR "strash; dretime; map {D}; buffer; upsize {D}; dnsize {D}; stime -p"

From 249ddbc16cca88f0ac7942526f0189c56ace93f9 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 1 Feb 2017 11:15:37 +0100
Subject: [PATCH 16/28] Update ABC to hg rev fe96921e5d50

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 01e1f6ad4..2d247a4ca 100644
--- a/Makefile
+++ b/Makefile
@@ -86,7 +86,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 = f8cadfe3861f
+ABCREV = fe96921e5d50
 ABCPULL = 1
 ABCURL ?= https://bitbucket.org/alanmi/abc
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)"

From 911c44d164e04026bd3a3a2eb1bf0c5d9cca5c19 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 4 Feb 2017 13:36:00 +0100
Subject: [PATCH 17/28] Add assert/assume support to verific front-end

---
 frontends/verific/build_amd64.txt |    2 +-
 frontends/verific/verific.cc      | 1474 +++++++++++++++--------------
 2 files changed, 769 insertions(+), 707 deletions(-)

diff --git a/frontends/verific/build_amd64.txt b/frontends/verific/build_amd64.txt
index d6952820e..95d618ecc 100644
--- a/frontends/verific/build_amd64.txt
+++ b/frontends/verific/build_amd64.txt
@@ -6,7 +6,7 @@ only have the i386 eval version of Verific:
 1.) Use a Makefile.conf like the following one:
 
 --snip--
-CONFIG := clang
+CONFIG := gcc
 ENABLE_TCL := 0
 ENABLE_PLUGINS := 0
 ENABLE_VERIFIC := 1
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 7dd36a747..9bf5a6c6c 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -49,7 +49,13 @@ USING_YOSYS_NAMESPACE
 using namespace Verific ;
 #endif
 
-static void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
+#endif
+
+PRIVATE_NAMESPACE_BEGIN
+
+#ifdef YOSYS_ENABLE_VERIFIC
+
+void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
 {
 	log("VERIFIC-%s [%s] ",
 			msg_type == VERIFIC_NONE ? "NONE" :
@@ -65,763 +71,817 @@ static void msg_func(msg_type_t msg_type, const char *message_id, linefile_type
 	log("\n");
 }
 
-static void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
+struct VerificImporter
 {
-	MapIter mi;
-	Att *attr;
-
-	if (obj->Linefile())
-		attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));
-
-	// FIXME: Parse numeric attributes
-	FOREACH_ATTRIBUTE(obj, mi, attr)
-		attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
-}
-
-static RTLIL::SigSpec operatorInput(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map)
-{
-	RTLIL::SigSpec sig;
-	for (int i = int(inst->InputSize())-1; i >= 0; i--)
-		if (inst->GetInputBit(i))
-			sig.append(net_map.at(inst->GetInputBit(i)));
-		else
-			sig.append(RTLIL::State::Sz);
-	return sig;
-}
-
-static RTLIL::SigSpec operatorInput1(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map)
-{
-	RTLIL::SigSpec sig;
-	for (int i = int(inst->Input1Size())-1; i >= 0; i--)
-		if (inst->GetInput1Bit(i))
-			sig.append(net_map.at(inst->GetInput1Bit(i)));
-		else
-			sig.append(RTLIL::State::Sz);
-	return sig;
-}
-
-static RTLIL::SigSpec operatorInput2(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map)
-{
-	RTLIL::SigSpec sig;
-	for (int i = int(inst->Input2Size())-1; i >= 0; i--)
-		if (inst->GetInput2Bit(i))
-			sig.append(net_map.at(inst->GetInput2Bit(i)));
-		else
-			sig.append(RTLIL::State::Sz);
-	return sig;
-}
-
-static RTLIL::SigSpec operatorInport(Instance *inst, const char *portname, std::map<Net*, RTLIL::SigBit> &net_map)
-{
-	PortBus *portbus = inst->View()->GetPortBus(portname);
-	if (portbus) {
-		RTLIL::SigSpec sig;
-		for (unsigned i = 0; i < portbus->Size(); i++) {
-			Net *net = inst->GetNet(portbus->ElementAtIndex(i));
-			if (net) {
-				if (net->IsGnd())
-					sig.append(RTLIL::State::S0);
-				else if (net->IsPwr())
-					sig.append(RTLIL::State::S1);
-				else
-					sig.append(net_map.at(net));
-			} else
-				sig.append(RTLIL::State::Sz);
-		}
-		return sig;
-	} else {
-		Port *port = inst->View()->GetPort(portname);
-		log_assert(port != NULL);
-		Net *net = inst->GetNet(port);
-		return net_map.at(net);
-	}
-}
-
-static RTLIL::SigSpec operatorOutput(Instance *inst, std::map<Net*, RTLIL::SigBit> &net_map, RTLIL::Module *module)
-{
-	RTLIL::SigSpec sig;
-	RTLIL::Wire *dummy_wire = NULL;
-	for (int i = int(inst->OutputSize())-1; i >= 0; i--)
-		if (inst->GetOutputBit(i)) {
-			sig.append(net_map.at(inst->GetOutputBit(i)));
-			dummy_wire = NULL;
-		} else {
-			if (dummy_wire == NULL)
-				dummy_wire = module->addWire(NEW_ID);
-			else
-				dummy_wire->width++;
-			sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1));
-		}
-	return sig;
-}
-
-static bool import_netlist_instance_gates(RTLIL::Module *module, std::map<Net*, RTLIL::SigBit> &net_map, Instance *inst)
-{
-	if (inst->Type() == PRIM_AND) {
-		module->addAndGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_NAND) {
-		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
-		module->addAndGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
-		module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_OR) {
-		module->addOrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_NOR) {
-		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
-		module->addOrGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
-		module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_XOR) {
-		module->addXorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_XNOR) {
-		module->addXnorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_BUF) {
-		module->addBufGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_INV) {
-		module->addNotGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_MUX) {
-		module->addMuxGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_TRI) {
-		module->addMuxGate(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_FADD)
-	{
-		RTLIL::SigSpec a = net_map.at(inst->GetInput1()), b = net_map.at(inst->GetInput2()), c = net_map.at(inst->GetCin());
-		RTLIL::SigSpec x = inst->GetCout() ? net_map.at(inst->GetCout()) : module->addWire(NEW_ID);
-		RTLIL::SigSpec y = inst->GetOutput() ? net_map.at(inst->GetOutput()) : module->addWire(NEW_ID);
-		RTLIL::SigSpec tmp1 = module->addWire(NEW_ID);
-		RTLIL::SigSpec tmp2 = module->addWire(NEW_ID);
-		RTLIL::SigSpec tmp3 = module->addWire(NEW_ID);
-		module->addXorGate(NEW_ID, a, b, tmp1);
-		module->addXorGate(RTLIL::escape_id(inst->Name()), tmp1, c, y);
-		module->addAndGate(NEW_ID, tmp1, c, tmp2);
-		module->addAndGate(NEW_ID, a, b, tmp3);
-		module->addOrGate(NEW_ID, tmp2, tmp3, x);
-		return true;
-	}
-
-	if (inst->Type() == PRIM_DFFRS)
-	{
-		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
-			module->addDffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		else if (inst->GetSet()->IsGnd())
-			module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), false);
-		else if (inst->GetReset()->IsGnd())
-			module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), true);
-		else
-			module->addDffsrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	return false;
-}
-
-static bool import_netlist_instance_cells(RTLIL::Module *module, std::map<Net*, RTLIL::SigBit> &net_map, Instance *inst)
-{
-	if (inst->Type() == PRIM_AND) {
-		module->addAnd(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_NAND) {
-		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
-		module->addAnd(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
-		module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_OR) {
-		module->addOr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_NOR) {
-		RTLIL::SigSpec tmp = module->addWire(NEW_ID);
-		module->addOr(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
-		module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_XOR) {
-		module->addXor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_XNOR) {
-		module->addXnor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_INV) {
-		module->addNot(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_MUX) {
-		module->addMux(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_TRI) {
-		module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_FADD)
-	{
-		RTLIL::SigSpec a_plus_b = module->addWire(NEW_ID, 2);
-		RTLIL::SigSpec y = inst->GetOutput() ? net_map.at(inst->GetOutput()) : module->addWire(NEW_ID);
-		if (inst->GetCout())
-			y.append(net_map.at(inst->GetCout()));
-		module->addAdd(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), a_plus_b);
-		module->addAdd(RTLIL::escape_id(inst->Name()), a_plus_b, net_map.at(inst->GetCin()), y);
-		return true;
-	}
-
-	if (inst->Type() == PRIM_DFFRS)
-	{
-		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
-			module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		else if (inst->GetSet()->IsGnd())
-			module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S0);
-		else if (inst->GetReset()->IsGnd())
-			module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S1);
-		else
-			module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	if (inst->Type() == PRIM_DLATCHRS)
-	{
-		if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
-			module->addDlatch(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		else
-			module->addDlatchsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
-					net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-		return true;
-	}
-
-	#define IN  operatorInput(inst, net_map)
-	#define IN1 operatorInput1(inst, net_map)
-	#define IN2 operatorInput2(inst, net_map)
-	#define OUT operatorOutput(inst, net_map, module)
-	#define SIGNED inst->View()->IsSigned()
-
-	if (inst->Type() == OPER_ADDER) {
-		RTLIL::SigSpec out = OUT;
-		if (inst->GetCout() != NULL)
-			out.append(net_map.at(inst->GetCout()));
-		if (inst->GetCin()->IsGnd()) {
-			module->addAdd(RTLIL::escape_id(inst->Name()), IN1, IN2, out, SIGNED);
-		} else {
-			RTLIL::SigSpec tmp = module->addWire(NEW_ID, GetSize(out));
-			module->addAdd(NEW_ID, IN1, IN2, tmp, SIGNED);
-			module->addAdd(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetCin()), out, false);
-		}
-		return true;
-	}
-
-	if (inst->Type() == OPER_MULTIPLIER) {
-		module->addMul(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_DIVIDER) {
-		module->addDiv(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_MODULO) {
-		module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_REMAINDER) {
-		module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_SHIFT_LEFT) {
-		module->addShl(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false);
-		return true;
-	}
-
-	if (inst->Type() == OPER_ENABLED_DECODER) {
-		RTLIL::SigSpec vec;
-		vec.append(net_map.at(inst->GetControl()));
-		for (unsigned i = 1; i < inst->OutputSize(); i++) {
-			vec.append(RTLIL::State::S0);
-		}
-		module->addShl(RTLIL::escape_id(inst->Name()), vec, IN, OUT, false);
-		return true;
-	}
-
-	if (inst->Type() == OPER_DECODER) {
-		RTLIL::SigSpec vec;
-		vec.append(RTLIL::State::S1);
-		for (unsigned i = 1; i < inst->OutputSize(); i++) {
-			vec.append(RTLIL::State::S0);
-		}
-		module->addShl(RTLIL::escape_id(inst->Name()), vec, IN, OUT, false);
-		return true;
-	}
-
-	if (inst->Type() == OPER_SHIFT_RIGHT) {
-		Net *net_cin = inst->GetCin();
-		Net *net_a_msb = inst->GetInput1Bit(0);
-		if (net_cin->IsGnd())
-			module->addShr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false);
-		else if (net_cin == net_a_msb)
-			module->addSshr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, true);
-		else
-			log_error("Can't import Verific OPER_SHIFT_RIGHT instance %s: carry_in is neither 0 nor msb of left input\n", inst->Name());
-		return true;
-	}
-
-	if (inst->Type() == OPER_REDUCE_AND) {
-		module->addReduceAnd(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_REDUCE_OR) {
-		module->addReduceOr(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_REDUCE_XOR) {
-		module->addReduceXor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_REDUCE_XNOR) {
-		module->addReduceXnor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_LESSTHAN) {
-		Net *net_cin = inst->GetCin();
-		if (net_cin->IsGnd())
-			module->addLt(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
-		else if (net_cin->IsPwr())
-			module->addLe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
-		else
-			log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name());
-		return true;
-	}
-
-	if (inst->Type() == OPER_WIDE_AND) {
-		module->addAnd(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_WIDE_OR) {
-		module->addOr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_WIDE_XOR) {
-		module->addXor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_WIDE_XNOR) {
-		module->addXnor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_WIDE_BUF) {
-		module->addPos(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_WIDE_INV) {
-		module->addNot(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_MINUS) {
-		module->addSub(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_UMINUS) {
-		module->addNeg(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_EQUAL) {
-		module->addEq(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_NEQUAL) {
-		module->addNe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
-		return true;
-	}
-
-	if (inst->Type() == OPER_WIDE_MUX) {
-		module->addMux(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetControl()), OUT);
-		return true;
-	}
-
-	if (inst->Type() == OPER_WIDE_TRI) {
-		module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map.at(inst->GetControl()), OUT);
-		return true;
-	}
-
-	if (inst->Type() == OPER_WIDE_DFFRS) {
-		RTLIL::SigSpec sig_set = operatorInport(inst, "set", net_map);
-		RTLIL::SigSpec sig_reset = operatorInport(inst, "reset", net_map);
-		if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool())
-			module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), IN, OUT);
-		else
-			module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), sig_set, sig_reset, IN, OUT);
-		return true;
-	}
-
-	#undef IN
-	#undef IN1
-	#undef IN2
-	#undef OUT
-	#undef SIGNED
-
-	return false;
-}
-
-static void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool mode_gates)
-{
-	std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name());
-
-	if (design->has(module_name)) {
-		if (!nl->IsOperator())
-			log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
-		return;
-	}
-
-	RTLIL::Module *module = new RTLIL::Module;
-	module->name = module_name;
-	design->add(module);
-
-	log("Importing module %s.\n", RTLIL::id2cstr(module->name));
-
+	RTLIL::Module *module;
 	std::map<Net*, RTLIL::SigBit> net_map;
+	std::map<Net*, Net*> sva_posedge_map;
 
-	SetIter si;
-	MapIter mi, mi2;
-	Port *port;
-	PortBus *portbus;
-	Net *net;
-	NetBus *netbus;
-	Instance *inst;
-	PortRef *pr;
-
-	FOREACH_PORT_OF_NETLIST(nl, mi, port)
+	void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj)
 	{
-		if (port->Bus())
-			continue;
+		MapIter mi;
+		Att *attr;
 
-		// log("  importing port %s.\n", port->Name());
+		if (obj->Linefile())
+			attributes["\\src"] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile()));
 
-		RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name()));
-		import_attributes(wire->attributes, port);
+		// FIXME: Parse numeric attributes
+		FOREACH_ATTRIBUTE(obj, mi, attr)
+			attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(std::string(attr->Value()));
+	}
 
-		wire->port_id = nl->IndexOf(port) + 1;
-
-		if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_IN)
-			wire->port_input = true;
-		if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_OUT)
-			wire->port_output = true;
-
-		if (port->GetNet()) {
-			net = port->GetNet();
-			if (net_map.count(net) == 0)
-				net_map[net] = wire;
-			else if (wire->port_input)
-				module->connect(net_map.at(net), wire);
+	RTLIL::SigSpec operatorInput(Instance *inst)
+	{
+		RTLIL::SigSpec sig;
+		for (int i = int(inst->InputSize())-1; i >= 0; i--)
+			if (inst->GetInputBit(i))
+				sig.append(net_map.at(inst->GetInputBit(i)));
 			else
-				module->connect(wire, net_map.at(net));
-		}
+				sig.append(RTLIL::State::Sz);
+		return sig;
 	}
 
-	FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
+	RTLIL::SigSpec operatorInput1(Instance *inst)
 	{
-		// log("  importing portbus %s.\n", portbus->Name());
-
-		RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size());
-		wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex());
-		import_attributes(wire->attributes, portbus);
-
-		if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN)
-			wire->port_input = true;
-		if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_OUT)
-			wire->port_output = true;
-
-		for (int i = portbus->LeftIndex();; i += portbus->IsUp() ? +1 : -1) {
-			if (portbus->ElementAtIndex(i) && portbus->ElementAtIndex(i)->GetNet()) {
-				net = portbus->ElementAtIndex(i)->GetNet();
-				RTLIL::SigBit bit(wire, i - wire->start_offset);
-				if (net_map.count(net) == 0)
-					net_map[net] = bit;
-				else if (wire->port_input)
-					module->connect(net_map.at(net), bit);
-				else
-					module->connect(bit, net_map.at(net));
-			}
-			if (i == portbus->RightIndex())
-				break;
-		}
+		RTLIL::SigSpec sig;
+		for (int i = int(inst->Input1Size())-1; i >= 0; i--)
+			if (inst->GetInput1Bit(i))
+				sig.append(net_map.at(inst->GetInput1Bit(i)));
+			else
+				sig.append(RTLIL::State::Sz);
+		return sig;
 	}
 
-	module->fixup_ports();
-
-	FOREACH_NET_OF_NETLIST(nl, mi, net)
+	RTLIL::SigSpec operatorInput2(Instance *inst)
 	{
-		if (net->IsRamNet())
-		{
-			RTLIL::Memory *memory = new RTLIL::Memory;
-			memory->name = RTLIL::escape_id(net->Name());
-			log_assert(module->count_id(memory->name) == 0);
-			module->memories[memory->name] = memory;
-
-			int number_of_bits = net->Size();
-			int bits_in_word = number_of_bits;
-			FOREACH_PORTREF_OF_NET(net, si, pr) {
-				if (pr->GetInst()->Type() == OPER_READ_PORT) {
-					bits_in_word = min<int>(bits_in_word, pr->GetInst()->OutputSize());
-					continue;
-				}
-				if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) {
-					bits_in_word = min<int>(bits_in_word, pr->GetInst()->Input2Size());
-					continue;
-				}
-				log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n",
-						net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name());
-			}
-
-			memory->width = bits_in_word;
-			memory->size = number_of_bits / bits_in_word;
-			continue;
-		}
-
-		if (net_map.count(net)) {
-			// log("  skipping net %s.\n", net->Name());
-			continue;
-		}
-
-		if (net->Bus())
-			continue;
-
-		// log("  importing net %s.\n", net->Name());
-
-		RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(net->Name()));
-		RTLIL::Wire *wire = module->addWire(wire_name);
-		import_attributes(wire->attributes, net);
-
-		net_map[net] = wire;
+		RTLIL::SigSpec sig;
+		for (int i = int(inst->Input2Size())-1; i >= 0; i--)
+			if (inst->GetInput2Bit(i))
+				sig.append(net_map.at(inst->GetInput2Bit(i)));
+			else
+				sig.append(RTLIL::State::Sz);
+		return sig;
 	}
 
-	FOREACH_NETBUS_OF_NETLIST(nl, mi, netbus)
+	RTLIL::SigSpec operatorInport(Instance *inst, const char *portname)
 	{
-		bool found_new_net = false;
-		for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
-			net = netbus->ElementAtIndex(i);
-			if (net_map.count(net) == 0)
-				found_new_net = true;
-			if (i == netbus->RightIndex())
-				break;
-		}
-
-		if (found_new_net)
-		{
-			// log("  importing netbus %s.\n", netbus->Name());
-
-			RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(netbus->Name()));
-			RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
-			wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
-			import_attributes(wire->attributes, netbus);
-
-			for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
-				if (netbus->ElementAtIndex(i)) {
-					net = netbus->ElementAtIndex(i);
-					RTLIL::SigBit bit(wire, i - wire->start_offset);
-					if (net_map.count(net) == 0)
-						net_map[net] = bit;
+		PortBus *portbus = inst->View()->GetPortBus(portname);
+		if (portbus) {
+			RTLIL::SigSpec sig;
+			for (unsigned i = 0; i < portbus->Size(); i++) {
+				Net *net = inst->GetNet(portbus->ElementAtIndex(i));
+				if (net) {
+					if (net->IsGnd())
+						sig.append(RTLIL::State::S0);
+					else if (net->IsPwr())
+						sig.append(RTLIL::State::S1);
 					else
-						module->connect(bit, net_map.at(net));
-				}
-				if (i == netbus->RightIndex())
-					break;
+						sig.append(net_map.at(net));
+				} else
+					sig.append(RTLIL::State::Sz);
 			}
-		}
-		else
-		{
-			// log("  skipping netbus %s.\n", netbus->Name());
+			return sig;
+		} else {
+			Port *port = inst->View()->GetPort(portname);
+			log_assert(port != NULL);
+			Net *net = inst->GetNet(port);
+			return net_map.at(net);
 		}
 	}
 
-	FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
+	RTLIL::SigSpec operatorOutput(Instance *inst)
 	{
-		// log("  importing cell %s (%s).\n", inst->Name(), inst->View()->Owner()->Name());
+		RTLIL::SigSpec sig;
+		RTLIL::Wire *dummy_wire = NULL;
+		for (int i = int(inst->OutputSize())-1; i >= 0; i--)
+			if (inst->GetOutputBit(i)) {
+				sig.append(net_map.at(inst->GetOutputBit(i)));
+				dummy_wire = NULL;
+			} else {
+				if (dummy_wire == NULL)
+					dummy_wire = module->addWire(NEW_ID);
+				else
+					dummy_wire->width++;
+				sig.append(RTLIL::SigSpec(dummy_wire, dummy_wire->width - 1));
+			}
+		return sig;
+	}
 
-		if (inst->Type() == PRIM_PWR) {
-			module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S1);
-			continue;
+	bool import_netlist_instance_gates(Instance *inst)
+	{
+		if (inst->Type() == PRIM_AND) {
+			module->addAndGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
 		}
 
-		if (inst->Type() == PRIM_GND) {
-			module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S0);
-			continue;
+		if (inst->Type() == PRIM_NAND) {
+			RTLIL::SigSpec tmp = module->addWire(NEW_ID);
+			module->addAndGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
+			module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_OR) {
+			module->addOrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_NOR) {
+			RTLIL::SigSpec tmp = module->addWire(NEW_ID);
+			module->addOrGate(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
+			module->addNotGate(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_XOR) {
+			module->addXorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_XNOR) {
+			module->addXnorGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
 		}
 
 		if (inst->Type() == PRIM_BUF) {
 			module->addBufGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
-			continue;
+			return true;
 		}
 
-		if (inst->Type() == PRIM_X) {
-			module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sx);
-			continue;
+		if (inst->Type() == PRIM_INV) {
+			module->addNotGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			return true;
 		}
 
-		if (inst->Type() == PRIM_Z) {
-			module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sz);
-			continue;
+		if (inst->Type() == PRIM_MUX) {
+			module->addMuxGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
+			return true;
 		}
 
-		if (inst->Type() == OPER_READ_PORT)
+		if (inst->Type() == PRIM_TRI) {
+			module->addMuxGate(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_FADD)
 		{
-			RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name()));
-			if (memory->width != int(inst->OutputSize()))
-				log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
-
-			RTLIL::SigSpec addr = operatorInput1(inst, net_map);
-			RTLIL::SigSpec data = operatorOutput(inst, net_map, module);
-
-			RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memrd");
-			cell->parameters["\\MEMID"] = memory->name.str();
-			cell->parameters["\\CLK_ENABLE"] = false;
-			cell->parameters["\\CLK_POLARITY"] = true;
-			cell->parameters["\\TRANSPARENT"] = false;
-			cell->parameters["\\ABITS"] = GetSize(addr);
-			cell->parameters["\\WIDTH"] = GetSize(data);
-			cell->setPort("\\CLK", RTLIL::State::Sx);
-			cell->setPort("\\EN", RTLIL::State::Sx);
-			cell->setPort("\\ADDR", addr);
-			cell->setPort("\\DATA", data);
-			continue;
+			RTLIL::SigSpec a = net_map.at(inst->GetInput1()), b = net_map.at(inst->GetInput2()), c = net_map.at(inst->GetCin());
+			RTLIL::SigSpec x = inst->GetCout() ? net_map.at(inst->GetCout()) : module->addWire(NEW_ID);
+			RTLIL::SigSpec y = inst->GetOutput() ? net_map.at(inst->GetOutput()) : module->addWire(NEW_ID);
+			RTLIL::SigSpec tmp1 = module->addWire(NEW_ID);
+			RTLIL::SigSpec tmp2 = module->addWire(NEW_ID);
+			RTLIL::SigSpec tmp3 = module->addWire(NEW_ID);
+			module->addXorGate(NEW_ID, a, b, tmp1);
+			module->addXorGate(RTLIL::escape_id(inst->Name()), tmp1, c, y);
+			module->addAndGate(NEW_ID, tmp1, c, tmp2);
+			module->addAndGate(NEW_ID, a, b, tmp3);
+			module->addOrGate(NEW_ID, tmp2, tmp3, x);
+			return true;
 		}
 
-		if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT)
+		if (inst->Type() == PRIM_DFFRS)
 		{
-			RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name()));
-			if (memory->width != int(inst->Input2Size()))
-				log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
-
-			RTLIL::SigSpec addr = operatorInput1(inst, net_map);
-			RTLIL::SigSpec data = operatorInput2(inst, net_map);
-
-			RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memwr");
-			cell->parameters["\\MEMID"] = memory->name.str();
-			cell->parameters["\\CLK_ENABLE"] = false;
-			cell->parameters["\\CLK_POLARITY"] = true;
-			cell->parameters["\\PRIORITY"] = 0;
-			cell->parameters["\\ABITS"] = GetSize(addr);
-			cell->parameters["\\WIDTH"] = GetSize(data);
-			cell->setPort("\\EN", RTLIL::SigSpec(net_map.at(inst->GetControl())).repeat(GetSize(data)));
-			cell->setPort("\\CLK", RTLIL::State::S0);
-			cell->setPort("\\ADDR", addr);
-			cell->setPort("\\DATA", data);
-
-			if (inst->Type() == OPER_CLOCKED_WRITE_PORT) {
-				cell->parameters["\\CLK_ENABLE"] = true;
-				cell->setPort("\\CLK", net_map.at(inst->GetClock()));
-			}
-			continue;
+			if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
+				module->addDffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			else if (inst->GetSet()->IsGnd())
+				module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()),
+						net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), false);
+			else if (inst->GetReset()->IsGnd())
+				module->addAdffGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()),
+						net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), true);
+			else
+				module->addDffsrGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
+						net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			return true;
 		}
 
-		if (!mode_gates) {
-			if (import_netlist_instance_cells(module, net_map, inst))
+		return false;
+	}
+
+	bool import_netlist_instance_cells(Instance *inst)
+	{
+		if (inst->Type() == PRIM_AND) {
+			module->addAnd(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_NAND) {
+			RTLIL::SigSpec tmp = module->addWire(NEW_ID);
+			module->addAnd(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
+			module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_OR) {
+			module->addOr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_NOR) {
+			RTLIL::SigSpec tmp = module->addWire(NEW_ID);
+			module->addOr(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), tmp);
+			module->addNot(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_XOR) {
+			module->addXor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_XNOR) {
+			module->addXnor(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_INV) {
+			module->addNot(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_MUX) {
+			module->addMux(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_TRI) {
+			module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::State::Sz, net_map.at(inst->GetInput()), net_map.at(inst->GetControl()), net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_FADD)
+		{
+			RTLIL::SigSpec a_plus_b = module->addWire(NEW_ID, 2);
+			RTLIL::SigSpec y = inst->GetOutput() ? net_map.at(inst->GetOutput()) : module->addWire(NEW_ID);
+			if (inst->GetCout())
+				y.append(net_map.at(inst->GetCout()));
+			module->addAdd(NEW_ID, net_map.at(inst->GetInput1()), net_map.at(inst->GetInput2()), a_plus_b);
+			module->addAdd(RTLIL::escape_id(inst->Name()), a_plus_b, net_map.at(inst->GetCin()), y);
+			return true;
+		}
+
+		if (inst->Type() == PRIM_DFFRS)
+		{
+			if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
+				module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			else if (inst->GetSet()->IsGnd())
+				module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetReset()),
+						net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S0);
+			else if (inst->GetReset()->IsGnd())
+				module->addAdff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()),
+						net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()), RTLIL::State::S1);
+			else
+				module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
+						net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		if (inst->Type() == PRIM_DLATCHRS)
+		{
+			if (inst->GetSet()->IsGnd() && inst->GetReset()->IsGnd())
+				module->addDlatch(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			else
+				module->addDlatchsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetControl()), net_map.at(inst->GetSet()), net_map.at(inst->GetReset()),
+						net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+			return true;
+		}
+
+		#define IN  operatorInput(inst)
+		#define IN1 operatorInput1(inst)
+		#define IN2 operatorInput2(inst)
+		#define OUT operatorOutput(inst)
+		#define SIGNED inst->View()->IsSigned()
+
+		if (inst->Type() == OPER_ADDER) {
+			RTLIL::SigSpec out = OUT;
+			if (inst->GetCout() != NULL)
+				out.append(net_map.at(inst->GetCout()));
+			if (inst->GetCin()->IsGnd()) {
+				module->addAdd(RTLIL::escape_id(inst->Name()), IN1, IN2, out, SIGNED);
+			} else {
+				RTLIL::SigSpec tmp = module->addWire(NEW_ID, GetSize(out));
+				module->addAdd(NEW_ID, IN1, IN2, tmp, SIGNED);
+				module->addAdd(RTLIL::escape_id(inst->Name()), tmp, net_map.at(inst->GetCin()), out, false);
+			}
+			return true;
+		}
+
+		if (inst->Type() == OPER_MULTIPLIER) {
+			module->addMul(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_DIVIDER) {
+			module->addDiv(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_MODULO) {
+			module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_REMAINDER) {
+			module->addMod(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_SHIFT_LEFT) {
+			module->addShl(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false);
+			return true;
+		}
+
+		if (inst->Type() == OPER_ENABLED_DECODER) {
+			RTLIL::SigSpec vec;
+			vec.append(net_map.at(inst->GetControl()));
+			for (unsigned i = 1; i < inst->OutputSize(); i++) {
+				vec.append(RTLIL::State::S0);
+			}
+			module->addShl(RTLIL::escape_id(inst->Name()), vec, IN, OUT, false);
+			return true;
+		}
+
+		if (inst->Type() == OPER_DECODER) {
+			RTLIL::SigSpec vec;
+			vec.append(RTLIL::State::S1);
+			for (unsigned i = 1; i < inst->OutputSize(); i++) {
+				vec.append(RTLIL::State::S0);
+			}
+			module->addShl(RTLIL::escape_id(inst->Name()), vec, IN, OUT, false);
+			return true;
+		}
+
+		if (inst->Type() == OPER_SHIFT_RIGHT) {
+			Net *net_cin = inst->GetCin();
+			Net *net_a_msb = inst->GetInput1Bit(0);
+			if (net_cin->IsGnd())
+				module->addShr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, false);
+			else if (net_cin == net_a_msb)
+				module->addSshr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, true);
+			else
+				log_error("Can't import Verific OPER_SHIFT_RIGHT instance %s: carry_in is neither 0 nor msb of left input\n", inst->Name());
+			return true;
+		}
+
+		if (inst->Type() == OPER_REDUCE_AND) {
+			module->addReduceAnd(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_REDUCE_OR) {
+			module->addReduceOr(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_REDUCE_XOR) {
+			module->addReduceXor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_REDUCE_XNOR) {
+			module->addReduceXnor(RTLIL::escape_id(inst->Name()), IN, net_map.at(inst->GetOutput()), SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_LESSTHAN) {
+			Net *net_cin = inst->GetCin();
+			if (net_cin->IsGnd())
+				module->addLt(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
+			else if (net_cin->IsPwr())
+				module->addLe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
+			else
+				log_error("Can't import Verific OPER_LESSTHAN instance %s: carry_in is neither 0 nor 1\n", inst->Name());
+			return true;
+		}
+
+		if (inst->Type() == OPER_WIDE_AND) {
+			module->addAnd(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_WIDE_OR) {
+			module->addOr(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_WIDE_XOR) {
+			module->addXor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_WIDE_XNOR) {
+			module->addXnor(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_WIDE_BUF) {
+			module->addPos(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_WIDE_INV) {
+			module->addNot(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_MINUS) {
+			module->addSub(RTLIL::escape_id(inst->Name()), IN1, IN2, OUT, SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_UMINUS) {
+			module->addNeg(RTLIL::escape_id(inst->Name()), IN, OUT, SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_EQUAL) {
+			module->addEq(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_NEQUAL) {
+			module->addNe(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetOutput()), SIGNED);
+			return true;
+		}
+
+		if (inst->Type() == OPER_WIDE_MUX) {
+			module->addMux(RTLIL::escape_id(inst->Name()), IN1, IN2, net_map.at(inst->GetControl()), OUT);
+			return true;
+		}
+
+		if (inst->Type() == OPER_WIDE_TRI) {
+			module->addMux(RTLIL::escape_id(inst->Name()), RTLIL::SigSpec(RTLIL::State::Sz, inst->OutputSize()), IN, net_map.at(inst->GetControl()), OUT);
+			return true;
+		}
+
+		if (inst->Type() == OPER_WIDE_DFFRS) {
+			RTLIL::SigSpec sig_set = operatorInport(inst, "set");
+			RTLIL::SigSpec sig_reset = operatorInport(inst, "reset");
+			if (sig_set.is_fully_const() && !sig_set.as_bool() && sig_reset.is_fully_const() && !sig_reset.as_bool())
+				module->addDff(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), IN, OUT);
+			else
+				module->addDffsr(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetClock()), sig_set, sig_reset, IN, OUT);
+			return true;
+		}
+
+		#undef IN
+		#undef IN1
+		#undef IN2
+		#undef OUT
+		#undef SIGNED
+
+		return false;
+	}
+
+	void import_netlist(RTLIL::Design *design, Netlist *nl, std::set<Netlist*> &nl_todo, bool mode_gates)
+	{
+		std::string module_name = nl->IsOperator() ? std::string("$verific$") + nl->Owner()->Name() : RTLIL::escape_id(nl->Owner()->Name());
+
+		if (design->has(module_name)) {
+			if (!nl->IsOperator())
+				log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name());
+			return;
+		}
+
+		module = new RTLIL::Module;
+		module->name = module_name;
+		design->add(module);
+
+		log("Importing module %s.\n", RTLIL::id2cstr(module->name));
+
+		SetIter si;
+		MapIter mi, mi2;
+		Port *port;
+		PortBus *portbus;
+		Net *net;
+		NetBus *netbus;
+		Instance *inst;
+		PortRef *pr;
+
+		FOREACH_PORT_OF_NETLIST(nl, mi, port)
+		{
+			if (port->Bus())
 				continue;
-			if (inst->IsOperator())
-				log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name());
-		} else {
-			if (import_netlist_instance_gates(module, net_map, inst))
+
+			// log("  importing port %s.\n", port->Name());
+
+			RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(port->Name()));
+			import_attributes(wire->attributes, port);
+
+			wire->port_id = nl->IndexOf(port) + 1;
+
+			if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_IN)
+				wire->port_input = true;
+			if (port->GetDir() == DIR_INOUT || port->GetDir() == DIR_OUT)
+				wire->port_output = true;
+
+			if (port->GetNet()) {
+				net = port->GetNet();
+				if (net_map.count(net) == 0)
+					net_map[net] = wire;
+				else if (wire->port_input)
+					module->connect(net_map.at(net), wire);
+				else
+					module->connect(wire, net_map.at(net));
+			}
+		}
+
+		FOREACH_PORTBUS_OF_NETLIST(nl, mi, portbus)
+		{
+			// log("  importing portbus %s.\n", portbus->Name());
+
+			RTLIL::Wire *wire = module->addWire(RTLIL::escape_id(portbus->Name()), portbus->Size());
+			wire->start_offset = min(portbus->LeftIndex(), portbus->RightIndex());
+			import_attributes(wire->attributes, portbus);
+
+			if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_IN)
+				wire->port_input = true;
+			if (portbus->GetDir() == DIR_INOUT || portbus->GetDir() == DIR_OUT)
+				wire->port_output = true;
+
+			for (int i = portbus->LeftIndex();; i += portbus->IsUp() ? +1 : -1) {
+				if (portbus->ElementAtIndex(i) && portbus->ElementAtIndex(i)->GetNet()) {
+					net = portbus->ElementAtIndex(i)->GetNet();
+					RTLIL::SigBit bit(wire, i - wire->start_offset);
+					if (net_map.count(net) == 0)
+						net_map[net] = bit;
+					else if (wire->port_input)
+						module->connect(net_map.at(net), bit);
+					else
+						module->connect(bit, net_map.at(net));
+				}
+				if (i == portbus->RightIndex())
+					break;
+			}
+		}
+
+		module->fixup_ports();
+
+		FOREACH_NET_OF_NETLIST(nl, mi, net)
+		{
+			if (net->IsRamNet())
+			{
+				RTLIL::Memory *memory = new RTLIL::Memory;
+				memory->name = RTLIL::escape_id(net->Name());
+				log_assert(module->count_id(memory->name) == 0);
+				module->memories[memory->name] = memory;
+
+				int number_of_bits = net->Size();
+				int bits_in_word = number_of_bits;
+				FOREACH_PORTREF_OF_NET(net, si, pr) {
+					if (pr->GetInst()->Type() == OPER_READ_PORT) {
+						bits_in_word = min<int>(bits_in_word, pr->GetInst()->OutputSize());
+						continue;
+					}
+					if (pr->GetInst()->Type() == OPER_WRITE_PORT || pr->GetInst()->Type() == OPER_CLOCKED_WRITE_PORT) {
+						bits_in_word = min<int>(bits_in_word, pr->GetInst()->Input2Size());
+						continue;
+					}
+					log_error("Verific RamNet %s is connected to unsupported instance type %s (%s).\n",
+							net->Name(), pr->GetInst()->View()->Owner()->Name(), pr->GetInst()->Name());
+				}
+
+				memory->width = bits_in_word;
+				memory->size = number_of_bits / bits_in_word;
 				continue;
+			}
+
+			if (net_map.count(net)) {
+				// log("  skipping net %s.\n", net->Name());
+				continue;
+			}
+
+			if (net->Bus())
+				continue;
+
+			// log("  importing net %s.\n", net->Name());
+
+			RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(net->Name()));
+			RTLIL::Wire *wire = module->addWire(wire_name);
+			import_attributes(wire->attributes, net);
+
+			net_map[net] = wire;
 		}
 
-		if (inst->IsPrimitive())
-			log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
-
-		nl_todo.insert(inst->View());
-
-		RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), inst->IsOperator() ?
-				std::string("$verific$") + inst->View()->Owner()->Name() : RTLIL::escape_id(inst->View()->Owner()->Name()));
-
-		dict<IdString, vector<SigBit>> cell_port_conns;
-
-		FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
-			// log("      .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name());
-			const char *port_name = pr->GetPort()->Name();
-			int port_offset = 0;
-			if (pr->GetPort()->Bus()) {
-				port_name = pr->GetPort()->Bus()->Name();
-				port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) -
-						min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex());
+		FOREACH_NETBUS_OF_NETLIST(nl, mi, netbus)
+		{
+			bool found_new_net = false;
+			for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
+				net = netbus->ElementAtIndex(i);
+				if (net_map.count(net) == 0)
+					found_new_net = true;
+				if (i == netbus->RightIndex())
+					break;
 			}
-			IdString port_name_id = RTLIL::escape_id(port_name);
-			auto &sigvec = cell_port_conns[port_name_id];
-			if (GetSize(sigvec) <= port_offset) {
-				SigSpec zwires = module->addWire(NEW_ID, port_offset+1-GetSize(sigvec));
-				for (auto bit : zwires)
-					sigvec.push_back(bit);
+
+			if (found_new_net)
+			{
+				// log("  importing netbus %s.\n", netbus->Name());
+
+				RTLIL::IdString wire_name = module->uniquify(RTLIL::escape_id(netbus->Name()));
+				RTLIL::Wire *wire = module->addWire(wire_name, netbus->Size());
+				wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
+				import_attributes(wire->attributes, netbus);
+
+				for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
+					if (netbus->ElementAtIndex(i)) {
+						net = netbus->ElementAtIndex(i);
+						RTLIL::SigBit bit(wire, i - wire->start_offset);
+						if (net_map.count(net) == 0)
+							net_map[net] = bit;
+						else
+							module->connect(bit, net_map.at(net));
+					}
+					if (i == netbus->RightIndex())
+						break;
+				}
+			}
+			else
+			{
+				// log("  skipping netbus %s.\n", netbus->Name());
 			}
-			sigvec[port_offset] = net_map.at(pr->GetNet());
 		}
 
-		for (auto &it : cell_port_conns) {
-			// log("      .%s(%s)\n", log_id(it.first), log_signal(it.second));
-			cell->setPort(it.first, it.second);
+		FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
+		{
+			if (inst->Type() == PRIM_SVA_POSEDGE) {
+				Net *in_net = inst->GetInput();
+				Net *out_net = inst->GetOutput();
+				sva_posedge_map[out_net] = in_net;
+				continue;
+			}
+		}
+
+		FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
+		{
+			if (inst->Type() == PRIM_SVA_POSEDGE)
+				continue;
+
+			// log("  importing cell %s (%s).\n", inst->Name(), inst->View()->Owner()->Name());
+
+			if (inst->Type() == PRIM_SVA_AT)
+			{
+				Net *in1 = inst->GetInput1();
+				Net *in2 = inst->GetInput2();
+				Net *out = inst->GetOutput();
+
+				if (sva_posedge_map.count(in2))
+					std::swap(in1, in2);
+
+				log_assert(sva_posedge_map.count(in1));
+				Net *clk = sva_posedge_map.at(in1);
+
+				SigBit outsig = net_map.at(out);
+				log_assert(outsig.wire && GetSize(outsig.wire) == 1);
+				outsig.wire->attributes["\\init"] == Const(0, 1);
+
+				module->addDff(NEW_ID, net_map.at(clk), net_map.at(in2), net_map.at(out));
+				continue;
+			}
+
+			if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSERT || inst->Type() == PRIM_SVA_ASSERT) {
+				Net *in = inst->GetInput();
+				module->addAssert(NEW_ID, net_map.at(in), State::S1);
+				continue;
+			}
+
+			if (inst->Type() == PRIM_SVA_IMMEDIATE_ASSUME || inst->Type() == PRIM_SVA_ASSUME) {
+				Net *in = inst->GetInput();
+				module->addAssume(NEW_ID, net_map.at(in), State::S1);
+				continue;
+			}
+
+			if (inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_COVER) {
+				// Net *in = inst->GetInput();
+				// module->addCover(NEW_ID, net_map.at(in), State::S1);
+				continue;
+			}
+
+			if (inst->Type() == PRIM_PWR) {
+				module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S1);
+				continue;
+			}
+
+			if (inst->Type() == PRIM_GND) {
+				module->connect(net_map.at(inst->GetOutput()), RTLIL::State::S0);
+				continue;
+			}
+
+			if (inst->Type() == PRIM_BUF) {
+				module->addBufGate(RTLIL::escape_id(inst->Name()), net_map.at(inst->GetInput()), net_map.at(inst->GetOutput()));
+				continue;
+			}
+
+			if (inst->Type() == PRIM_X) {
+				module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sx);
+				continue;
+			}
+
+			if (inst->Type() == PRIM_Z) {
+				module->connect(net_map.at(inst->GetOutput()), RTLIL::State::Sz);
+				continue;
+			}
+
+			if (inst->Type() == OPER_READ_PORT)
+			{
+				RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetInput()->Name()));
+				if (memory->width != int(inst->OutputSize()))
+					log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
+
+				RTLIL::SigSpec addr = operatorInput1(inst);
+				RTLIL::SigSpec data = operatorOutput(inst);
+
+				RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memrd");
+				cell->parameters["\\MEMID"] = memory->name.str();
+				cell->parameters["\\CLK_ENABLE"] = false;
+				cell->parameters["\\CLK_POLARITY"] = true;
+				cell->parameters["\\TRANSPARENT"] = false;
+				cell->parameters["\\ABITS"] = GetSize(addr);
+				cell->parameters["\\WIDTH"] = GetSize(data);
+				cell->setPort("\\CLK", RTLIL::State::Sx);
+				cell->setPort("\\EN", RTLIL::State::Sx);
+				cell->setPort("\\ADDR", addr);
+				cell->setPort("\\DATA", data);
+				continue;
+			}
+
+			if (inst->Type() == OPER_WRITE_PORT || inst->Type() == OPER_CLOCKED_WRITE_PORT)
+			{
+				RTLIL::Memory *memory = module->memories.at(RTLIL::escape_id(inst->GetOutput()->Name()));
+				if (memory->width != int(inst->Input2Size()))
+					log_error("Import of asymetric memories from Verific is not supported yet: %s %s\n", inst->Name(), inst->GetInput()->Name());
+
+				RTLIL::SigSpec addr = operatorInput1(inst);
+				RTLIL::SigSpec data = operatorInput2(inst);
+
+				RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), "$memwr");
+				cell->parameters["\\MEMID"] = memory->name.str();
+				cell->parameters["\\CLK_ENABLE"] = false;
+				cell->parameters["\\CLK_POLARITY"] = true;
+				cell->parameters["\\PRIORITY"] = 0;
+				cell->parameters["\\ABITS"] = GetSize(addr);
+				cell->parameters["\\WIDTH"] = GetSize(data);
+				cell->setPort("\\EN", RTLIL::SigSpec(net_map.at(inst->GetControl())).repeat(GetSize(data)));
+				cell->setPort("\\CLK", RTLIL::State::S0);
+				cell->setPort("\\ADDR", addr);
+				cell->setPort("\\DATA", data);
+
+				if (inst->Type() == OPER_CLOCKED_WRITE_PORT) {
+					cell->parameters["\\CLK_ENABLE"] = true;
+					cell->setPort("\\CLK", net_map.at(inst->GetClock()));
+				}
+				continue;
+			}
+
+			if (!mode_gates) {
+				if (import_netlist_instance_cells(inst))
+					continue;
+				if (inst->IsOperator())
+					log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name());
+			} else {
+				if (import_netlist_instance_gates(inst))
+					continue;
+			}
+
+			if (inst->IsPrimitive())
+				log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
+
+			nl_todo.insert(inst->View());
+
+			RTLIL::Cell *cell = module->addCell(RTLIL::escape_id(inst->Name()), inst->IsOperator() ?
+					std::string("$verific$") + inst->View()->Owner()->Name() : RTLIL::escape_id(inst->View()->Owner()->Name()));
+
+			dict<IdString, vector<SigBit>> cell_port_conns;
+
+			FOREACH_PORTREF_OF_INST(inst, mi2, pr) {
+				// log("      .%s(%s)\n", pr->GetPort()->Name(), pr->GetNet()->Name());
+				const char *port_name = pr->GetPort()->Name();
+				int port_offset = 0;
+				if (pr->GetPort()->Bus()) {
+					port_name = pr->GetPort()->Bus()->Name();
+					port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) -
+							min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex());
+				}
+				IdString port_name_id = RTLIL::escape_id(port_name);
+				auto &sigvec = cell_port_conns[port_name_id];
+				if (GetSize(sigvec) <= port_offset) {
+					SigSpec zwires = module->addWire(NEW_ID, port_offset+1-GetSize(sigvec));
+					for (auto bit : zwires)
+						sigvec.push_back(bit);
+				}
+				sigvec[port_offset] = net_map.at(pr->GetNet());
+			}
+
+			for (auto &it : cell_port_conns) {
+				// log("      .%s(%s)\n", log_id(it.first), log_signal(it.second));
+				cell->setPort(it.first, it.second);
+			}
 		}
 	}
-}
+};
 
 #endif /* YOSYS_ENABLE_VERIFIC */
 
-YOSYS_NAMESPACE_BEGIN
-
 struct VerificPass : public Pass {
 	VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { }
 	virtual void help()
@@ -982,8 +1042,10 @@ struct VerificPass : public Pass {
 
 			while (!nl_todo.empty()) {
 				Netlist *nl = *nl_todo.begin();
-				if (nl_done.count(nl) == 0)
-					import_netlist(design, nl, nl_todo, mode_gates);
+				if (nl_done.count(nl) == 0) {
+					VerificImporter importer;
+					importer.import_netlist(design, nl, nl_todo, mode_gates);
+				}
 				nl_todo.erase(nl);
 				nl_done.insert(nl);
 			}
@@ -1001,5 +1063,5 @@ struct VerificPass : public Pass {
 #endif
 } VerificPass;
 
-YOSYS_NAMESPACE_END
+PRIVATE_NAMESPACE_END
 

From 3928482a3c4fb71b8e6ccdcb362c030eef34a479 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 4 Feb 2017 14:14:26 +0100
Subject: [PATCH 18/28] Add $cover cell type and SVA cover() support

---
 frontends/ast/ast.cc               |  1 +
 frontends/ast/ast.h                |  1 +
 frontends/ast/genrtlil.cc          |  2 ++
 frontends/ast/simplify.cc          |  4 ++--
 frontends/verific/verific.cc       |  4 ++--
 frontends/verilog/verilog_lexer.l  |  1 +
 frontends/verilog/verilog_parser.y |  8 +++++++-
 kernel/celltypes.h                 |  1 +
 kernel/rtlil.cc                    | 10 +++++++++-
 kernel/rtlil.h                     |  1 +
 manual/CHAPTER_CellLib.tex         |  2 +-
 passes/hierarchy/hierarchy.cc      |  2 +-
 passes/opt/opt_clean.cc            |  2 +-
 techlibs/common/simlib.v           |  8 ++++++++
 14 files changed, 38 insertions(+), 9 deletions(-)

diff --git a/frontends/ast/ast.cc b/frontends/ast/ast.cc
index 2d58c682f..38a19a36f 100644
--- a/frontends/ast/ast.cc
+++ b/frontends/ast/ast.cc
@@ -84,6 +84,7 @@ std::string AST::type2str(AstNodeType type)
 	X(AST_PREFIX)
 	X(AST_ASSERT)
 	X(AST_ASSUME)
+	X(AST_COVER)
 	X(AST_FCALL)
 	X(AST_TO_BITS)
 	X(AST_TO_SIGNED)
diff --git a/frontends/ast/ast.h b/frontends/ast/ast.h
index cd6e264e6..0b9116d39 100644
--- a/frontends/ast/ast.h
+++ b/frontends/ast/ast.h
@@ -65,6 +65,7 @@ namespace AST
 		AST_PREFIX,
 		AST_ASSERT,
 		AST_ASSUME,
+		AST_COVER,
 
 		AST_FCALL,
 		AST_TO_BITS,
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index db8d7409f..bdac4de00 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -1336,9 +1336,11 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 	// generate $assert cells
 	case AST_ASSERT:
 	case AST_ASSUME:
+	case AST_COVER:
 		{
 			const char *celltype = "$assert";
 			if (type == AST_ASSUME) celltype = "$assume";
+			if (type == AST_COVER) celltype = "$cover";
 
 			log_assert(children.size() == 2);
 
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index c1e77c6ec..eecc04132 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -1400,7 +1400,7 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 	}
 skip_dynamic_range_lvalue_expansion:;
 
-	if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME) && current_block != NULL)
+	if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME || type == AST_COVER) && current_block != NULL)
 	{
 		std::stringstream sstr;
 		sstr << "$formal$" << filename << ":" << linenum << "$" << (autoidx++);
@@ -1462,7 +1462,7 @@ skip_dynamic_range_lvalue_expansion:;
 		goto apply_newNode;
 	}
 
-	if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME) && children.size() == 1)
+	if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME || type == AST_COVER) && children.size() == 1)
 	{
 		children.push_back(mkconst_int(1, false, 1));
 		did_something = true;
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 9bf5a6c6c..f5efdea7e 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -752,8 +752,8 @@ struct VerificImporter
 			}
 
 			if (inst->Type() == PRIM_SVA_IMMEDIATE_COVER || inst->Type() == PRIM_SVA_COVER) {
-				// Net *in = inst->GetInput();
-				// module->addCover(NEW_ID, net_map.at(in), State::S1);
+				Net *in = inst->GetInput();
+				module->addCover(NEW_ID, net_map.at(in), State::S1);
 				continue;
 			}
 
diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index c22fdf39c..4d040e3d1 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -177,6 +177,7 @@ YOSYS_NAMESPACE_END
 
 "assert"   { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); }
 "assume"   { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); }
+"cover"    { if (formal_mode) return TOK_COVER; SV_KEYWORD(TOK_COVER); }
 "restrict" { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); }
 "property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); }
 "logic"    { SV_KEYWORD(TOK_REG); }
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index ba47bf2d3..0f823a082 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -114,7 +114,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 %token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE
 %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED
 %token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME
-%token TOK_RESTRICT TOK_PROPERTY TOK_ENUM TOK_TYPEDEF
+%token TOK_RESTRICT TOK_COVER TOK_PROPERTY TOK_ENUM TOK_TYPEDEF
 
 %type <ast> range range_or_multirange  non_opt_range non_opt_multirange range_or_signed_int
 %type <ast> wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list
@@ -1000,6 +1000,9 @@ assert:
 	TOK_ASSUME '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $3));
 	} |
+	TOK_COVER '(' expr ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, $3));
+	} |
 	TOK_RESTRICT '(' expr ')' ';' {
 		if (norestrict_mode)
 			delete $3;
@@ -1014,6 +1017,9 @@ assert_property:
 	TOK_ASSUME TOK_PROPERTY '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $4));
 	} |
+	TOK_COVER TOK_PROPERTY '(' expr ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, $4));
+	} |
 	TOK_RESTRICT TOK_PROPERTY '(' expr ')' ';' {
 		if (norestrict_mode)
 			delete $4;
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index f0ead1e89..04db5125e 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -116,6 +116,7 @@ struct CellTypes
 
 		setup_type("$assert", {A, EN}, pool<RTLIL::IdString>(), true);
 		setup_type("$assume", {A, EN}, pool<RTLIL::IdString>(), true);
+		setup_type("$cover", {A, EN}, pool<RTLIL::IdString>(), true);
 		setup_type("$initstate", pool<RTLIL::IdString>(), {Y}, true);
 		setup_type("$anyconst", pool<RTLIL::IdString>(), {Y}, true);
 		setup_type("$anyseq", pool<RTLIL::IdString>(), {Y}, true);
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 365bfd9f8..978a7a537 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -1026,7 +1026,7 @@ namespace {
 				return;
 			}
 
-			if (cell->type.in("$assert", "$assume")) {
+			if (cell->type.in("$assert", "$assume", "$cover")) {
 				port("\\A", 1);
 				port("\\EN", 1);
 				check_expected();
@@ -1819,6 +1819,14 @@ RTLIL::Cell* RTLIL::Module::addAssume(RTLIL::IdString name, RTLIL::SigSpec sig_a
 	return cell;
 }
 
+RTLIL::Cell* RTLIL::Module::addCover(RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en)
+{
+	RTLIL::Cell *cell = addCell(name, "$cover");
+	cell->setPort("\\A", sig_a);
+	cell->setPort("\\EN", sig_en);
+	return cell;
+}
+
 RTLIL::Cell* RTLIL::Module::addEquiv(RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_b, RTLIL::SigSpec sig_y)
 {
 	RTLIL::Cell *cell = addCell(name, "$equiv");
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index 8dd8fcca3..7a6f5717d 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -1007,6 +1007,7 @@ public:
 	RTLIL::Cell* addTribuf (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en, RTLIL::SigSpec sig_y);
 	RTLIL::Cell* addAssert (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en);
 	RTLIL::Cell* addAssume (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en);
+	RTLIL::Cell* addCover  (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_en);
 	RTLIL::Cell* addEquiv  (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_b, RTLIL::SigSpec sig_y);
 
 	RTLIL::Cell* addSr    (RTLIL::IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, RTLIL::SigSpec sig_q, bool set_polarity = true, bool clr_polarity = true);
diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex
index a831fdf33..7686f5963 100644
--- a/manual/CHAPTER_CellLib.tex
+++ b/manual/CHAPTER_CellLib.tex
@@ -421,7 +421,7 @@ pass. The combinatorial logic cells can be mapped to physical cells from a Liber
 using the {\tt abc} pass.
 
 \begin{fixme}
-Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$equiv}, {\tt \$initstate}, {\tt \$anyconst}, and {\tt \$anyseq} cells.
+Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$cover}, {\tt \$equiv}, {\tt \$initstate}, {\tt \$anyconst}, and {\tt \$anyseq} cells.
 \end{fixme}
 
 \begin{fixme}
diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index f1c4a1d3b..4786aacaf 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -313,7 +313,7 @@ bool set_keep_assert(std::map<RTLIL::Module*, bool> &cache, RTLIL::Module *mod)
 	if (cache.count(mod) == 0)
 		for (auto c : mod->cells()) {
 			RTLIL::Module *m = mod->design->module(c->type);
-			if ((m != nullptr && set_keep_assert(cache, m)) || c->type.in("$assert", "$assume"))
+			if ((m != nullptr && set_keep_assert(cache, m)) || c->type.in("$assert", "$assume", "$cover"))
 				return cache[mod] = true;
 		}
 	return cache[mod];
diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index 6600ffa25..65944caec 100644
--- a/passes/opt/opt_clean.cc
+++ b/passes/opt/opt_clean.cc
@@ -64,7 +64,7 @@ struct keep_cache_t
 
 	bool query(Cell *cell)
 	{
-		if (cell->type.in("$memwr", "$meminit", "$assert", "$assume"))
+		if (cell->type.in("$memwr", "$meminit", "$assert", "$assume", "$cover"))
 			return true;
 
 		if (cell->has_keep_attr())
diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index 2c4db1ac6..d0abd3b34 100644
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -1305,6 +1305,14 @@ endmodule
 
 // --------------------------------------------------------
 
+module \$cover (A, EN);
+
+input A, EN;
+
+endmodule
+
+// --------------------------------------------------------
+
 module \$initstate (Y);
 
 output reg Y = 1;

From 6abf79eb280a645f5896f307dca7afb92d75d25e Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 4 Feb 2017 17:02:13 +0100
Subject: [PATCH 19/28] Further improve cover() support

---
 README.md                          | 10 +++++-----
 backends/smt2/smt2.cc              |  8 +++++---
 frontends/verilog/verilog_parser.y |  6 ++++++
 3 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/README.md b/README.md
index 9b9f72cc0..221bb0ce1 100644
--- a/README.md
+++ b/README.md
@@ -46,7 +46,7 @@ Getting Started
 
 You need a C++ compiler with C++11 support (up-to-date CLANG or GCC is
 recommended) and some standard tools such as GNU Flex, GNU Bison, and GNU Make.
-TCL, readline and libffi are optional (see ENABLE_* settings in Makefile).
+TCL, readline and libffi are optional (see ``ENABLE_*`` settings in Makefile).
 Xdot (graphviz) is used by the ``show`` command in yosys to display schematics.
 For example on Ubuntu Linux 16.04 LTS the following commands will install all
 prerequisites for building yosys:
@@ -372,8 +372,8 @@ Verilog Attributes and non-standard features
 Non-standard or SystemVerilog features for formal verification
 ==============================================================
 
-- Support for ``assert``, ``assume``, and ``restrict`` is enabled when
-  ``read_verilog`` is called with ``-formal``.
+- Support for ``assert``, ``assume``, ``restrict``, and ``cover'' is enabled
+  when ``read_verilog`` is called with ``-formal``.
 
 - The system task ``$initstate`` evaluates to 1 in the initial state and
   to 0 otherwise.
@@ -400,8 +400,8 @@ from SystemVerilog:
   form. In module context: ``assert property (<expression>);`` and within an
   always block: ``assert(<expression>);``. It is transformed to a $assert cell.
 
-- The ``assume`` and ``restrict`` statements from SystemVerilog are also
-  supported. The same limitations as with the ``assert`` statement apply.
+- The ``assume``, ``restrict``, and ``cover`` statements from SystemVerilog are
+  also supported. The same limitations as with the ``assert`` statement apply.
 
 - The keywords ``always_comb``, ``always_ff`` and ``always_latch``, ``logic``
   and ``bit`` are supported.
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index e0daae728..02661f1cf 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -662,9 +662,9 @@ struct Smt2Worker
 
 		if (verbose) log("=> export logic driving asserts\n");
 
-		vector<string> assert_list, assume_list;
+		vector<string> assert_list, assume_list, cover_list;
 		for (auto cell : module->cells())
-			if (cell->type.in("$assert", "$assume")) {
+			if (cell->type.in("$assert", "$assume", "$cover")) {
 				string name_a = get_bool(cell->getPort("\\A"));
 				string name_en = get_bool(cell->getPort("\\EN"));
 				decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
@@ -673,8 +673,10 @@ struct Smt2Worker
 						get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
 				if (cell->type == "$assert")
 					assert_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
-				else
+				else if (cell->type == "$assume")
 					assume_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
+				else if (cell->type == "$cover")
+					cover_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
 			}
 
 		for (int iter = 1; !registers.empty(); iter++)
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 0f823a082..4fedff5cf 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -1003,6 +1003,12 @@ assert:
 	TOK_COVER '(' expr ')' ';' {
 		ast_stack.back()->children.push_back(new AstNode(AST_COVER, $3));
 	} |
+	TOK_COVER '(' ')' ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false)));
+	} |
+	TOK_COVER ';' {
+		ast_stack.back()->children.push_back(new AstNode(AST_COVER, AstNode::mkconst_int(1, false)));
+	} |
 	TOK_RESTRICT '(' expr ')' ';' {
 		if (norestrict_mode)
 			delete $3;

From 0c0784b6bfa41274d6b9fcd64c4fb061489dd798 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 4 Feb 2017 18:17:08 +0100
Subject: [PATCH 20/28] Partially implement cover() support in yosys-smtbmc

---
 backends/smt2/smt2.cc   |  8 +++-
 backends/smt2/smtbmc.py | 89 ++++++++++++++++++++++++++++++++++++++++-
 backends/smt2/smtio.py  |  4 ++
 3 files changed, 97 insertions(+), 4 deletions(-)

diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 02661f1cf..932f5cd68 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -669,8 +669,12 @@ struct Smt2Worker
 				string name_en = get_bool(cell->getPort("\\EN"));
 				decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
 						cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
-				decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
-						get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
+				if (cell->type == "$cover")
+					decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
+							get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
+				else
+					decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
+							get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
 				if (cell->type == "$assert")
 					assert_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
 				else if (cell->type == "$assume")
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 10875f523..880aa64fa 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -36,6 +36,7 @@ vlogtbfile = None
 inconstr = list()
 outconstr = None
 gentrace = False
+covermode = False
 tempind = False
 dumpall = False
 assume_skipped = None
@@ -61,6 +62,9 @@ yosys-smtbmc [options] <yosys_smt2_output>
     -i
         instead of BMC run temporal induction
 
+    -c
+        instead of regular BMC run cover analysis
+
     -m <module_name>
         name of the top module
 
@@ -120,7 +124,7 @@ yosys-smtbmc [options] <yosys_smt2_output>
 
 
 try:
-    opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igm:", so.longopts +
+    opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
             ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader",
              "dump-vcd=", "dump-vlogtb=", "dump-smtc=", "dump-all", "noinfo", "append="])
 except:
@@ -173,6 +177,8 @@ for o, a in opts:
         tempind = True
     elif o == "-g":
         gentrace = True
+    elif o == "-c":
+        covermode = True
     elif o == "-m":
         topmod = a
     elif so.handle(o, a):
@@ -183,6 +189,8 @@ for o, a in opts:
 if len(args) != 1:
     usage()
 
+if sum([tempind, gentrace, covermode]) > 1:
+    usage()
 
 constr_final_start = None
 constr_asserts = defaultdict(list)
@@ -746,6 +754,24 @@ def print_anyconsts(state):
     print_anyconsts_worker(topmod, "s%d" % state, topmod)
 
 
+def get_cover_list(mod, base):
+    assert mod in smt.modinfo
+
+    cover_expr = list()
+    cover_desc = list()
+
+    for expr, desc in smt.modinfo[mod].covers.items():
+        cover_expr.append("(ite (|%s| %s) #b1 #b0)" % (expr, base))
+        cover_desc.append(desc)
+
+    for cell, submod in smt.modinfo[mod].cells.items():
+        e, d = get_cover_list(submod, "(|%s_h %s| %s)" % (mod, cell, base))
+        cover_expr += e
+        cover_desc += d
+
+    return cover_expr, cover_desc
+
+
 if tempind:
     retstatus = False
     skip_counter = step_size
@@ -793,8 +819,67 @@ if tempind:
             retstatus = True
             break
 
+elif covermode:
+    cover_expr, cover_desc = get_cover_list(topmod, "state")
 
-else:  # not tempind
+    if len(cover_expr) > 1:
+        cover_expr = "(concat %s)" % " ".join(cover_expr)
+    elif len(cover_expr) == 1:
+        cover_expr = cover_expr[0]
+    else:
+        cover_expr = "#b0"
+
+    coveridx = 0
+    smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr))
+
+    step = 0
+    retstatus = False
+
+    assert step_size == 1
+
+    while step < num_steps:
+        smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod))
+        smt.write("(assert (|%s_u| s%d))" % (topmod, step))
+        smt.write("(assert (|%s_h| s%d))" % (topmod, step))
+        smt.write("(assert %s)" % get_constr_expr(constr_assumes, step))
+
+        if step == 0:
+            smt.write("(assert (|%s_i| s0))" % (topmod))
+            smt.write("(assert (|%s_is| s0))" % (topmod))
+
+        else:
+            smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step-1, step))
+            smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
+
+        while True:
+            print_msg("Checking cover reachability in step %d.." % (step))
+            smt.write("(push 1)")
+            smt.write("(assert (distinct (covers_%d s%d) #b%s))" % (coveridx, step, "0" * len(cover_desc)))
+
+            if smt.check_sat() == "unsat":
+                smt.write("(pop 1)")
+                break
+
+            reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
+
+            for i in range(len(reached_covers)):
+                if reached_covers[i] == "0":
+                    continue
+
+                print_msg("  reached cover statement %s." % cover_desc[i])
+
+            write_trace(0, step+1, "%d" % coveridx)
+
+            # TBD
+            assert False
+
+        if len(cover_desc) == 0:
+            retstatus = True
+            break
+
+        step += 1
+
+else:  # not tempind, covermode
     step = 0
     retstatus = True
     while step < num_steps:
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index 3946c3423..dda804efb 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -42,6 +42,7 @@ class SmtModInfo:
         self.wsize = dict()
         self.cells = dict()
         self.asserts = dict()
+        self.covers = dict()
         self.anyconsts = dict()
 
 
@@ -331,6 +332,9 @@ class SmtIo:
         if fields[1] == "yosys-smt2-assert":
             self.modinfo[self.curmod].asserts[fields[2]] = fields[3]
 
+        if fields[1] == "yosys-smt2-cover":
+            self.modinfo[self.curmod].covers[fields[2]] = fields[3]
+
         if fields[1] == "yosys-smt2-anyconst":
             self.modinfo[self.curmod].anyconsts[fields[2]] = fields[3]
 

From adbecfee66e296916074f32d2c812450a15f2ba5 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 4 Feb 2017 21:10:24 +0100
Subject: [PATCH 21/28] Improve yosys-smtbmc cover() support

---
 backends/smt2/smtbmc.py | 24 +++++++++++++++++++-----
 1 file changed, 19 insertions(+), 5 deletions(-)

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 880aa64fa..16ba543e7 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -821,6 +821,7 @@ if tempind:
 
 elif covermode:
     cover_expr, cover_desc = get_cover_list(topmod, "state")
+    cover_mask = "1" * len(cover_desc)
 
     if len(cover_expr) > 1:
         cover_expr = "(concat %s)" % " ".join(cover_expr)
@@ -851,7 +852,7 @@ elif covermode:
             smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step-1, step))
             smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step))
 
-        while True:
+        while "1" in cover_mask:
             print_msg("Checking cover reachability in step %d.." % (step))
             smt.write("(push 1)")
             smt.write("(assert (distinct (covers_%d s%d) #b%s))" % (coveridx, step, "0" * len(cover_desc)))
@@ -861,24 +862,37 @@ elif covermode:
                 break
 
             reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
+            assert len(reached_covers) == len(cover_desc)
+
+            new_cover_mask = []
 
             for i in range(len(reached_covers)):
                 if reached_covers[i] == "0":
+                    new_cover_mask.append(cover_mask[i])
                     continue
 
-                print_msg("  reached cover statement %s." % cover_desc[i])
+                print_msg("Reached cover statement at %s in step %d." % (cover_desc[i], step))
+                new_cover_mask.append("0")
 
             write_trace(0, step+1, "%d" % coveridx)
 
-            # TBD
-            assert False
+            cover_mask = "".join(new_cover_mask)
 
-        if len(cover_desc) == 0:
+            coveridx += 1
+            smt.write("(pop 1)")
+            smt.write("(define-fun covers_%d ((state |%s_s|)) (_ BitVec %d) (bvand (covers_%d state) #b%s))" % (coveridx, topmod, len(cover_desc), coveridx-1, cover_mask))
+
+        if "1" not in cover_mask:
             retstatus = True
             break
 
         step += 1
 
+    if "1" in cover_mask:
+        for i in range(len(cover_mask)):
+            if cover_mask[i] == "1":
+                print_msg("Unreached cover statement at %s." % cover_desc[i])
+
 else:  # not tempind, covermode
     step = 0
     retstatus = True

From 5541b421590e9ab16eef899508bad53494258819 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sat, 4 Feb 2017 21:22:17 +0100
Subject: [PATCH 22/28] Add assert check in "yosys-smtbmc -c"

---
 backends/smt2/smtbmc.py | 35 ++++++++++++++++++++++++++++-------
 1 file changed, 28 insertions(+), 7 deletions(-)

diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index 16ba543e7..d8b47504c 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -713,30 +713,40 @@ def write_trace(steps_start, steps_stop, index):
         write_constr_trace(steps_start, steps_stop, index)
 
 
-def print_failed_asserts_worker(mod, state, path):
+def print_failed_asserts_worker(mod, state, path, extrainfo):
     assert mod in smt.modinfo
+    found_failed_assert = False
 
     if smt.get("(|%s_a| %s)" % (mod, state)) in ["true", "#b1"]:
         return
 
     for cellname, celltype in smt.modinfo[mod].cells.items():
-        print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
+        if print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname, extrainfo):
+            found_failed_assert = True
 
     for assertfun, assertinfo in smt.modinfo[mod].asserts.items():
         if smt.get("(|%s| %s)" % (assertfun, state)) in ["false", "#b0"]:
-            print_msg("Assert failed in %s: %s" % (path, assertinfo))
+            print_msg("Assert failed in %s: %s%s" % (path, assertinfo, extrainfo))
+            found_failed_assert = True
+
+    return found_failed_assert
 
 
-def print_failed_asserts(state, final=False):
+def print_failed_asserts(state, final=False, extrainfo=""):
     if noinfo: return
     loc_list, expr_list, value_list = get_constr_expr(constr_asserts, state, final=final, getvalues=True)
+    found_failed_assert = False
 
     for loc, expr, value in zip(loc_list, expr_list, value_list):
         if smt.bv2int(value) == 0:
-            print_msg("Assert %s failed: %s" % (loc, expr))
+            print_msg("Assert %s failed: %s%s" % (loc, expr, extrainfo))
+            found_failed_assert = True
 
     if not final:
-        print_failed_asserts_worker(topmod, "s%d" % state, topmod)
+        if print_failed_asserts_worker(topmod, "s%d" % state, topmod, extrainfo):
+            found_failed_assert = True
+
+    return found_failed_assert
 
 
 def print_anyconsts_worker(mod, state, path):
@@ -835,6 +845,7 @@ elif covermode:
 
     step = 0
     retstatus = False
+    found_failed_assert = False
 
     assert step_size == 1
 
@@ -874,14 +885,24 @@ elif covermode:
                 print_msg("Reached cover statement at %s in step %d." % (cover_desc[i], step))
                 new_cover_mask.append("0")
 
+            cover_mask = "".join(new_cover_mask)
+
+            for i in range(step+1):
+                if print_failed_asserts(i, extrainfo=" (step %d)" % i):
+                    found_failed_assert = True
+
             write_trace(0, step+1, "%d" % coveridx)
 
-            cover_mask = "".join(new_cover_mask)
+            if found_failed_assert:
+                break
 
             coveridx += 1
             smt.write("(pop 1)")
             smt.write("(define-fun covers_%d ((state |%s_s|)) (_ BitVec %d) (bvand (covers_%d state) #b%s))" % (coveridx, topmod, len(cover_desc), coveridx-1, cover_mask))
 
+        if found_failed_assert:
+            break
+
         if "1" not in cover_mask:
             retstatus = True
             break

From e3a12b57f571423979869b28c4b49f78abe6e2c4 Mon Sep 17 00:00:00 2001
From: Piotr Esden-Tempski <piotr@esden.net>
Date: Tue, 31 Jan 2017 16:00:17 -0800
Subject: [PATCH 23/28] Use -E sed parameter instead of -r.

BSD sed equivalent to -r parameter is -E and it is also supported in GNU
sed thus using -E results in support on both platforms.
---
 manual/clean.sh | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/manual/clean.sh b/manual/clean.sh
index 11c2e7bf2..addc34ed1 100755
--- a/manual/clean.sh
+++ b/manual/clean.sh
@@ -1,2 +1,2 @@
 #!/bin/bash
-for f in $( find . -name .gitignore ); do sed -re "s,^,find ${f%.gitignore} -name ',; s,$,' | xargs rm -f,;" $f; done | bash -v
+for f in $( find . -name .gitignore ); do sed -Ee "s,^,find ${f%.gitignore} -name ',; s,$,' | xargs rm -f,;" $f; done | bash -v

From 19303f63925eef95138c76cddc4e5ef0673b3a47 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 5 Feb 2017 20:04:17 +0100
Subject: [PATCH 24/28] Update ABC to hg rev a2fcd1cc61a6

---
 Makefile | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Makefile b/Makefile
index 2d247a4ca..320eec018 100644
--- a/Makefile
+++ b/Makefile
@@ -86,7 +86,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 = fe96921e5d50
+ABCREV = a2fcd1cc61a6
 ABCPULL = 1
 ABCURL ?= https://bitbucket.org/alanmi/abc
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)"

From aab58045a867a6a7d2998d329a9f20924ab7b8a1 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Sun, 5 Feb 2017 22:43:33 +0100
Subject: [PATCH 25/28] Fix undef propagation bug in $pmux SAT model

---
 kernel/satgen.h | 18 ++++--------------
 1 file changed, 4 insertions(+), 14 deletions(-)

diff --git a/kernel/satgen.h b/kernel/satgen.h
index 690f8e337..25a22fd8a 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -507,11 +507,7 @@ struct SatGen
 				std::vector<int> undef_s = importUndefSigSpec(cell->getPort("\\S"), timestep);
 				std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
 
-				int maybe_one_hot = ez->CONST_FALSE;
-				int maybe_many_hot = ez->CONST_FALSE;
-
-				int sure_one_hot = ez->CONST_FALSE;
-				int sure_many_hot = ez->CONST_FALSE;
+				int maybe_a = ez->CONST_TRUE;
 
 				std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
 				std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
@@ -524,18 +520,12 @@ struct SatGen
 					int maybe_s = ez->OR(s.at(i), undef_s.at(i));
 					int sure_s = ez->AND(s.at(i), ez->NOT(undef_s.at(i)));
 
-					maybe_one_hot = ez->OR(maybe_one_hot, maybe_s);
-					maybe_many_hot = ez->OR(maybe_many_hot, ez->AND(maybe_one_hot, maybe_s));
+					maybe_a = ez->AND(maybe_a, ez->NOT(sure_s));
 
-					sure_one_hot = ez->OR(sure_one_hot, sure_s);
-					sure_many_hot = ez->OR(sure_many_hot, ez->AND(sure_one_hot, sure_s));
-
-					bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b))), bits_set);
-					bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b))), bits_clr);
+					bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b)), bits_set);
+					bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b)), bits_clr);
 				}
 
-				int maybe_a = ez->NOT(maybe_one_hot);
-
 				bits_set = ez->vec_ite(maybe_a, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(a, undef_a))), bits_set);
 				bits_clr = ez->vec_ite(maybe_a, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(a), undef_a))), bits_clr);
 

From 7e0b776a793f648bed3338dfbc6b25bc1c24e873 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Mon, 6 Feb 2017 14:48:03 +0100
Subject: [PATCH 26/28] Add "read_blif -wideports"

---
 frontends/blif/blifparse.cc | 79 +++++++++++++++++++++++++++++++++++--
 frontends/blif/blifparse.h  |  3 +-
 2 files changed, 77 insertions(+), 5 deletions(-)

diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc
index 6d4d60870..f610a25c3 100644
--- a/frontends/blif/blifparse.cc
+++ b/frontends/blif/blifparse.cc
@@ -55,7 +55,30 @@ static bool read_next_line(char *&buffer, size_t &buffer_size, int &line_count,
 	}
 }
 
-void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bool run_clean, bool sop_mode)
+static std::pair<RTLIL::IdString, int> wideports_split(std::string name)
+{
+	int pos = -1;
+
+	if (name.empty() || name.back() != ']')
+		goto failed;
+
+	for (int i = 0; i+1 < GetSize(name); i++) {
+		if (name[i] == '[')
+			pos = i;
+		else if (name[i] < '0' || name[i] > '9')
+			pos = -1;
+		else if (i == pos+1 && name[i] == '0')
+			pos = -1;
+	}
+
+	if (pos >= 0)
+		return std::pair<RTLIL::IdString, int>("\\" + name.substr(0, pos), atoi(name.c_str() + pos+1)+1);
+
+failed:
+	return std::pair<RTLIL::IdString, int>("\\" + name, 0);
+}
+
+void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bool run_clean, bool sop_mode, bool wideports)
 {
 	RTLIL::Module *module = nullptr;
 	RTLIL::Const *lutptr = NULL;
@@ -96,6 +119,8 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 	dict<RTLIL::IdString, RTLIL::Const> *obj_attributes = nullptr;
 	dict<RTLIL::IdString, RTLIL::Const> *obj_parameters = nullptr;
 
+	dict<RTLIL::IdString, std::pair<int, bool>> wideports_cache;
+
 	size_t buffer_size = 4096;
 	char *buffer = (char*)malloc(buffer_size);
 	int line_count = 0;
@@ -148,7 +173,32 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 
 			if (!strcmp(cmd, ".end"))
 			{
+				for (auto &wp : wideports_cache)
+				{
+					auto name = wp.first;
+					int width = wp.second.first;
+					bool isinput = wp.second.second;
+
+					RTLIL::Wire *wire = module->addWire(name, width);
+					wire->port_input = isinput;
+					wire->port_output = !isinput;
+
+					for (int i = 0; i < width; i++) {
+						RTLIL::IdString other_name = name.str() + stringf("[%d]", i);
+						RTLIL::Wire *other_wire = module->wire(other_name);
+						if (other_wire) {
+							other_wire->port_input = false;
+							other_wire->port_output = false;
+							if (isinput)
+								module->connect(other_wire, SigSpec(wire, i));
+							else
+								module->connect(SigSpec(wire, i), other_wire);
+						}
+					}
+				}
+
 				module->fixup_ports();
+				wideports_cache.clear();
 
 				if (run_clean)
 				{
@@ -187,9 +237,11 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 				continue;
 			}
 
-			if (!strcmp(cmd, ".inputs") || !strcmp(cmd, ".outputs")) {
+			if (!strcmp(cmd, ".inputs") || !strcmp(cmd, ".outputs"))
+			{
 				char *p;
-				while ((p = strtok(NULL, " \t\r\n")) != NULL) {
+				while ((p = strtok(NULL, " \t\r\n")) != NULL)
+				{
 					RTLIL::IdString wire_name(stringf("\\%s", p));
 					RTLIL::Wire *wire = module->wire(wire_name);
 					if (wire == nullptr)
@@ -198,6 +250,14 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 						wire->port_input = true;
 					else
 						wire->port_output = true;
+
+					if (wideports) {
+						std::pair<RTLIL::IdString, int> wp = wideports_split(p);
+						if (wp.second > 0) {
+							wideports_cache[wp.first].first = std::max(wideports_cache[wp.first].first, wp.second);
+							wideports_cache[wp.first].second = !strcmp(cmd, ".inputs");
+						}
+					}
 				}
 				obj_attributes = nullptr;
 				obj_parameters = nullptr;
@@ -452,6 +512,8 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo
 		}
 	}
 
+	return;
+
 error:
 	log_error("Syntax error in line %d!\n", line_count);
 }
@@ -469,10 +531,15 @@ struct BlifFrontend : public Frontend {
 		log("    -sop\n");
 		log("        Create $sop cells instead of $lut cells\n");
 		log("\n");
+		log("    -wideports\n");
+		log("        Merge ports that match the pattern 'name[int]' into a single\n");
+		log("        multi-bit port 'name'.\n");
+		log("\n");
 	}
 	virtual void execute(std::istream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
 	{
 		bool sop_mode = false;
+		bool wideports = false;
 
 		log_header(design, "Executing BLIF frontend.\n");
 
@@ -483,11 +550,15 @@ struct BlifFrontend : public Frontend {
 				sop_mode = true;
 				continue;
 			}
+			if (arg == "-wideports") {
+				wideports = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(f, filename, args, argidx);
 
-		parse_blif(design, *f, "", true, sop_mode);
+		parse_blif(design, *f, "", true, sop_mode, wideports);
 	}
 } BlifFrontend;
 
diff --git a/frontends/blif/blifparse.h b/frontends/blif/blifparse.h
index 058087d81..955b6aacf 100644
--- a/frontends/blif/blifparse.h
+++ b/frontends/blif/blifparse.h
@@ -24,7 +24,8 @@
 
 YOSYS_NAMESPACE_BEGIN
 
-extern void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bool run_clean = false, bool sop_mode = false);
+extern void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name,
+		bool run_clean = false, bool sop_mode = false, bool wideports = false);
 
 YOSYS_NAMESPACE_END
 

From 1d1f56a3617dcee6d856a29d1d8576969bf8dce5 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 8 Feb 2017 10:40:33 +0100
Subject: [PATCH 27/28] Add PSL parser mode to verific front-end

---
 frontends/verific/verific.cc | 19 +++++++++++++++++--
 1 file changed, 17 insertions(+), 2 deletions(-)

diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index f5efdea7e..f3b997dc5 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -888,12 +888,12 @@ struct VerificPass : public Pass {
 	{
 		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 		log("\n");
-		log("    verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv} <verilog-file>..\n");
+		log("    verific {-vlog95|-vlog2k|-sv2005|-sv2009|-sv|-vlpsl} <verilog-file>..\n");
 		log("\n");
 		log("Load the specified Verilog/SystemVerilog files into Verific.\n");
 		log("\n");
 		log("\n");
-		log("    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008} <vhdl-file>..\n");
+		log("    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdpsl} <vhdl-file>..\n");
 		log("\n");
 		log("Load the specified VHDL files into Verific.\n");
 		log("\n");
@@ -950,6 +950,13 @@ struct VerificPass : public Pass {
 			return;
 		}
 
+		if (args.size() > 1 && args[1] == "-vlpsl") {
+			for (size_t argidx = 2; argidx < args.size(); argidx++)
+				if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_PSL))
+					log_cmd_error("Reading `%s' in VERILOG_PSL mode failed.\n", args[argidx].c_str());
+			return;
+		}
+
 		if (args.size() > 1 && args[1] == "-vhdl87") {
 			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str());
 			for (size_t argidx = 2; argidx < args.size(); argidx++)
@@ -982,6 +989,14 @@ struct VerificPass : public Pass {
 			return;
 		}
 
+		if (args.size() > 1 && args[1] == "-vhdpsl") {
+			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
+			for (size_t argidx = 2; argidx < args.size(); argidx++)
+				if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_PSL))
+					log_cmd_error("Reading `%s' in VHDL_PSL mode failed.\n", args[argidx].c_str());
+			return;
+		}
+
 		if (args.size() > 1 && args[1] == "-import")
 		{
 			std::set<Netlist*> nl_todo, nl_done;

From ef4a28e112be10d3d62395f68e53e8b7e42dbf68 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Wed, 8 Feb 2017 14:38:15 +0100
Subject: [PATCH 28/28] Add SV "rand" and "const rand" support

---
 README.md                          |  7 +++++--
 frontends/verilog/verilog_lexer.l  |  6 ++++--
 frontends/verilog/verilog_parser.y | 30 ++++++++++++++++++++++++------
 3 files changed, 33 insertions(+), 10 deletions(-)

diff --git a/README.md b/README.md
index 221bb0ce1..396189d5f 100644
--- a/README.md
+++ b/README.md
@@ -378,10 +378,11 @@ Non-standard or SystemVerilog features for formal verification
 - The system task ``$initstate`` evaluates to 1 in the initial state and
   to 0 otherwise.
 
-- The system task ``$anyconst`` evaluates to any constant value.
+- The system task ``$anyconst`` evaluates to any constant value. This is
+  equivalent to declaring a reg as ``const rand``.
 
 - The system task ``$anyseq`` evaluates to any value, possibly a different
-  value in each cycle.
+  value in each cycle. This is equivalent to declaring a reg as ``rand``.
 
 - The SystemVerilog tasks ``$past``, ``$stable``, ``$rose`` and ``$fell`` are
   supported in any clocked block.
@@ -406,6 +407,8 @@ from SystemVerilog:
 - The keywords ``always_comb``, ``always_ff`` and ``always_latch``, ``logic``
   and ``bit`` are supported.
 
+- Declaring free variables with ``rand`` and ``const rand`` is supported.
+
 - SystemVerilog packages are supported. Once a SystemVerilog file is read
   into a design with ``read_verilog``, all its packages are available to
   SystemVerilog files being read into the same design afterwards.
diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index 4d040e3d1..97af0ae2d 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -180,6 +180,8 @@ YOSYS_NAMESPACE_END
 "cover"    { if (formal_mode) return TOK_COVER; SV_KEYWORD(TOK_COVER); }
 "restrict" { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); }
 "property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); }
+"rand"     { if (formal_mode) return TOK_RAND; SV_KEYWORD(TOK_RAND); }
+"const"    { if (formal_mode) return TOK_CONST; SV_KEYWORD(TOK_CONST); }
 "logic"    { SV_KEYWORD(TOK_REG); }
 "bit"      { SV_KEYWORD(TOK_REG); }
 
@@ -198,12 +200,12 @@ YOSYS_NAMESPACE_END
 
 [0-9][0-9_]* {
 	frontend_verilog_yylval.string = new std::string(yytext);
-	return TOK_CONST;
+	return TOK_CONSTVAL;
 }
 
 [0-9]*[ \t]*\'s?[bodhBODH][ \t\r\n]*[0-9a-fA-FzxZX?_]+ {
 	frontend_verilog_yylval.string = new std::string(yytext);
-	return TOK_CONST;
+	return TOK_CONSTVAL;
 }
 
 [0-9][0-9_]*\.[0-9][0-9_]*([eE][-+]?[0-9_]+)? {
diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y
index 4fedff5cf..3eb03dfd8 100644
--- a/frontends/verilog/verilog_parser.y
+++ b/frontends/verilog/verilog_parser.y
@@ -59,6 +59,7 @@ namespace VERILOG_FRONTEND {
 	bool default_nettype_wire;
 	bool sv_mode, formal_mode, lib_mode;
 	bool norestrict_mode, assume_asserts_mode;
+	bool current_wire_rand, current_wire_const;
 	std::istream *lexin;
 }
 YOSYS_NAMESPACE_END
@@ -100,7 +101,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 	bool boolean;
 }
 
-%token <string> TOK_STRING TOK_ID TOK_CONST TOK_REALVAL TOK_PRIMITIVE
+%token <string> TOK_STRING TOK_ID TOK_CONSTVAL TOK_REALVAL TOK_PRIMITIVE
 %token ATTR_BEGIN ATTR_END DEFATTR_BEGIN DEFATTR_END
 %token TOK_MODULE TOK_ENDMODULE TOK_PARAMETER TOK_LOCALPARAM TOK_DEFPARAM
 %token TOK_PACKAGE TOK_ENDPACKAGE TOK_PACKAGESEP
@@ -115,6 +116,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED
 %token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME
 %token TOK_RESTRICT TOK_COVER TOK_PROPERTY TOK_ENUM TOK_TYPEDEF
+%token TOK_RAND TOK_CONST
 
 %type <ast> range range_or_multirange  non_opt_range non_opt_multirange range_or_signed_int
 %type <ast> wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list
@@ -355,6 +357,8 @@ delay:
 wire_type:
 	{
 		astbuf3 = new AstNode(AST_WIRE);
+		current_wire_rand = false;
+		current_wire_const = false;
 	} wire_type_token_list delay {
 		$$ = astbuf3;
 	};
@@ -392,6 +396,12 @@ wire_type_token:
 	} |
 	TOK_SIGNED {
 		astbuf3->is_signed = true;
+	} |
+	TOK_RAND {
+		current_wire_rand = true;
+	} |
+	TOK_CONST {
+		current_wire_const = true;
 	};
 
 non_opt_range:
@@ -730,7 +740,15 @@ wire_name_list:
 	wire_name_and_opt_assign | wire_name_list ',' wire_name_and_opt_assign;
 
 wire_name_and_opt_assign:
-	wire_name |
+	wire_name {
+		if (current_wire_rand) {
+			AstNode *wire = new AstNode(AST_IDENTIFIER);
+			AstNode *fcall = new AstNode(AST_FCALL);
+			wire->str = ast_stack.back()->children.back()->str;
+			fcall->str = current_wire_const ? "\\$anyconst" : "\\$anyseq";
+			ast_stack.back()->children.push_back(new AstNode(AST_ASSIGN, wire, fcall));
+		}
+	} |
 	wire_name '=' expr {
 		AstNode *wire = new AstNode(AST_IDENTIFIER);
 		wire->str = ast_stack.back()->children.back()->str;
@@ -1362,7 +1380,7 @@ basic_expr:
 	rvalue {
 		$$ = $1;
 	} |
-	'(' expr ')' TOK_CONST {
+	'(' expr ')' TOK_CONSTVAL {
 		if ($4->substr(0, 1) != "'")
 			frontend_verilog_yyerror("Syntax error.");
 		AstNode *bits = $2;
@@ -1372,7 +1390,7 @@ basic_expr:
 		$$ = new AstNode(AST_TO_BITS, bits, val);
 		delete $4;
 	} |
-	hierarchical_id TOK_CONST {
+	hierarchical_id TOK_CONSTVAL {
 		if ($2->substr(0, 1) != "'")
 			frontend_verilog_yyerror("Syntax error.");
 		AstNode *bits = new AstNode(AST_IDENTIFIER);
@@ -1384,14 +1402,14 @@ basic_expr:
 		delete $1;
 		delete $2;
 	} |
-	TOK_CONST TOK_CONST {
+	TOK_CONSTVAL TOK_CONSTVAL {
 		$$ = const2ast(*$1 + *$2, case_type_stack.size() == 0 ? 0 : case_type_stack.back(), !lib_mode);
 		if ($$ == NULL || (*$2)[0] != '\'')
 			log_error("Value conversion failed: `%s%s'\n", $1->c_str(), $2->c_str());
 		delete $1;
 		delete $2;
 	} |
-	TOK_CONST {
+	TOK_CONSTVAL {
 		$$ = const2ast(*$1, case_type_stack.size() == 0 ? 0 : case_type_stack.back(), !lib_mode);
 		if ($$ == NULL)
 			log_error("Value conversion failed: `%s'\n", $1->c_str());