diff --git a/.gitignore b/.gitignore
index 086e6bc994b..9fcffb0d831 100644
--- a/.gitignore
+++ b/.gitignore
@@ -52,3 +52,6 @@ __pycache__
 /tests/verilog/roundtrip_proc_1.v
 /tests/verilog/roundtrip_proc_2.v
 /result
+
+# Preqorsor
+preqorsor
diff --git a/Makefile b/Makefile
index 79cd91ff302..329d7890349 100644
--- a/Makefile
+++ b/Makefile
@@ -27,7 +27,6 @@ ENABLE_VERIFIC_LIBERTY := 0
 ENABLE_COVER := 1
 ENABLE_LIBYOSYS := 0
 ENABLE_ZLIB := 1
-ENABLE_FUNC := 0
 
 # python wrappers
 ENABLE_PYOSYS := 1
@@ -40,7 +39,7 @@ ENABLE_LTO := 0
 ENABLE_CCACHE := 0
 # sccache is not always a drop-in replacement for ccache in practice
 ENABLE_SCCACHE := 0
-ENABLE_FUNCTIONAL_TESTS := 0
+ENABLE_FUNCTIONAL_TESTS := 1
 LINK_CURSES := 0
 LINK_TERMCAP := 0
 LINK_ABC := 0
@@ -500,7 +499,7 @@ endif
 LIBS_VERIFIC =
 ifeq ($(ENABLE_VERIFIC),1)
 VERIFIC_DIR ?= ./verific
-VERIFIC_COMPONENTS ?= database util containers hdl_file_sort
+VERIFIC_COMPONENTS ?= database util containers
 ifeq ($(ENABLE_VERIFIC_HIER_TREE),1)
 VERIFIC_COMPONENTS += hier_tree
 CXXFLAGS += -DVERIFIC_HIER_TREE_SUPPORT
@@ -650,9 +649,7 @@ $(eval $(call add_include_file,backends/rtlil/rtlil_backend.h))
 OBJS += kernel/driver.o kernel/register.o kernel/rtlil.o kernel/log.o kernel/calc.o kernel/yosys.o
 OBJS += kernel/binding.o
 OBJS += kernel/cellaigs.o kernel/celledges.o kernel/cost.o kernel/satgen.o kernel/scopeinfo.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o kernel/yw.o kernel/json.o kernel/fmt.o kernel/sexpr.o
-ifeq ($(ENABLE_FUNC),1)
 OBJS += kernel/drivertools.o kernel/functional.o
-endif
 ifeq ($(ENABLE_ZLIB),1)
 OBJS += kernel/fstdata.o
 endif
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index 41a61441892..266ea15a206 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -3809,6 +3809,7 @@ struct VerificPass : public Pass {
 			veri_file::DefineMacro("YOSYS");
 			veri_file::DefineMacro("VERIFIC");
 			veri_file::DefineMacro(args[argidx] == "-formal" ? "FORMAL" : "SYNTHESIS");
+			RuntimeFlags::SetVar("veri_ignore_assertion_statements", args[argidx] != "-formal");
 
 			for (argidx++; argidx < GetSize(args) && GetSize(args[argidx]) >= 2 && args[argidx].compare(0, 2, "-D") == 0; argidx++) {
 				std::string name = args[argidx].substr(2);
@@ -4457,7 +4458,7 @@ struct ReadPass : public Pass {
 
 		if (args[1] == "-vlog95" || args[1] == "-vlog2k") {
 			if (use_verific) {
-				args[0] = "verific";
+				args[0] = "import";
 			} else {
 				args[0] = "read_verilog";
 				args[1] = "-defer";
@@ -4468,11 +4469,13 @@ struct ReadPass : public Pass {
 
 		if (args[1] == "-sv2005" || args[1] == "-sv2009" || args[1] == "-sv2012" || args[1] == "-sv" || args[1] == "-formal") {
 			if (use_verific) {
-				args[0] = "verific";
+				args[0] = "import";
 			} else {
 				args[0] = "read_verilog";
-				if (args[1] == "-formal")
+				if (args[1] == "-formal") {
 					args.insert(args.begin()+1, std::string());
+					RuntimeFlags::SetVar("veri_ignore_assertion_statements", 0);
+				}
 				args[1] = "-sv";
 				args.insert(args.begin()+1, "-defer");
 			}
@@ -4483,7 +4486,7 @@ struct ReadPass : public Pass {
 #ifdef VERIFIC_VHDL_SUPPORT
 		if (args[1] == "-vhdl87" || args[1] == "-vhdl93" || args[1] == "-vhdl2k" || args[1] == "-vhdl2008" || args[1] == "-vhdl2019" || args[1] == "-vhdl") {
 			if (use_verific) {
-				args[0] = "verific";
+				args[0] = "import";
 				Pass::call(design, args);
 			} else {
 				cmd_error(args, 1, "This version of Yosys is built without Verific support.\n");
@@ -4494,7 +4497,7 @@ struct ReadPass : public Pass {
 #ifdef VERIFIC_EDIF_SUPPORT
 		if (args[1] == "-edif") {
 			if (use_verific) {
-				args[0] = "verific";
+				args[0] = "import";
 				Pass::call(design, args);
 			} else {
 				cmd_error(args, 1, "This version of Yosys is built without Verific support.\n");
@@ -4504,7 +4507,7 @@ struct ReadPass : public Pass {
 #endif
 		if (args[1] == "-liberty") {
 			if (use_verific) {
-				args[0] = "verific";
+				args[0] = "import";
 			} else {
 				args[0] = "read_liberty";
 			}
@@ -4513,7 +4516,7 @@ struct ReadPass : public Pass {
 		}
 		if (args[1] == "-f" || args[1] == "-F") {
 			if (use_verific) {
-				args[0] = "verific";
+				args[0] = "import";
 				Pass::call(design, args);
 			} else {
 				cmd_error(args, 1, "This version of Yosys is built without Verific support.\n");
@@ -4523,7 +4526,7 @@ struct ReadPass : public Pass {
 
 		if (args[1] == "-define") {
 			if (use_verific) {
-				args[0] = "verific";
+				args[0] = "import";
 				args[1] = "-vlog-define";
 				Pass::call(design, args);
 			}
@@ -4537,7 +4540,7 @@ struct ReadPass : public Pass {
 
 		if (args[1] == "-undef") {
 			if (use_verific) {
-				args[0] = "verific";
+				args[0] = "import";
 				args[1] = "-vlog-undef";
 				Pass::call(design, args);
 			}
@@ -4551,7 +4554,7 @@ struct ReadPass : public Pass {
 
 		if (args[1] == "-incdir") {
 			if (use_verific) {
-				args[0] = "verific";
+				args[0] = "import";
 				args[1] = "-vlog-incdir";
 				Pass::call(design, args);
 			}
diff --git a/tests/verific/bounds.ys b/tests/verific/bounds.ys.fail
similarity index 100%
rename from tests/verific/bounds.ys
rename to tests/verific/bounds.ys.fail