From 482d9208aa9dacb7afe21f08c882d4881581013a Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 12 Jun 2014 11:54:20 +0200 Subject: [PATCH] Added read_verilog -sv options, added support for bit, logic, allways_ff, always_comb, and always_latch --- README | 16 +++++++++++++--- frontends/verilog/lexer.l | 17 ++++++++++++++++- frontends/verilog/parser.y | 10 ++++++++-- frontends/verilog/verilog_frontend.cc | 10 ++++++++++ frontends/verilog/verilog_frontend.h | 3 +++ tests/sat/asserts.ys | 2 +- tests/sat/asserts_seq.ys | 2 +- 7 files changed, 52 insertions(+), 8 deletions(-) diff --git a/README b/README index d021c8864..05628a8e3 100644 --- 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 's?[bodh]) support constant + expressions as . 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 ();" and within an always block: "assert();". It is transformed to a $assert cell that is supported by the "sat" and "write_btor" commands. -- Sized constants (the syntax 's?[bodh]) support constant - expressions as . 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 5300d1b26..8f4b49916 100644 --- a/frontends/verilog/lexer.l +++ b/frontends/verilog/lexer.l @@ -52,6 +52,14 @@ namespace VERILOG_FRONTEND { std::vector 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 f422258c7..cce8a8c40 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 case_type_stack; bool default_nettype_wire; + bool sv_mode; } static void append_attr(AstNode *ast, std::map *al) @@ -105,7 +106,7 @@ static void free_attr(std::map *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 wire_type range non_opt_range range_or_integer expr basic_expr concat_list rvalue lvalue lvalue_concat_list %type 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 108214586..437fc3ec0 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 defines_map; std::list include_dirs; std::list 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 99b2164ef..6d01a1532 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 de5e7c9aa..d8f994925 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 c622ef610..e97686644 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 -- 2.30.2