Merge https://github.com/cliffordwolf/yosys

25 files changed, 588 insertions, 449 deletions

diff --git a/.travis.yml b/.travis.yml
index d8cd5b298..1c08c21a8 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -29,8 +29,8 @@ before_install:
   - (cd iverilog && autoconf && ./configure --prefix=$HOME/iverilog && make && make install)
   - export PATH=$PATH:$HOME/iverilog/bin
 compiler:
-#  - clang
+# - clang
   - gcc
 os:
   - linux
-  - osx
+# - osx
diff --git a/COPYING b/COPYING
new file mode 100644
index 000000000..a01b7b697
--- /dev/null
+++ b/COPYING
@@ -0,0 +1,13 @@
+Copyright (C) 2012 - 2017  Clifford Wolf <clifford@clifford.at>
+
+Permission to use, copy, modify, and/or distribute this software for any
+purpose with or without fee is hereby granted, provided that the above
+copyright notice and this permission notice appear in all copies.
+
+THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
diff --git a/Makefile b/Makefile
index 393701019..924fd88b7 100644
--- a/Makefile
+++ b/Makefile
@@ -11,12 +11,14 @@ ENABLE_TCL := 1
 ENABLE_ABC := 1
 ENABLE_PLUGINS := 1
 ENABLE_READLINE := 1
+ENABLE_EDITLINE := 0
 ENABLE_VERIFIC := 0
 ENABLE_COVER := 1
 ENABLE_LIBYOSYS := 0
 
 # other configuration flags
 ENABLE_GPROF := 0
+ENABLE_DEBUG := 0
 ENABLE_NDEBUG := 0
 LINK_CURSES := 0
 LINK_TERMCAP := 0
@@ -99,7 +101,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 = 0fc1803a77c0
+ABCREV = f6838749f234
 ABCPULL = 1
 ABCURL ?= https://bitbucket.org/alanmi/abc
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1
@@ -225,6 +227,11 @@ endif
 ifeq ($(CONFIG),mxe)
 LDLIBS += -ltermcap
 endif
+else
+ifeq ($(ENABLE_EDITLINE),1)
+CXXFLAGS += -DYOSYS_ENABLE_EDITLINE
+LDLIBS += -ledit -ltinfo -lbsd
+endif
 endif
 
 ifeq ($(ENABLE_PLUGINS),1)
@@ -251,7 +258,15 @@ LDFLAGS += -pg
 endif
 
 ifeq ($(ENABLE_NDEBUG),1)
-CXXFLAGS := -O3 -DNDEBUG $(filter-out -Os,$(CXXFLAGS))
+CXXFLAGS := -O3 -DNDEBUG $(filter-out -Os -ggdb,$(CXXFLAGS))
+endif
+
+ifeq ($(ENABLE_DEBUG),1)
+ifeq ($(CONFIG),clang)
+CXXFLAGS := -O0 $(filter-out -Os,$(CXXFLAGS))
+else
+CXXFLAGS := -Og $(filter-out -Os,$(CXXFLAGS))
+endif
 endif
 
 ifeq ($(ENABLE_ABC),1)
diff --git a/README.md b/README.md
index 514e32b35..92dc68a6a 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,7 @@
 ```
 yosys -- Yosys Open SYnthesis Suite
 
-Copyright (C) 2012 - 2016  Clifford Wolf <clifford@clifford.at>
+Copyright (C) 2012 - 2017  Clifford Wolf <clifford@clifford.at>
 
 Permission to use, copy, modify, and/or distribute this software for any
 purpose with or without fee is hereby granted, provided that the above
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index dce7c25de..8daa52eb3 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -811,6 +811,9 @@ struct Smt2Worker
 				Module *m = module->design->module(cell->type);
 				log_assert(m != nullptr);
 
+				hier.push_back(stringf("  (= (|%s_is| state) (|%s_is| %s))\n",
+						get_id(module), get_id(cell->type), cell_state.c_str()));
+
 				for (auto &conn : cell->connections())
 				{
 					Wire *w = m->wire(conn.first);
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index c8151c266..d9b79e26e 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -644,6 +644,9 @@ def write_vcd_trace(steps_start, steps_stop, index):
                 data = ["x"] * width
                 gotread = False
 
+                if len(wdata) == 0 and len(rdata) != 0:
+                    wdata = [[]] * len(rdata)
+
                 assert len(rdata) == len(wdata)
 
                 for i in range(len(wdata)):
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index abf8e812d..61ac14c82 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -20,6 +20,8 @@ import sys, subprocess, re, os
 from copy import deepcopy
 from select import select
 from time import time
+from queue import Queue, Empty
+from threading import Thread
 
 
 hex_dict = {
@@ -126,7 +128,7 @@ class SmtIo:
             if self.dummy_file is not None:
                 self.dummy_fd = open(self.dummy_file, "w")
             if not self.noincr:
-                self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+                self.p_open()
 
         if self.unroll:
             self.logic_uf = False
@@ -209,6 +211,57 @@ class SmtIo:
 
         return stmt
 
+    def p_thread_main(self):
+        while True:
+            data = self.p.stdout.readline().decode("ascii")
+            if data == "": break
+            self.p_queue.put(data)
+        self.p_running = False
+
+    def p_open(self):
+        assert self.p is None
+        self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+        self.p_running = True
+        self.p_next = None
+        self.p_queue = Queue()
+        self.p_thread = Thread(target=self.p_thread_main)
+        self.p_thread.start()
+
+    def p_write(self, data, flush):
+        assert self.p is not None
+        self.p.stdin.write(bytes(data, "ascii"))
+        if flush: self.p.stdin.flush()
+
+    def p_read(self):
+        assert self.p is not None
+        assert self.p_running
+        if self.p_next is not None:
+            data = self.p_next
+            self.p_next = None
+            return data
+        return self.p_queue.get()
+
+    def p_poll(self):
+        assert self.p is not None
+        assert self.p_running
+        if self.p_next is not None:
+            return False
+        try:
+            self.p_next = self.p_queue.get(True, 0.1)
+            return False
+        except Empty:
+            return True
+
+    def p_close(self):
+        assert self.p is not None
+        self.p.stdin.close()
+        self.p_thread.join()
+        assert not self.p_running
+        self.p = None
+        self.p_next = None
+        self.p_queue = None
+        self.p_thread = None
+
     def write(self, stmt, unroll=True):
         if stmt.startswith(";"):
             self.info(stmt)
@@ -281,20 +334,17 @@ class SmtIo:
         if self.solver != "dummy":
             if self.noincr:
                 if self.p is not None and not stmt.startswith("(get-"):
-                    self.p.stdin.close()
-                    self.p = None
+                    self.p_close()
                 if stmt == "(push 1)":
                     self.smt2cache.append(list())
                 elif stmt == "(pop 1)":
                     self.smt2cache.pop()
                 else:
                     if self.p is not None:
-                        self.p.stdin.write(bytes(stmt + "\n", "ascii"))
-                        self.p.stdin.flush()
+                        self.p_write(stmt + "\n", True)
                     self.smt2cache[-1].append(stmt)
             else:
-                self.p.stdin.write(bytes(stmt + "\n", "ascii"))
-                self.p.stdin.flush()
+                self.p_write(stmt + "\n", True)
 
     def info(self, stmt):
         if not stmt.startswith("; yosys-smt2-"):
@@ -408,7 +458,7 @@ class SmtIo:
             if self.solver == "dummy":
                 line = self.dummy_fd.readline().strip()
             else:
-                line = self.p.stdout.readline().decode("ascii").strip()
+                line = self.p_read().strip()
                 if self.dummy_file is not None:
                     self.dummy_fd.write(line + "\n")
 
@@ -441,15 +491,13 @@ class SmtIo:
         if self.solver != "dummy":
             if self.noincr:
                 if self.p is not None:
-                    self.p.stdin.close()
-                    self.p = None
-                self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+                    self.p_close()
+                self.p_open()
                 for cache_ctx in self.smt2cache:
                     for cache_stmt in cache_ctx:
-                        self.p.stdin.write(bytes(cache_stmt + "\n", "ascii"))
+                        self.p_write(cache_stmt + "\n", False)
 
-            self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
-            self.p.stdin.flush()
+            self.p_write("(check-sat)\n", True)
 
             if self.timeinfo:
                 i = 0
@@ -457,7 +505,7 @@ class SmtIo:
 
                 count = 0
                 num_bs = 0
-                while select([self.p.stdout], [], [], 0.1) == ([], [], []):
+                while self.p_poll():
                     count += 1
 
                     if count < 25:
@@ -672,6 +720,7 @@ class SmtIo:
     def wait(self):
         if self.p is not None:
             self.p.wait()
+            self.p_close()
 
 
 class SmtOpts:
diff --git a/examples/osu035/Makefile b/examples/osu035/Makefile
index 8d8e247e3..2bb8162b3 100644
--- a/examples/osu035/Makefile
+++ b/examples/osu035/Makefile
@@ -1,5 +1,5 @@
 
-example.edif: example.ys example.v osu035_stdcells.lib
+example.edif: example.ys example.v example.constr osu035_stdcells.lib
 	yosys -l example.yslog -q example.ys
 
 osu035_stdcells.lib:
diff --git a/examples/osu035/example.constr b/examples/osu035/example.constr
new file mode 100644
index 000000000..eb2c6e8d5
--- /dev/null
+++ b/examples/osu035/example.constr
@@ -0,0 +1,2 @@
+set_driving_cell INVX1
+set_load 0.015
diff --git a/examples/osu035/example.ys b/examples/osu035/example.ys
index 040f776a6..6821ef426 100644
--- a/examples/osu035/example.ys
+++ b/examples/osu035/example.ys
@@ -4,7 +4,7 @@ read_liberty -lib osu035_stdcells.lib
 synth -top top
 
 dfflibmap -liberty osu035_stdcells.lib
-abc -liberty osu035_stdcells.lib
+abc -D 10000 -constr example.constr -liberty osu035_stdcells.lib
 opt_clean
 
 stat -liberty osu035_stdcells.lib
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index cd2120b8c..74e7b4675 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -405,9 +405,13 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
 		current_always_clocked = false;
 
 		if (type == AST_ALWAYS)
-			for (auto child : children)
+			for (auto child : children) {
 				if (child->type == AST_POSEDGE || child->type == AST_NEGEDGE)
 					current_always_clocked = true;
+				if (child->type == AST_EDGE && GetSize(child->children) == 1 &&
+						child->children[0]->type == AST_IDENTIFIER && child->children[0]->str == "\\$global_clock")
+					current_always_clocked = true;
+			}
 	}
 
 	int backup_width_hint = width_hint;
@@ -1824,21 +1828,6 @@ skip_dynamic_range_lvalue_expansion:;
 				goto apply_newNode;
 			}
 
-			if (str == "\\$rose" || str == "\\$fell")
-			{
-				if (GetSize(children) != 1)
-					log_error("System function %s got %d arguments, expected 1 at %s:%d.\n",
-							RTLIL::unescape_id(str).c_str(), int(children.size()), filename.c_str(), linenum);
-
-				if (!current_always_clocked)
-					log_error("System function %s is only allowed in clocked blocks at %s:%d.\n",
-							RTLIL::unescape_id(str).c_str(), filename.c_str(), linenum);
-
-				newNode = new AstNode(AST_EQ, children.at(0)->clone(), clone());
-				newNode->children.at(1)->str = "\\$past";
-				goto apply_newNode;
-			}
-
 			// $anyconst and $anyseq are mapped in AstNode::genRTLIL()
 			if (str == "\\$anyconst" || str == "\\$anyseq") {
 				recursion_counter--;
diff --git a/frontends/verific/README b/frontends/verific/README
index e747255db..b4c436a3a 100644
--- a/frontends/verific/README
+++ b/frontends/verific/README
@@ -33,6 +33,13 @@ make -j8
 ./yosys -p 'verific -sv frontends/verific/example.sv; verific -import top'
 
 
+Verific Features that should be enabled in your Verific library
+===============================================================
+
+database/DBCompileFlags.h:
+	DB_PRESERVE_INITIAL_VALUE
+
+
 Testing Verific+Yosys+SymbiYosys for formal verification
 ========================================================
 
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index ae39f7c9d..54210f98a 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -99,11 +99,14 @@ struct VerificImporter;
 void import_sva_assert(VerificImporter *importer, Instance *inst);
 void import_sva_assume(VerificImporter *importer, Instance *inst);
 void import_sva_cover(VerificImporter *importer, Instance *inst);
+void svapp_assert(VerificImporter *importer, Instance *inst);
+void svapp_assume(VerificImporter *importer, Instance *inst);
+void svapp_cover(VerificImporter *importer, Instance *inst);
 
 struct VerificClockEdge {
-	Net *clock_net;
-	SigBit clock_sig;
-	bool posedge;
+	Net *clock_net = nullptr;
+	SigBit clock_sig = State::Sx;
+	bool posedge = false;
 	VerificClockEdge(VerificImporter *importer, Instance *inst);
 };
 
@@ -115,14 +118,13 @@ struct VerificImporter
 	std::map<Net*, RTLIL::SigBit> net_map;
 	std::map<Net*, Net*> sva_posedge_map;
 
-	bool mode_gates, mode_keep, mode_nosva, mode_names, verbose;
+	bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose;
 
 	pool<int> verific_sva_prims;
-	pool<int> verific_psl_prims;
 
-	VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool verbose) :
-			mode_gates(mode_gates), mode_keep(mode_keep),
-			mode_nosva(mode_nosva), mode_names(mode_names), verbose(verbose)
+	VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) :
+			mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
+			mode_nosvapp(mode_nosvapp), mode_names(mode_names), verbose(verbose)
 	{
 		// Copy&paste from Verific 3.16_484_32_170630 Netlist.h
 		vector<int> sva_prims {
@@ -149,29 +151,6 @@ struct VerificImporter
 
 		for (int p : sva_prims)
 			verific_sva_prims.insert(p);
-
-		// Copy&paste from Verific 3.16_484_32_170630 Netlist.h
-		vector<int> psl_prims {
-			OPER_PSLPREV, OPER_PSLNEXTFUNC, PRIM_PSL_ASSERT, PRIM_PSL_ASSUME,
-			PRIM_PSL_ASSUME_GUARANTEE, PRIM_PSL_RESTRICT, PRIM_PSL_RESTRICT_GUARANTEE,
-			PRIM_PSL_COVER, PRIM_ENDPOINT,  PRIM_ROSE, PRIM_FELL, PRIM_AT, PRIM_ATSTRONG,
-			PRIM_ABORT, PRIM_PSL_NOT, PRIM_PSL_AND, PRIM_PSL_OR, PRIM_IMPL, PRIM_EQUIV,
-			PRIM_PSL_X, PRIM_PSL_XSTRONG, PRIM_PSL_G, PRIM_PSL_F, PRIM_PSL_U, PRIM_PSL_W,
-			PRIM_NEXT, PRIM_NEXTSTRONG, PRIM_ALWAYS, PRIM_NEVER, PRIM_EVENTUALLY,
-			PRIM_UNTIL, PRIM_UNTIL_, PRIM_UNTILSTRONG, PRIM_UNTILSTRONG_, PRIM_BEFORE,
-			PRIM_BEFORE_, PRIM_BEFORESTRONG, PRIM_BEFORESTRONG_, PRIM_NEXT_A,
-			PRIM_NEXT_ASTRONG, PRIM_NEXT_E, PRIM_NEXT_ESTRONG, PRIM_NEXT_EVENT,
-			PRIM_NEXT_EVENTSTRONG, PRIM_NEXT_EVENT_A, PRIM_NEXT_EVENT_ASTRONG,
-			PRIM_NEXT_EVENT_E, PRIM_NEXT_EVENT_ESTRONG, PRIM_SEQ_IMPL, PRIM_OSUFFIX_IMPL,
-			PRIM_SUFFIX_IMPL, PRIM_OSUFFIX_IMPLSTRONG, PRIM_SUFFIX_IMPLSTRONG, PRIM_WITHIN,
-			PRIM_WITHIN_, PRIM_WITHINSTRONG, PRIM_WITHINSTRONG_, PRIM_WHILENOT,
-			PRIM_WHILENOT_, PRIM_WHILENOTSTRONG, PRIM_WHILENOTSTRONG_, PRIM_CONCAT,
-			PRIM_FUSION, PRIM_SEQ_AND_LEN, PRIM_SEQ_AND, PRIM_SEQ_OR, PRIM_CONS_REP,
-			PRIM_NONCONS_REP, PRIM_GOTO_REP
-		};
-
-		for (int p : psl_prims)
-			verific_psl_prims.insert(p);
 	}
 
 	RTLIL::SigBit net_map_at(Net *net)
@@ -1123,20 +1102,20 @@ struct VerificImporter
 			if (!mode_gates) {
 				if (import_netlist_instance_cells(inst, inst_name))
 					continue;
-				if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()) && !verific_psl_prims.count(inst->Type()))
+				if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()))
 					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, inst_name))
 					continue;
 			}
 
-			if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_PSL_ASSERT)
+			if (inst->Type() == PRIM_SVA_ASSERT)
 				sva_asserts.insert(inst);
 
-			if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_PSL_ASSUME)
+			if (inst->Type() == PRIM_SVA_ASSUME)
 				sva_assumes.insert(inst);
 
-			if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_PSL_COVER)
+			if (inst->Type() == PRIM_SVA_COVER)
 				sva_covers.insert(inst);
 
 			if (inst->Type() == PRIM_SVA_PAST && !mode_nosva)
@@ -1156,38 +1135,9 @@ struct VerificImporter
 					continue;
 			}
 
-			if (inst->Type() == OPER_PSLPREV && !mode_nosva)
-			{
-				Net *clock = inst->GetClock();
-
-				if (!clock->IsConstant())
-				{
-					VerificClockEdge clock_edge(this, clock->Driver());
-
-					SigSpec sig_d, sig_q;
-
-					for (int i = 0; i < int(inst->InputSize()); i++) {
-						sig_d.append(net_map_at(inst->GetInputBit(i)));
-						sig_q.append(net_map_at(inst->GetOutputBit(i)));
-					}
-
-					if (verbose)
-						log("    %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
-								log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
-
-					RTLIL::Cell *ff = module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
-
-					if (inst->InputSize() == 1)
-						past_ffs.insert(ff);
-
-					if (!mode_keep)
-						continue;
-				}
-			}
-
-			if (!mode_keep && (verific_sva_prims.count(inst->Type()) || verific_psl_prims.count(inst->Type()))) {
+			if (!mode_keep && verific_sva_prims.count(inst->Type())) {
 				if (verbose)
-					log("    skipping SVA/PSL cell in non k-mode\n");
+					log("    skipping SVA cell in non k-mode\n");
 				continue;
 			}
 
@@ -1199,7 +1149,7 @@ struct VerificImporter
 				if (!mode_keep)
 					log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
 
-				if (!verific_sva_prims.count(inst->Type()) && !verific_psl_prims.count(inst->Type()))
+				if (!verific_sva_prims.count(inst->Type()))
 					log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
 			}
 
@@ -1246,6 +1196,18 @@ struct VerificImporter
 			}
 		}
 
+		if (!mode_nosvapp)
+		{
+			for (auto inst : sva_asserts)
+				svapp_assert(this, inst);
+
+			for (auto inst : sva_assumes)
+				svapp_assume(this, inst);
+
+			for (auto inst : sva_covers)
+				svapp_cover(this, inst);
+		}
+
 		if (!mode_nosva)
 		{
 			for (auto inst : sva_asserts)
@@ -1262,36 +1224,6 @@ struct VerificImporter
 	}
 };
 
-Net *verific_follow_inv(Net *w)
-{
-	if (w == nullptr || w->IsMultipleDriven())
-		return nullptr;
-
-	Instance *i = w->Driver();
-	if (i == nullptr || i->Type() != PRIM_INV)
-		return nullptr;
-
-	return i->GetInput();
-}
-
-Net *verific_follow_pslprev(Net *w)
-{
-	if (w == nullptr || w->IsMultipleDriven())
-		return nullptr;
-
-	Instance *i = w->Driver();
-	if (i == nullptr || i->Type() != OPER_PSLPREV || i->InputSize() != 1)
-		return nullptr;
-
-	return i->GetInputBit(0);
-}
-
-Net *verific_follow_inv_pslprev(Net *w)
-{
-	w = verific_follow_inv(w);
-	return verific_follow_pslprev(w);
-}
-
 VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst)
 {
 	log_assert(importer != nullptr);
@@ -1312,45 +1244,125 @@ VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst)
 		clock_sig = importer->net_map_at(clock_net);
 		return;
 	}
+}
+
+// ==================================================================
+
+struct VerificSvaPP
+{
+	VerificImporter *importer;
+	Module *module;
 
-	// VHDL-flavored PSL clock
-	if (inst->Type() == PRIM_AND)
+	Netlist *netlist;
+	Instance *root;
+
+	bool mode_assert = false;
+	bool mode_assume = false;
+	bool mode_cover = false;
+
+	Instance *net_to_ast_driver(Net *n)
 	{
-		Net *w1 = inst->GetInput1();
-		Net *w2 = inst->GetInput2();
+		if (n == nullptr)
+			return nullptr;
 
-		clock_net = verific_follow_inv_pslprev(w1);
-		if (clock_net == w2) {
-			clock_sig = importer->net_map_at(clock_net);
-			posedge = true;
-			return;
-		}
+		if (n->IsMultipleDriven())
+			return nullptr;
 
-		clock_net = verific_follow_inv_pslprev(w2);
-		if (clock_net == w1) {
-			clock_sig = importer->net_map_at(clock_net);
-			posedge = true;
-			return;
+		Instance *inst = n->Driver();
+
+		if (inst == nullptr)
+			return nullptr;
+
+		if (!importer->verific_sva_prims.count(inst->Type()))
+			return nullptr;
+
+		if (inst->Type() == PRIM_SVA_PAST)
+			return nullptr;
+
+		return inst;
+	}
+
+	Instance *get_ast_input(Instance *inst) { return net_to_ast_driver(inst->GetInput()); }
+	Instance *get_ast_input1(Instance *inst) { return net_to_ast_driver(inst->GetInput1()); }
+	Instance *get_ast_input2(Instance *inst) { return net_to_ast_driver(inst->GetInput2()); }
+	Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
+	Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }
+
+	Net *impl_to_seq(Instance *inst)
+	{
+		if (inst == nullptr)
+			return nullptr;
+
+		if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME) {
+			Net *new_net = impl_to_seq(get_ast_input(inst));
+			if (new_net) {
+				inst->Disconnect(inst->View()->GetInput());
+				inst->Connect(inst->View()->GetInput(), new_net);
+			}
+			return nullptr;
 		}
 
-		clock_net = verific_follow_pslprev(w1);
-		if (clock_net == verific_follow_inv(w2)) {
-			clock_sig = importer->net_map_at(clock_net);
-			posedge = false;
-			return;
+		if (inst->Type() == PRIM_SVA_AT) {
+			Net *new_net = impl_to_seq(get_ast_input2(inst));
+			if (new_net) {
+				inst->Disconnect(inst->View()->GetInput2());
+				inst->Connect(inst->View()->GetInput2(), new_net);
+			}
+			return nullptr;
 		}
 
-		clock_net = verific_follow_pslprev(w2);
-		if (clock_net == verific_follow_inv(w1)) {
-			clock_sig = importer->net_map_at(clock_net);
-			posedge = false;
-			return;
+		if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+		{
+			if (mode_cover) {
+				Net *new_in1 = impl_to_seq(get_ast_input1(inst));
+				Net *new_in2 = impl_to_seq(get_ast_input2(inst));
+				if (!new_in1) new_in1 = inst->GetInput1();
+				if (!new_in2) new_in2 = inst->GetInput2();
+				return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile());
+			}
 		}
 
-		log_abort();
+		return nullptr;
 	}
+
+	void run()
+	{
+		module = importer->module;
+		netlist = root->Owner();
+
+		// impl_to_seq(root);
+	}
+};
+
+void svapp_assert(VerificImporter *importer, Instance *inst)
+{
+	VerificSvaPP worker;
+	worker.importer = importer;
+	worker.root = inst;
+	worker.mode_assert = true;
+	worker.run();
+}
+
+void svapp_assume(VerificImporter *importer, Instance *inst)
+{
+	VerificSvaPP worker;
+	worker.importer = importer;
+	worker.root = inst;
+	worker.mode_assume = true;
+	worker.run();
 }
 
+void svapp_cover(VerificImporter *importer, Instance *inst)
+{
+	VerificSvaPP worker;
+	worker.importer = importer;
+	worker.root = inst;
+	worker.mode_cover = true;
+	worker.run();
+}
+
+// ==================================================================
+
 struct VerificSvaImporter
 {
 	VerificImporter *importer;
@@ -1367,6 +1379,7 @@ struct VerificSvaImporter
 	bool mode_assert = false;
 	bool mode_assume = false;
 	bool mode_cover = false;
+	bool eventually = false;
 
 	Instance *net_to_ast_driver(Net *n)
 	{
@@ -1381,8 +1394,7 @@ struct VerificSvaImporter
 		if (inst == nullptr)
 			return nullptr;
 
-		if (!importer->verific_sva_prims.count(inst->Type()) &&
-				!importer->verific_psl_prims.count(inst->Type()))
+		if (!importer->verific_sva_prims.count(inst->Type()))
 			return nullptr;
 
 		if (inst->Type() == PRIM_SVA_PAST)
@@ -1491,31 +1503,6 @@ struct VerificSvaImporter
 			return;
 		}
 
-		// PSL Primitives
-
-		if (inst->Type() == PRIM_ALWAYS)
-		{
-			parse_sequence(seq, inst->GetInput());
-			return;
-		}
-
-		if (inst->Type() == PRIM_IMPL)
-		{
-			parse_sequence(seq, inst->GetInput1());
-			seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
-			parse_sequence(seq, inst->GetInput2());
-			return;
-		}
-
-		if (inst->Type() == PRIM_SUFFIX_IMPL)
-		{
-			parse_sequence(seq, inst->GetInput1());
-			seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
-			sequence_ff(seq);
-			parse_sequence(seq, inst->GetInput2());
-			return;
-		}
-
 		// Handle unsupported primitives
 
 		if (!importer->mode_keep)
@@ -1531,24 +1518,33 @@ struct VerificSvaImporter
 		// parse SVA property clock event
 
 		Instance *at_node = get_ast_input(root);
-		log_assert(at_node && (at_node->Type() == PRIM_SVA_AT || at_node->Type() == PRIM_AT));
+		log_assert(at_node && at_node->Type() == PRIM_SVA_AT);
 
-		VerificClockEdge clock_edge(importer, at_node->Type() == PRIM_SVA_AT ? get_ast_input1(at_node) : at_node->GetInput2()->Driver());
+		VerificClockEdge clock_edge(importer, get_ast_input1(at_node));
 		clock = clock_edge.clock_sig;
 		clock_posedge = clock_edge.posedge;
 
 		// parse disable_iff expression
 
-		Net *sequence_net = at_node->Type() == PRIM_SVA_AT ? at_node->GetInput2() : at_node->GetInput1();
-		Instance *sequence_node = net_to_ast_driver(sequence_net);
+		Net *sequence_net = at_node->GetInput2();
+
+		while (1)
+		{
+			Instance *sequence_node = net_to_ast_driver(sequence_net);
+
+			if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) {
+				eventually = true;
+				sequence_net = sequence_node->GetInput();
+				continue;
+			}
 
-		if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) {
-			disable_iff = importer->net_map_at(sequence_node->GetInput1());
-			sequence_net = sequence_node->GetInput2();
-		} else
-		if (sequence_node && sequence_node->Type() == PRIM_ABORT) {
-			disable_iff = importer->net_map_at(sequence_node->GetInput2());
-			sequence_net = sequence_node->GetInput1();
+			if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) {
+				disable_iff = importer->net_map_at(sequence_node->GetInput1());
+				sequence_net = sequence_node->GetInput2();
+				continue;
+			}
+
+			break;
 		}
 
 		// parse SVA sequence into trigger signal
@@ -1561,9 +1557,14 @@ struct VerificSvaImporter
 
 		RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
 
-		if (mode_assert) module->addAssert(root_name, seq.sig_a, seq.sig_en);
-		if (mode_assume) module->addAssume(root_name, seq.sig_a, seq.sig_en);
-		if (mode_cover) module->addCover(root_name, seq.sig_a, seq.sig_en);
+		if (eventually) {
+			if (mode_assert) module->addLive(root_name, seq.sig_a, seq.sig_en);
+			if (mode_assume) module->addFair(root_name, seq.sig_a, seq.sig_en);
+		} else {
+			if (mode_assert) module->addAssert(root_name, seq.sig_a, seq.sig_en);
+			if (mode_assume) module->addAssume(root_name, seq.sig_a, seq.sig_en);
+			if (mode_cover) module->addCover(root_name, seq.sig_a, seq.sig_en);
+		}
 	}
 };
 
@@ -1594,6 +1595,8 @@ void import_sva_cover(VerificImporter *importer, Instance *inst)
 	worker.run();
 }
 
+// ==================================================================
+
 struct VerificExtNets
 {
 	int portname_cnt = 0;
@@ -1690,11 +1693,27 @@ struct VerificPass : public Pass {
 		log("Load the specified Verilog/SystemVerilog files into Verific.\n");
 		log("\n");
 		log("\n");
-		log("    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl|-vhdpsl} <vhdl-file>..\n");
+		log("    verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
 		log("\n");
 		log("Load the specified VHDL files into Verific.\n");
 		log("\n");
 		log("\n");
+		log("    verific -vlog-incdir <directory>..\n");
+		log("\n");
+		log("Add Verilog include directories.\n");
+		log("\n");
+		log("\n");
+		log("    verific -vlog-libdir <directory>..\n");
+		log("\n");
+		log("Add Verilog library directories. Verific will search in this directories to\n");
+		log("find undefined modules.\n");
+		log("\n");
+		log("\n");
+		log("    verific -vlog-define <macro>[=<value>]..\n");
+		log("\n");
+		log("Add Verilog defines. (The macros SYNTHESIS and VERIFIC are defined implicitly.)\n");
+		log("\n");
+		log("\n");
 		log("    verific -import [options] <top-module>..\n");
 		log("\n");
 		log("Elaborate the design for the specified top modules, import to Yosys and\n");
@@ -1715,10 +1734,6 @@ struct VerificPass : public Pass {
 		log("  -extnets\n");
 		log("    Resolve references to external nets by adding module ports as needed.\n");
 		log("\n");
-		log("  -nosva\n");
-		log("    Ignore SVA properties, do not infer checker logic. (This also disables\n");
-		log("    PSL properties in -vhdpsl mode.)\n");
-		log("\n");
 		log("  -v\n");
 		log("    Verbose log messages.\n");
 		log("\n");
@@ -1731,6 +1746,12 @@ struct VerificPass : public Pass {
 		log("    This will also add all SVA related cells to the design parallel to\n");
 		log("    the checker logic inferred by it.\n");
 		log("\n");
+		log("  -nosva\n");
+		log("    Ignore SVA properties, do not infer checker logic.\n");
+		log("\n");
+		log("  -nosvapp\n");
+		log("    Disable SVA properties pre-processing pass. This implies -nosva.\n");
+		log("\n");
 		log("  -n\n");
 		log("    Keep all Verific names on instances and nets. By default only\n");
 		log("    user-declared names are preserved.\n");
@@ -1750,6 +1771,8 @@ struct VerificPass : public Pass {
 		Message::RegisterCallBackMsg(msg_func);
 		RuntimeFlags::SetVar("db_allow_external_nets", 1);
 		RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
+		veri_file::DefineCmdLineMacro("VERIFIC");
+		veri_file::DefineCmdLineMacro("SYNTHESIS");
 
 		const char *release_str = Message::ReleaseString();
 		time_t release_time = Message::ReleaseDate();
@@ -1765,6 +1788,33 @@ struct VerificPass : public Pass {
 
 		int argidx = 1;
 
+		if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") {
+			for (argidx++; argidx < GetSize(args); argidx++)
+				veri_file::AddIncludeDir(args[argidx].c_str());
+			goto check_error;
+		}
+
+		if (GetSize(args) > argidx && args[argidx] == "-vlog-libdir") {
+			for (argidx++; argidx < GetSize(args); argidx++)
+				veri_file::AddYDir(args[argidx].c_str());
+			goto check_error;
+		}
+
+		if (GetSize(args) > argidx && args[argidx] == "-vlog-define") {
+			for (argidx++; argidx < GetSize(args); argidx++) {
+				string name = args[argidx];
+				size_t equal = name.find('=');
+				if (equal != std::string::npos) {
+					string value = name.substr(equal+1);
+					name = name.substr(0, equal);
+					veri_file::DefineCmdLineMacro(name.c_str(), value.c_str());
+				} else {
+					veri_file::DefineCmdLineMacro(name.c_str());
+				}
+			}
+			goto check_error;
+		}
+
 		if (GetSize(args) > argidx && args[argidx] == "-vlog95") {
 			for (argidx++; argidx < GetSize(args); argidx++)
 				if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_95))
@@ -1832,19 +1882,11 @@ struct VerificPass : public Pass {
 			goto check_error;
 		}
 
-		if (GetSize(args) > argidx && args[argidx] == "-vhdpsl") {
-			vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
-			for (argidx++; argidx < GetSize(args); 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());
-			goto check_error;
-		}
-
 		if (GetSize(args) > argidx && args[argidx] == "-import")
 		{
 			std::set<Netlist*> nl_todo, nl_done;
 			bool mode_all = false, mode_gates = false, mode_keep = false;
-			bool mode_nosva = false, mode_names = false;
+			bool mode_nosva = false, mode_nosvapp = false, mode_names = false;
 			bool verbose = false, flatten = false, extnets = false;
 			string dumpfile;
 
@@ -1873,6 +1915,11 @@ struct VerificPass : public Pass {
 					mode_nosva = true;
 					continue;
 				}
+				if (args[argidx] == "-nosvapp") {
+					mode_nosva = true;
+					mode_nosvapp = true;
+					continue;
+				}
 				if (args[argidx] == "-n") {
 					mode_names = true;
 					continue;
@@ -1968,13 +2015,15 @@ struct VerificPass : public Pass {
 			while (!nl_todo.empty()) {
 				Netlist *nl = *nl_todo.begin();
 				if (nl_done.count(nl) == 0) {
-					VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_names, verbose);
+					VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose);
 					importer.import_netlist(design, nl, nl_todo);
 				}
 				nl_todo.erase(nl);
 				nl_done.insert(nl);
 			}
 
+			veri_file::Reset();
+			vhdl_file::Reset();
 			Libset::Reset();
 			goto check_error;
 		}
diff --git a/frontends/vhdl2verilog/Makefile.inc b/frontends/vhdl2verilog/Makefile.inc
deleted file mode 100644
index 003d89c4a..000000000
--- a/frontends/vhdl2verilog/Makefile.inc
+++ /dev/null
@@ -1 +0,0 @@
-OBJS += frontends/vhdl2verilog/vhdl2verilog.o
diff --git a/frontends/vhdl2verilog/vhdl2verilog.cc b/frontends/vhdl2verilog/vhdl2verilog.cc
deleted file mode 100644
index 6f9c0e3f5..000000000
--- a/frontends/vhdl2verilog/vhdl2verilog.cc
+++ /dev/null
@@ -1,183 +0,0 @@
-/*
- *  yosys -- Yosys Open SYnthesis Suite
- *
- *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
- *
- *  Permission to use, copy, modify, and/or distribute this software for any
- *  purpose with or without fee is hereby granted, provided that the above
- *  copyright notice and this permission notice appear in all copies.
- *
- *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
- *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
- *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
- *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
- *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
- *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
- *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
- *
- */
-
-#include "kernel/register.h"
-#include "kernel/sigtools.h"
-#include "kernel/log.h"
-#include <stdlib.h>
-#include <stdio.h>
-#include <string.h>
-#include <errno.h>
-#include <limits.h>
-
-#ifndef _WIN32
-#  include <unistd.h>
-#  include <dirent.h>
-#endif
-
-YOSYS_NAMESPACE_BEGIN
-
-struct Vhdl2verilogPass : public Pass {
-	Vhdl2verilogPass() : Pass("vhdl2verilog", "importing VHDL designs using vhdl2verilog") { }
-	virtual void help()
-	{
-		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
-		log("\n");
-		log("    vhdl2verilog [options] <vhdl-file>..\n");
-		log("\n");
-		log("This command reads VHDL source files using the 'vhdl2verilog' tool and the\n");
-		log("Yosys Verilog frontend.\n");
-		log("\n");
-		log("    -out <out_file>\n");
-		log("        do not import the vhdl2verilog output. instead write it to the\n");
-		log("        specified file.\n");
-		log("\n");
-		log("    -vhdl2verilog_dir <directory>\n");
-		log("        do use the specified vhdl2verilog installation. this is the directory\n");
-		log("        that contains the setup_env.sh file. when this option is not present,\n");
-		log("        it is assumed that vhdl2verilog is in the PATH environment variable.\n");
-		log("\n");
-		log("    -top <top-entity-name>\n");
-		log("        The name of the top entity. This option is mandatory.\n");
-		log("\n");
-		log("The following options are passed as-is to vhdl2verilog:\n");
-		log("\n");
-		log("    -arch <architecture_name>\n");
-		log("    -unroll_generate\n");
-		log("    -nogenericeval\n");
-		log("    -nouniquify\n");
-		log("    -oldparser\n");
-		log("    -suppress <list>\n");
-		log("    -quiet\n");
-		log("    -nobanner\n");
-		log("    -mapfile <file>\n");
-		log("\n");
-		log("vhdl2verilog can be obtained from:\n");
-		log("http://www.edautils.com/vhdl2verilog.html\n");
-		log("\n");
-	}
-	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
-	{
-		log_header(design, "Executing VHDL2VERILOG (importing VHDL designs using vhdl2verilog).\n");
-		log_push();
-
-		std::string out_file, top_entity;
-		std::string vhdl2verilog_dir;
-		std::string extra_opts;
-
-		size_t argidx;
-		for (argidx = 1; argidx < args.size(); argidx++) {
-			if (args[argidx] == "-out" && argidx+1 < args.size()) {
-				out_file = args[++argidx];
-				continue;
-			}
-			if (args[argidx] == "-top" && argidx+1 < args.size()) {
-				top_entity = args[++argidx];
-				continue;
-			}
-			if (args[argidx] == "-vhdl2verilog_dir" && argidx+1 < args.size()) {
-				vhdl2verilog_dir = args[++argidx];
-				continue;
-			}
-			if ((args[argidx] == "-arch" || args[argidx] == "-suppress" || args[argidx] == "-mapfile") && argidx+1 < args.size()) {
-				if (args[argidx] == "-mapfile" && !args[argidx+1].empty() && args[argidx+1][0] != '/') {
-					char pwd[PATH_MAX];
-					if (!getcwd(pwd, sizeof(pwd))) {
-						log_cmd_error("getcwd failed: %s", strerror(errno));
-						log_abort();
-					}
-					args[argidx+1] = pwd + ("/" + args[argidx+1]);
-				}
-				extra_opts += std::string(" ") + args[argidx];
-				extra_opts += std::string(" '") + args[++argidx] + std::string("'");
-				continue;
-			}
-			if (args[argidx] == "-unroll_generate" || args[argidx] == "-nogenericeval" || args[argidx] == "-nouniquify" ||
-					args[argidx] == "-oldparser" || args[argidx] == "-quiet" || args[argidx] == "-nobanner") {
-				extra_opts += std::string(" ") + args[argidx];
-				continue;
-			}
-			break;
-		}
-
-		if (argidx == args.size())
-			cmd_error(args, argidx, "Missing filenames.");
-		if (args[argidx].substr(0, 1) == "-")
-			cmd_error(args, argidx, "Unknown option.");
-		if (top_entity.empty())
-			log_cmd_error("Missing -top option.\n");
-
-		std::string tempdir_name = make_temp_dir("/tmp/yosys-vhdl2verilog-XXXXXX");
-		log("Using temp directory %s.\n", tempdir_name.c_str());
-
-		if (!out_file.empty() && out_file[0] != '/') {
-			char pwd[PATH_MAX];
-			if (!getcwd(pwd, sizeof(pwd))) {
-				log_cmd_error("getcwd failed: %s", strerror(errno));
-				log_abort();
-			}
-			out_file = pwd + ("/" + out_file);
-		}
-
-		FILE *f = fopen(stringf("%s/files.list", tempdir_name.c_str()).c_str(), "wt");
-		while (argidx < args.size()) {
-			std::string file = args[argidx++];
-			if (file.empty())
-				continue;
-			if (file[0] != '/') {
-				char pwd[PATH_MAX];
-				if (!getcwd(pwd, sizeof(pwd))) {
-					log_cmd_error("getcwd failed: %s", strerror(errno));
-					log_abort();
-				}
-				file = pwd + ("/" + file);
-			}
-			fprintf(f, "%s\n", file.c_str());
-			log("Adding '%s' to the file list.\n", file.c_str());
-		}
-		fclose(f);
-
-		std::string command = "exec 2>&1; ";
-		if (!vhdl2verilog_dir.empty())
-			command += stringf("cd '%s'; . ./setup_env.sh; ", vhdl2verilog_dir.c_str());
-		command += stringf("cd '%s'; vhdl2verilog -out '%s' -filelist files.list -top '%s'%s", tempdir_name.c_str(),
-				out_file.empty() ? "vhdl2verilog_output.v" : out_file.c_str(), top_entity.c_str(), extra_opts.c_str());
-
-		log("Running '%s'..\n", command.c_str());
-
-		int ret = run_command(command, [](const std::string &line) { log("%s", line.c_str()); });
-		if (ret != 0)
-			log_error("Execution of command \"%s\" failed: return code %d.\n", command.c_str(), ret);
-
-		if (out_file.empty()) {
-			std::ifstream ff;
-			ff.open(stringf("%s/vhdl2verilog_output.v", tempdir_name.c_str()).c_str());
-			if (ff.fail())
-				log_error("Can't open vhdl2verilog output file `vhdl2verilog_output.v'.\n");
-			Frontend::frontend_call(design, &ff, stringf("%s/vhdl2verilog_output.v", tempdir_name.c_str()), "verilog");
-		}
-
-		log_header(design, "Removing temp directory `%s':\n", tempdir_name.c_str());
-		remove_directory(tempdir_name);
-		log_pop();
-	}
-} Vhdl2verilogPass;
-
-YOSYS_NAMESPACE_END
-
diff --git a/kernel/driver.cc b/kernel/driver.cc
index 1fe61b499..c5e31d718 100644
--- a/kernel/driver.cc
+++ b/kernel/driver.cc
@@ -25,6 +25,10 @@
 #  include <readline/history.h>
 #endif
 
+#ifdef YOSYS_ENABLE_EDITLINE
+#  include <editline/readline.h>
+#endif
+
 #include <stdio.h>
 #include <string.h>
 #include <limits.h>
@@ -119,27 +123,33 @@ const char *prompt()
 
 #else /* EMSCRIPTEN */
 
-#ifdef YOSYS_ENABLE_READLINE
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
 int yosys_history_offset = 0;
 std::string yosys_history_file;
 #endif
 
 void yosys_atexit()
 {
-#ifdef YOSYS_ENABLE_READLINE
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
 	if (!yosys_history_file.empty()) {
+#if defined(YOSYS_ENABLE_READLINE)
 		if (yosys_history_offset > 0) {
 			history_truncate_file(yosys_history_file.c_str(), 100);
 			append_history(where_history() - yosys_history_offset, yosys_history_file.c_str());
 		} else
 			write_history(yosys_history_file.c_str());
+#else
+		write_history(yosys_history_file.c_str());
+#endif
 	}
 
 	clear_history();
+#if defined(YOSYS_ENABLE_READLINE)
 	HIST_ENTRY **hist_list = history_list();
 	if (hist_list != NULL)
 		free(hist_list);
 #endif
+#endif
 }
 
 int main(int argc, char **argv)
@@ -159,7 +169,7 @@ int main(int argc, char **argv)
 	bool mode_v = false;
 	bool mode_q = false;
 
-#ifdef YOSYS_ENABLE_READLINE
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
 	if (getenv("HOME") != NULL) {
 		yosys_history_file = stringf("%s/.yosys_history", getenv("HOME"));
 		read_history(yosys_history_file.c_str());
diff --git a/kernel/yosys.cc b/kernel/yosys.cc
index e5b22eba7..34665a0ad 100644
--- a/kernel/yosys.cc
+++ b/kernel/yosys.cc
@@ -25,6 +25,10 @@
 #  include <readline/history.h>
 #endif
 
+#ifdef YOSYS_ENABLE_EDITLINE
+#  include <editline/readline.h>
+#endif
+
 #ifdef YOSYS_ENABLE_PLUGINS
 #  include <dlfcn.h>
 #endif
@@ -938,7 +942,7 @@ void run_backend(std::string filename, std::string command, RTLIL::Design *desig
 	Backend::backend_call(design, NULL, filename, command);
 }
 
-#ifdef YOSYS_ENABLE_READLINE
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
 static char *readline_cmd_generator(const char *text, int state)
 {
 	static std::map<std::string, Pass*>::iterator it;
@@ -1025,14 +1029,14 @@ void shell(RTLIL::Design *design)
 	recursion_counter++;
 	log_cmd_error_throw = true;
 
-#ifdef YOSYS_ENABLE_READLINE
-	rl_readline_name = "yosys";
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
+	rl_readline_name = (char*)"yosys";
 	rl_attempted_completion_function = readline_completion;
-	rl_basic_word_break_characters = " \t\n";
+	rl_basic_word_break_characters = (char*)" \t\n";
 #endif
 
 	char *command = NULL;
-#ifdef YOSYS_ENABLE_READLINE
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
 	while ((command = readline(create_prompt(design, recursion_counter))) != NULL)
 	{
 #else
@@ -1046,7 +1050,7 @@ void shell(RTLIL::Design *design)
 #endif
 		if (command[strspn(command, " \t\r\n")] == 0)
 			continue;
-#ifdef YOSYS_ENABLE_READLINE
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
 		add_history(command);
 #endif
 
@@ -1114,7 +1118,7 @@ struct ShellPass : public Pass {
 	}
 } ShellPass;
 
-#ifdef YOSYS_ENABLE_READLINE
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
 struct HistoryPass : public Pass {
 	HistoryPass() : Pass("history", "show last interactive commands") { }
 	virtual void help() {
@@ -1128,8 +1132,13 @@ struct HistoryPass : public Pass {
 	}
 	virtual void execute(std::vector<std::string> args, RTLIL::Design *design) {
 		extra_args(args, 1, design, false);
+#ifdef YOSYS_ENABLE_READLINE
 		for(HIST_ENTRY **list = history_list(); *list != NULL; list++)
 			log("%s\n", (*list)->line);
+#else
+		for (int i = where_history(); history_get(i); i++)
+			log("%s\n", history_get(i)->line);
+#endif
 	}
 } HistoryPass;
 #endif
diff --git a/passes/cmds/Makefile.inc b/passes/cmds/Makefile.inc
index 9e3934e16..44a83b2b9 100644
--- a/passes/cmds/Makefile.inc
+++ b/passes/cmds/Makefile.inc
@@ -28,4 +28,5 @@ OBJS += passes/cmds/edgetypes.o
 OBJS += passes/cmds/chformal.o
 OBJS += passes/cmds/chtype.o
 OBJS += passes/cmds/blackbox.o
+OBJS += passes/cmds/ltp.o
 
diff --git a/passes/cmds/ltp.cc b/passes/cmds/ltp.cc
new file mode 100644
index 000000000..42dc794ec
--- /dev/null
+++ b/passes/cmds/ltp.cc
@@ -0,0 +1,185 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
+ *
+ *  Permission to use, copy, modify, and/or distribute this software for any
+ *  purpose with or without fee is hereby granted, provided that the above
+ *  copyright notice and this permission notice appear in all copies.
+ *
+ *  THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ *  WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ *  MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ *  ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ *  WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ *  ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ *  OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/yosys.h"
+#include "kernel/celltypes.h"
+#include "kernel/sigtools.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct LtpWorker
+{
+	RTLIL::Design *design;
+	RTLIL::Module *module;
+	SigMap sigmap;
+
+	dict<SigBit, tuple<int, SigBit, Cell*>> bits;
+	dict<SigBit, dict<SigBit, Cell*>> bit2bits;
+	dict<SigBit, tuple<SigBit, Cell*>> bit2ff;
+
+	int maxlvl;
+	SigBit maxbit;
+	pool<SigBit> busy;
+
+	LtpWorker(RTLIL::Module *module, bool noff) : design(module->design), module(module), sigmap(module)
+	{
+		CellTypes ff_celltypes;
+
+		if (noff) {
+			ff_celltypes.setup_internals_mem();
+			ff_celltypes.setup_stdcells_mem();
+		}
+
+		for (auto wire : module->selected_wires())
+			for (auto bit : sigmap(wire))
+				bits[bit] = tuple<int, SigBit, Cell*>(-1, State::Sx, nullptr);
+
+		for (auto cell : module->selected_cells())
+		{
+			pool<SigBit> src_bits, dst_bits;
+
+			for (auto &conn : cell->connections())
+				for (auto bit : sigmap(conn.second)) {
+					if (cell->input(conn.first))
+						src_bits.insert(bit);
+					if (cell->output(conn.first))
+						dst_bits.insert(bit);
+				}
+
+			if (noff && ff_celltypes.cell_known(cell->type)) {
+				for (auto s : src_bits)
+					for (auto d : dst_bits) {
+						bit2ff[s] = tuple<SigBit, Cell*>(d, cell);
+						break;
+					}
+				continue;
+			}
+
+			for (auto s : src_bits)
+				for (auto d : dst_bits)
+					bit2bits[s][d] = cell;
+		}
+
+		maxlvl = -1;
+		maxbit = State::Sx;
+	}
+
+	void runner(SigBit bit, int level, SigBit from, Cell *via)
+	{
+		auto &bitinfo = bits.at(bit);
+
+		if (get<0>(bitinfo) >= level)
+			return;
+
+		if (busy.count(bit) > 0) {
+			log_warning("Detected loop at %s in %s\n", log_signal(bit), log_id(module));
+			return;
+		}
+
+		busy.insert(bit);
+		get<0>(bitinfo) = level;
+		get<1>(bitinfo) = from;
+		get<2>(bitinfo) = via;
+
+		if (level > maxlvl) {
+			maxlvl = level;
+			maxbit = bit;
+		}
+
+		if (bit2bits.count(bit)) {
+			for (auto &it : bit2bits.at(bit))
+				runner(it.first, level+1, bit, it.second);
+		}
+
+		busy.erase(bit);
+	}
+
+	void printpath(SigBit bit)
+	{
+		auto &bitinfo = bits.at(bit);
+		if (get<2>(bitinfo)) {
+			printpath(get<1>(bitinfo));
+			log("%5d: %s (via %s)\n", get<0>(bitinfo), log_signal(bit), log_id(get<2>(bitinfo)));
+		} else {
+			log("%5d: %s\n", get<0>(bitinfo), log_signal(bit));
+		}
+	}
+
+	void run()
+	{
+		for (auto &it : bits)
+			if (get<0>(it.second) < 0)
+				runner(it.first, 0, State::Sx, nullptr);
+
+		log("\n");
+		log("Longest topological path in %s (length=%d):\n", log_id(module), maxlvl);
+
+		if (maxlvl >= 0)
+			printpath(maxbit);
+
+		if (bit2ff.count(maxbit))
+			log("%5s: %s (via %s)\n", "ff", log_signal(get<0>(bit2ff.at(maxbit))), log_id(get<1>(bit2ff.at(maxbit))));
+	}
+};
+
+struct LtpPass : public Pass {
+	LtpPass() : Pass("ltp", "print longest topological path") { }
+	virtual void help()
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    ltp [options] [selection]\n");
+		log("\n");
+		log("This command prints the longest topological path in the design. (Only considers\n");
+		log("paths within a single module, so the design must be flattened.)\n");
+		log("\n");
+		log("    -noff\n");
+		log("        automatically exclude FF cell types\n");
+		log("\n");
+	}
+	virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+	{
+		bool noff = false;
+
+		log_header(design, "Executing LTP pass (find longest path).\n");
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-noff") {
+				noff = true;
+				continue;
+			}
+			break;
+		}
+
+		extra_args(args, argidx, design);
+
+		for (Module *module : design->selected_modules())
+		{
+			if (module->has_processes_warn())
+				continue;
+
+			LtpWorker worker(module, noff);
+			worker.run();
+		}
+	}
+} LtpPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc
index 3a3939a81..02624cf30 100644
--- a/passes/cmds/show.cc
+++ b/passes/cmds/show.cc
@@ -30,6 +30,10 @@
 #  include <readline/readline.h>
 #endif
 
+#ifdef YOSYS_ENABLE_EDITLINE
+#  include <editline/readline.h>
+#endif
+
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index fb1851868..2d2ffa9a1 100644
--- a/passes/opt/opt_clean.cc
+++ b/passes/opt/opt_clean.cc
@@ -392,7 +392,7 @@ bool rmunused_module_init(RTLIL::Module *module, bool purge_mode, bool verbose)
 		}
 
 		if (verbose)
-			log("  removing redundent init attribute on %s.\n", log_id(wire));
+			log("  removing redundant init attribute on %s.\n", log_id(wire));
 
 		wire->attributes.erase("\\init");
 		did_something = true;
diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index 02f3e93f5..edec42c4d 100644
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -430,6 +430,8 @@ struct OptRmdffPass : public Pass {
 
 			assign_map.set(module);
 			dff_init_map.set(module);
+			mux_drivers.clear();
+			init_attributes.clear();
 
 			for (auto wire : module->wires())
 			{
@@ -534,6 +536,7 @@ struct OptRmdffPass : public Pass {
 
 		assign_map.clear();
 		mux_drivers.clear();
+		init_attributes.clear();
 
 		if (total_count || total_initdrv)
 			design->scratchpad_set_bool("opt.did_something", true);
diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc
index 3d943e682..be86f642a 100644
--- a/passes/techmap/abc.cc
+++ b/passes/techmap/abc.cc
@@ -111,6 +111,7 @@ bool recover_init;
 
 bool clk_polarity, en_polarity;
 RTLIL::SigSpec clk_sig, en_sig;
+dict<int, std::string> pi_map, po_map;
 
 int map_signal(RTLIL::SigBit bit, gate_type_t gate_type = G(NONE), int in1 = -1, int in2 = -1, int in3 = -1, int in4 = -1)
 {
@@ -601,6 +602,14 @@ struct abc_output_filter
 
 	void next_line(const std::string &line)
 	{
+		int pi, po;
+		if (sscanf(line.c_str(), "Start-point = pi%d.  End-point = po%d.", &pi, &po) == 2) {
+			log("ABC: Start-point = pi%d (%s).  End-point = po%d (%s).\n",
+					pi, pi_map.count(pi) ? pi_map.at(pi).c_str() : "???",
+					po, po_map.count(po) ? po_map.at(po).c_str() : "???");
+			return;
+		}
+
 		for (char ch : line)
 			next_char(ch);
 	}
@@ -616,6 +625,8 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 
 	signal_map.clear();
 	signal_list.clear();
+	pi_map.clear();
+	po_map.clear();
 	recover_init = false;
 
 	if (clk_str != "$")
@@ -768,7 +779,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 		if (!si.is_port || si.type != G(NONE))
 			continue;
 		fprintf(f, " n%d", si.id);
-		count_input++;
+		pi_map[count_input++] = log_signal(si.bit);
 	}
 	if (count_input == 0)
 		fprintf(f, " dummy_input\n");
@@ -780,7 +791,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
 		if (!si.is_port || si.type == G(NONE))
 			continue;
 		fprintf(f, " n%d", si.id);
-		count_output++;
+		po_map[count_output++] = log_signal(si.bit);
 	}
 	fprintf(f, "\n");
 
@@ -1392,6 +1403,8 @@ struct AbcPass : public Pass {
 		signal_list.clear();
 		signal_map.clear();
 		signal_init.clear();
+		pi_map.clear();
+		po_map.clear();
 
 #ifdef ABCEXTERNAL
 		std::string exe_file = ABCEXTERNAL;
@@ -1819,6 +1832,8 @@ struct AbcPass : public Pass {
 		signal_list.clear();
 		signal_map.clear();
 		signal_init.clear();
+		pi_map.clear();
+		po_map.clear();
 
 		log_pop();
 	}
diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh
index 35c95a3e0..4c8e16542 100644
--- a/tests/sva/runtest.sh
+++ b/tests/sva/runtest.sh
@@ -29,7 +29,7 @@ generate_sby() {
 	fi
 
 	if [ -f $prefix.vhd ]; then
-		echo "verific -vhdpsl $prefix.vhd"
+		echo "verific -vhdl $prefix.vhd"
 	fi
 
 	cat <<- EOT
diff --git a/tests/sva/vhdlpsl00.vhd b/tests/sva/vhdlpsl00.vhd
deleted file mode 100644
index 6d765d5a9..000000000
--- a/tests/sva/vhdlpsl00.vhd
+++ /dev/null
@@ -1,34 +0,0 @@
-library ieee;
-use ieee.std_logic_1164.all;
-use ieee.std_logic_unsigned.all;
-use ieee.numeric_std.all;
-
-entity top is
-	port (
-		clk : in std_logic;
-		rst : in std_logic;
-		up : in std_logic;
-		down : in std_logic;
-		cnt : buffer std_logic_vector(7 downto 0)
-	);
-end entity;
-
-architecture rtl of top is
-begin
-	process (clk) begin
-		if rising_edge(clk) then
-			if rst = '1' then
-				cnt <= std_logic_vector(to_unsigned(0, 8));
-			elsif up = '1' then
-				cnt <= cnt + std_logic_vector(to_unsigned(1, 8));
-			elsif down = '1' then
-				cnt <= cnt - std_logic_vector(to_unsigned(1, 8));
-			end if;
-		end if;
-	end process;
-
-	-- PSL default clock is (rising_edge(clk));
-	-- PSL assume always ( down -> not up );
-	-- PSL assert always ( up |=> (cnt = prev(cnt) + std_logic_vector(to_unsigned(1, 8))) ) abort rst = '1';
-	-- PSL assert always ( down |=> (cnt = prev(cnt) - std_logic_vector(to_unsigned(1, 8))) ) abort rst = '1';
-end architecture;