diff --git a/systemverilog-plugin/tests/Makefile b/systemverilog-plugin/tests/Makefile
index 849a9f9..4312522 100644
--- a/systemverilog-plugin/tests/Makefile
+++ b/systemverilog-plugin/tests/Makefile
@@ -20,7 +20,8 @@
 		debug-flag \
 		report-flag \
 		defines \
-		defaults
+		defaults \
+		formal
 
 include $(shell pwd)/../../Makefile_test.common
 
@@ -31,3 +32,4 @@
 report-flag_verify = true
 defaults_verify = true
 defines_verify = true
+formal_verify = true
diff --git a/systemverilog-plugin/tests/formal/formal.tcl b/systemverilog-plugin/tests/formal/formal.tcl
new file mode 100644
index 0000000..2474219
--- /dev/null
+++ b/systemverilog-plugin/tests/formal/formal.tcl
@@ -0,0 +1,12 @@
+yosys -import
+if { [info procs read_uhdm] == {} } { plugin -i systemverilog }
+yosys -import  ;# ingest plugin commands
+
+set TMP_DIR /tmp
+if { [info exists ::env(TMPDIR) ] } {
+  set TMP_DIR $::env(TMPDIR)
+}
+
+read_systemverilog -formal $::env(DESIGN_TOP).v
+hierarchy
+write_verilog
diff --git a/systemverilog-plugin/tests/formal/formal.v b/systemverilog-plugin/tests/formal/formal.v
new file mode 100644
index 0000000..04e346c
--- /dev/null
+++ b/systemverilog-plugin/tests/formal/formal.v
@@ -0,0 +1,33 @@
+// Copyright 2020-2022 F4PGA Authors
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+//     http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+//
+// SPDX-License-Identifier: Apache-2.0
+
+module top #(
+)(
+  input clk,
+  output out
+);
+
+`ifdef SYNTHESIS
+  initial $stop("SYNTHESIS should be undefined");
+`endif
+`ifndef YOSYS
+  initial $stop("YOSYS should be defined");
+`endif
+`ifndef FORMAL
+  initial $stop("FORMAL should be defined");
+`endif
+  assign out = clk;
+endmodule
diff --git a/systemverilog-plugin/uhdmastshared.h b/systemverilog-plugin/uhdmastshared.h
index b185975..475ba70 100644
--- a/systemverilog-plugin/uhdmastshared.h
+++ b/systemverilog-plugin/uhdmastshared.h
@@ -51,6 +51,11 @@
     // applies only to read_systemverilog command
     bool link = false;
 
+    // Flag equivalent to read_verilog -formal
+    // Defines FORMAL, undefines SYNTHESIS
+    // Allows verification constructs in Surelog
+    bool formal = false;
+
     // Top nodes of the design (modules, interfaces)
     std::unordered_map<std::string, ::Yosys::AST::AstNode *> top_nodes;
 
diff --git a/systemverilog-plugin/uhdmcommonfrontend.cc b/systemverilog-plugin/uhdmcommonfrontend.cc
index 167259c..7fd3871 100644
--- a/systemverilog-plugin/uhdmcommonfrontend.cc
+++ b/systemverilog-plugin/uhdmcommonfrontend.cc
@@ -65,13 +65,19 @@
     log("        parameters of modules yield invalid or not synthesizable code.\n");
     log("        Needs to be followed by read_systemverilog -link after reading\n");
     log("        all files.\n");
+    log("\n");
     log("    -link\n");
     log("        performs linking and elaboration of the files read with -defer\n");
+    log("\n");
     log("    -parse-only\n");
     log("        this parameter only applies to read_systemverilog command,\n");
     log("        it runs only Surelog to parse design, but doesn't load generated\n");
     log("        tree into Yosys.\n");
     log("\n");
+    log("    -formal\n");
+    log("        enable support for SystemVerilog assertions and some Yosys extensions\n");
+    log("        replace the implicit -D SYNTHESIS with -D FORMAL\n");
+    log("\n");
 }
 
 void UhdmCommonFrontend::execute(std::istream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
@@ -120,6 +126,10 @@
             this->shared.link = true;
             // Surelog needs it in the command line to link correctly
             unhandled_args.push_back(args[i]);
+        } else if (args[i] == "-formal") {
+            this->shared.formal = true;
+            // Surelog needs it in the command line to annotate UHDM
+            unhandled_args.push_back(args[i]);
         } else {
             unhandled_args.push_back(args[i]);
         }
diff --git a/systemverilog-plugin/uhdmsurelogastfrontend.cc b/systemverilog-plugin/uhdmsurelogastfrontend.cc
index a72b405..8801d8e 100644
--- a/systemverilog-plugin/uhdmsurelogastfrontend.cc
+++ b/systemverilog-plugin/uhdmsurelogastfrontend.cc
@@ -132,6 +132,11 @@
     {
         std::vector<const char *> cstrings;
         bool link = false;
+        if (this->shared.formal) {
+            systemverilog_defines.push_back("-DFORMAL=1");
+        } else {
+            systemverilog_defines.push_back("-DSYNTHESIS=1");
+        }
         cstrings.reserve(this->args.size() + systemverilog_defaults.size() + systemverilog_defines.size());
         for (size_t i = 0; i < this->args.size(); ++i) {
             cstrings.push_back(const_cast<char *>(this->args[i].c_str()));