diff options
| -rw-r--r-- | README | 16 | ||||
| -rw-r--r-- | frontends/verilog/lexer.l | 17 | ||||
| -rw-r--r-- | frontends/verilog/parser.y | 10 | ||||
| -rw-r--r-- | frontends/verilog/verilog_frontend.cc | 10 | ||||
| -rw-r--r-- | frontends/verilog/verilog_frontend.h | 3 | ||||
| -rw-r--r-- | tests/sat/asserts.ys | 2 | ||||
| -rw-r--r-- | tests/sat/asserts_seq.ys | 2 |
7 files changed, 52 insertions, 8 deletions
@@ -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 5300d1b2..8f4b4991 100644 --- 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 f422258c..cce8a8c4 100644 --- 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 10821458..437fc3ec 100644 --- 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 99b2164e..6d01a153 100644 --- 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 de5e7c9a..d8f99492 100644 --- 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 c622ef61..e9768664 100644 --- 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 |