Merge pull request #426 from antmicro/rk/add-formal
Handle -formal
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()));
