Added read_verilog -sv options, added support for bit, logic,

allways_ff, always_comb, and always_latch

diff --git a/README b/README
index d021c8864d656bee661e5bd64ecad24c142aee6f..05628a8e3bfa8e552166d944260abd33c20482ee 100644 (file)
--- a/README
+++ b/README
@@ -263,14 +263,24 @@ Verilog Attributes and non-standard features
   for everything that comes after the {* ... *} statement. (Reset
   by adding an empty {* *} statement.)
 
+- Sized constants (the syntax <size>'s?[bodh]<value>) support constant
+  expressions as <size>. If the expresion is not a simple identifier, it
+  must be put in parentheses. Examples: WIDTH'd42, (4+2)'b101010
+
+
+Supported features from SystemVerilog
+=====================================
+
+When read_verilog is called with -sv, it accepts some language features
+from SystemVerilog:
+
 - The "assert" statement from SystemVerilog is supported in its most basic
   form. In module context: "assert property (<expression>);" and within an
   always block: "assert(<expression>);". It is transformed to a $assert cell
   that is supported by the "sat" and "write_btor" commands.
 
-- Sized constants (the syntax <size>'s?[bodh]<value>) support constant
-  expressions as <size>. If the expresion is not a simple identifier, it
-  must be put in parentheses. Examples: WIDTH'd42, (4+2)'b101010
+- The keywords "always_comb", "always_ff" and "always_latch", "logic" and
+  "bit" are supported.
 
 
 Roadmap / Large-scale TODOs

diff --git a/frontends/verilog/lexer.l b/frontends/verilog/lexer.l
index 5300d1b263aa5fdbc1cbc161a77976d680b50ea9..8f4b499164c3ebeaa8ef2240a6fd4a4b8eee6cf0 100644 (file)
--- a/frontends/verilog/lexer.l
+++ b/frontends/verilog/lexer.l
@@ -52,6 +52,14 @@ namespace VERILOG_FRONTEND {
        std::vector<int> ln_stack;
 }
 
+#define SV_KEYWORD(_tok) \
+       if (sv_mode) return _tok; \
+       log("Lexer warning: The SystemVerilog keyword `%s' (at %s:%d) is not "\
+                       "recognized unless read_verilog is called with -sv!\n", yytext, \
+                       AST::current_filename.c_str(), frontend_verilog_yyget_lineno()); \
+       frontend_verilog_yylval.string = new std::string(std::string("\\") + yytext); \
+       return TOK_ID;
+
 %}
 
 %option yylineno
@@ -143,7 +151,14 @@ namespace VERILOG_FRONTEND {
 "while"        { return TOK_WHILE; }
 "repeat"       { return TOK_REPEAT; }
 
-"assert"([ \t\r\n]+"property")? { return TOK_ASSERT; }
+"always_comb"  { SV_KEYWORD(TOK_ALWAYS); }
+"always_ff"    { SV_KEYWORD(TOK_ALWAYS); }
+"always_latch" { SV_KEYWORD(TOK_ALWAYS); }
+
+"assert"   { SV_KEYWORD(TOK_ASSERT); }
+"property" { SV_KEYWORD(TOK_PROPERTY); }
+"logic"    { SV_KEYWORD(TOK_REG); }
+"bit"      { SV_KEYWORD(TOK_REG); }
 
 "input"   { return TOK_INPUT; }
 "output"  { return TOK_OUTPUT; }

diff --git a/frontends/verilog/parser.y b/frontends/verilog/parser.y
index f422258c7712dd6a3e6f62feb745ae350ce7e4a5..cce8a8c405d7abab430d1437fbf0f0b7aa184ffe 100644 (file)
--- a/frontends/verilog/parser.y
+++ b/frontends/verilog/parser.y
@@ -54,6 +54,7 @@ namespace VERILOG_FRONTEND {
        int current_function_or_task_port_id;
        std::vector<char> case_type_stack;
        bool default_nettype_wire;
+       bool sv_mode;
 }
 
 static void append_attr(AstNode *ast, std::map<std::string, AstNode*> *al)
@@ -105,7 +106,7 @@ static void free_attr(std::map<std::string, AstNode*> *al)
 %token TOK_GENERATE TOK_ENDGENERATE TOK_GENVAR
 %token TOK_SYNOPSYS_FULL_CASE TOK_SYNOPSYS_PARALLEL_CASE
 %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED
-%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT
+%token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_PROPERTY
 
 %type <ast> wire_type range non_opt_range range_or_integer expr basic_expr concat_list rvalue lvalue lvalue_concat_list
 %type <string> opt_label tok_prim_wrapper hierarchical_id
@@ -379,7 +380,7 @@ module_body:
 
 module_body_stmt:
        task_func_decl | param_decl | localparam_decl | defparam_decl | wire_decl | assign_stmt | cell_stmt |
-       always_stmt | TOK_GENERATE module_gen_body TOK_ENDGENERATE | defattr | assert;
+       always_stmt | TOK_GENERATE module_gen_body TOK_ENDGENERATE | defattr | assert_property;
 
 task_func_decl:
        TOK_TASK TOK_ID ';' {
@@ -773,6 +774,11 @@ assert:
                ast_stack.back()->children.push_back(new AstNode(AST_ASSERT, $3));
        };
 
+assert_property:
+       TOK_ASSERT TOK_PROPERTY '(' expr ')' ';' {
+               ast_stack.back()->children.push_back(new AstNode(AST_ASSERT, $4));
+       };
+
 simple_behavioral_stmt:
        lvalue '=' expr {
                AstNode *node = new AstNode(AST_ASSIGN_EQ, $1, $3);

diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc
index 108214586f2d5e6342b9d2953322d1912f97c1cd..437fc3ec08f31f5cce296d36d152a279cb376fd1 100644 (file)
--- a/frontends/verilog/verilog_frontend.cc
+++ b/frontends/verilog/verilog_frontend.cc
@@ -53,6 +53,10 @@ struct VerilogFrontend : public Frontend {
                log("Load modules from a verilog file to the current design. A large subset of\n");
                log("Verilog-2005 is supported.\n");
                log("\n");
+               log("    -sv\n");
+               log("        enable support for SystemVerilog features. (only a small subset\n");
+               log("        of SystemVerilog is supported)\n");
+               log("\n");
                log("    -dump_ast1\n");
                log("        dump abstract syntax tree (before simplification)\n");
                log("\n");
@@ -150,7 +154,9 @@ struct VerilogFrontend : public Frontend {
                std::map<std::string, std::string> defines_map;
                std::list<std::string> include_dirs;
                std::list<std::string> attributes;
+
                frontend_verilog_yydebug = false;
+               sv_mode = false;
 
                log_header("Executing Verilog-2005 frontend.\n");
 
@@ -159,6 +165,10 @@ struct VerilogFrontend : public Frontend {
                size_t argidx;
                for (argidx = 1; argidx < args.size(); argidx++) {
                        std::string arg = args[argidx];
+                       if (arg == "-sv") {
+                               sv_mode = true;
+                               continue;
+                       }
                        if (arg == "-dump_ast1") {
                                flag_dump_ast1 = true;
                                continue;

diff --git a/frontends/verilog/verilog_frontend.h b/frontends/verilog/verilog_frontend.h
index 99b2164efe8a19ef81d4ccf50be1e5c576a350bd..6d01a15326c15d3d5131fc313e7d922d5c7037fb 100644 (file)
--- a/frontends/verilog/verilog_frontend.h
+++ b/frontends/verilog/verilog_frontend.h
@@ -45,6 +45,9 @@ namespace VERILOG_FRONTEND
 
        // state of `default_nettype
        extern bool default_nettype_wire;
+
+       // running in SystemVerilog mode
+       extern bool sv_mode;
 }
 
 // the pre-processor

diff --git a/tests/sat/asserts.ys b/tests/sat/asserts.ys
index de5e7c9aa6ab3c217ebdbd3ec64906530d785e57..d8f9949257f1f1e57de87683c621b43c84286e12 100644 (file)
--- a/tests/sat/asserts.ys
+++ b/tests/sat/asserts.ys
@@ -1,3 +1,3 @@
-read_verilog asserts.v
+read_verilog -sv asserts.v
 hierarchy; proc; opt
 sat -verify -seq 1 -set-at 1 rst 1 -tempinduct -prove-asserts

diff --git a/tests/sat/asserts_seq.ys b/tests/sat/asserts_seq.ys
index c622ef6101cfe7078b5a2d90ae94475010f3a738..e97686644c695c188ce9648a1b40fb85a0514d74 100644 (file)
--- a/tests/sat/asserts_seq.ys
+++ b/tests/sat/asserts_seq.ys
@@ -1,4 +1,4 @@
-read_verilog asserts_seq.v
+read_verilog -sv asserts_seq.v
 hierarchy; proc; opt
 
 sat -verify  -prove-asserts -tempinduct -seq 1 test_001