aboutsummaryrefslogtreecommitdiffstats
path: root/frontends
diff options
context:
space:
mode:
Diffstat (limited to 'frontends')
-rw-r--r--frontends/verilog/preproc.cc3
-rw-r--r--frontends/verilog/verilog_frontend.cc4
-rw-r--r--frontends/verilog/verilog_lexer.l2
3 files changed, 5 insertions, 4 deletions
diff --git a/frontends/verilog/preproc.cc b/frontends/verilog/preproc.cc
index fb8a7b95f..997920b89 100644
--- a/frontends/verilog/preproc.cc
+++ b/frontends/verilog/preproc.cc
@@ -39,6 +39,7 @@
#include <string.h>
YOSYS_NAMESPACE_BEGIN
+using namespace VERILOG_FRONTEND;
static std::list<std::string> output_code;
static std::list<std::string> input_buffer;
@@ -222,7 +223,7 @@ std::string frontend_verilog_preproc(std::istream &f, std::string filename, cons
input_file(f, filename);
defines_map["YOSYS"] = "1";
- defines_map["SYNTHESIS"] = "1";
+ defines_map[formal_mode ? "FORMAL" : "SYNTHESIS"] = "1";
while (!input_buffer.empty())
{
diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc
index b6500d5e5..cd8b586c4 100644
--- a/frontends/verilog/verilog_frontend.cc
+++ b/frontends/verilog/verilog_frontend.cc
@@ -63,8 +63,8 @@ struct VerilogFrontend : public Frontend {
log(" of SystemVerilog is supported)\n");
log("\n");
log(" -formal\n");
- log(" enable support for assert() and assume() statements\n");
- log(" (assert support is also enabled with -sv)\n");
+ log(" enable support for assert() and assume() from SystemVerilog\n");
+ log(" replace the implicit -D SYNTHESIS with -D FORMAL\n");
log("\n");
log(" -dump_ast1\n");
log(" dump abstract syntax tree (before simplification)\n");
diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l
index 47c1a0e63..69a8ddaad 100644
--- a/frontends/verilog/verilog_lexer.l
+++ b/frontends/verilog/verilog_lexer.l
@@ -170,7 +170,7 @@ YOSYS_NAMESPACE_END
"always_latch" { SV_KEYWORD(TOK_ALWAYS); }
"assert" { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); }
-"assume" { if (formal_mode) return TOK_ASSUME; return TOK_ID; }
+"assume" { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); }
"property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); }
"logic" { SV_KEYWORD(TOK_REG); }
"bit" { SV_KEYWORD(TOK_REG); }