SystemVerilog also has assume(), added implicit -D FORMAL

diff --git a/frontends/verilog/preproc.cc b/frontends/verilog/preproc.cc
index fb8a7b95f61de19aef2786e5180e85d60f38dbc6..997920b896fe25625d5316e770e71827c6d2e126 100644 (file)
--- 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 b6500d5e54a3dcf817a28250d0801a7919f8e17e..cd8b586c40d294dd727eb5ae2c7ec58180c391de 100644 (file)
--- 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 47c1a0e6363635177d43e37396fd56e20732f6da..69a8ddaad2d46546d383d5e542d2018b5deda436 100644 (file)
--- 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); }