From 848062088cfc702ba2f4616e1091f63c636bbe5b Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Thu, 9 Feb 2017 13:51:44 +0100 Subject: [PATCH] Add checker support to verilog front-end --- README.md | 12 +++++++++--- frontends/verilog/verilog_lexer.l | 20 +++++++++++--------- frontends/verilog/verilog_parser.y | 15 +++++++++++++-- 3 files changed, 33 insertions(+), 14 deletions(-) diff --git a/README.md b/README.md index 396189d5f..3d3ff422e 100644 --- a/README.md +++ b/README.md @@ -379,10 +379,13 @@ Non-standard or SystemVerilog features for formal verification to 0 otherwise. - The system task ``$anyconst`` evaluates to any constant value. This is - equivalent to declaring a reg as ``const rand``. + equivalent to declaring a reg as ``rand const``, but also works outside + of checkers. (Yosys also supports ``rand const`` outside checkers.) - The system task ``$anyseq`` evaluates to any value, possibly a different - value in each cycle. This is equivalent to declaring a reg as ``rand``. + value in each cycle. This is equivalent to declaring a reg as ``rand``, + but also works outside of checkers. (Yosys also supports ``rand`` + variables outside checkers.) - The SystemVerilog tasks ``$past``, ``$stable``, ``$rose`` and ``$fell`` are supported in any clocked block. @@ -407,7 +410,10 @@ from SystemVerilog: - The keywords ``always_comb``, ``always_ff`` and ``always_latch``, ``logic`` and ``bit`` are supported. -- Declaring free variables with ``rand`` and ``const rand`` is supported. +- Declaring free variables with ``rand`` and ``rand const`` is supported. + +- Checkers without a port list that do not need to be instantiated (but instead + behave like a named block) are supported. - SystemVerilog packages are supported. Once a SystemVerilog file is read into a design with ``read_verilog``, all its packages are available to diff --git a/frontends/verilog/verilog_lexer.l b/frontends/verilog/verilog_lexer.l index 97af0ae2d..ff2fa5753 100644 --- a/frontends/verilog/verilog_lexer.l +++ b/frontends/verilog/verilog_lexer.l @@ -175,15 +175,17 @@ YOSYS_NAMESPACE_END "always_ff" { SV_KEYWORD(TOK_ALWAYS); } "always_latch" { SV_KEYWORD(TOK_ALWAYS); } -"assert" { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); } -"assume" { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); } -"cover" { if (formal_mode) return TOK_COVER; SV_KEYWORD(TOK_COVER); } -"restrict" { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); } -"property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); } -"rand" { if (formal_mode) return TOK_RAND; SV_KEYWORD(TOK_RAND); } -"const" { if (formal_mode) return TOK_CONST; SV_KEYWORD(TOK_CONST); } -"logic" { SV_KEYWORD(TOK_REG); } -"bit" { SV_KEYWORD(TOK_REG); } +"assert" { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); } +"assume" { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); } +"cover" { if (formal_mode) return TOK_COVER; SV_KEYWORD(TOK_COVER); } +"restrict" { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); } +"property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); } +"rand" { if (formal_mode) return TOK_RAND; SV_KEYWORD(TOK_RAND); } +"const" { if (formal_mode) return TOK_CONST; SV_KEYWORD(TOK_CONST); } +"checker" { if (formal_mode) return TOK_CHECKER; SV_KEYWORD(TOK_CHECKER); } +"endchecker" { if (formal_mode) return TOK_ENDCHECKER; SV_KEYWORD(TOK_ENDCHECKER); } +"logic" { SV_KEYWORD(TOK_REG); } +"bit" { SV_KEYWORD(TOK_REG); } "input" { return TOK_INPUT; } "output" { return TOK_OUTPUT; } diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index 3eb03dfd8..1879ff441 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -116,7 +116,7 @@ static void free_attr(std::map *al) %token TOK_SUPPLY0 TOK_SUPPLY1 TOK_TO_SIGNED TOK_TO_UNSIGNED %token TOK_POS_INDEXED TOK_NEG_INDEXED TOK_ASSERT TOK_ASSUME %token TOK_RESTRICT TOK_COVER TOK_PROPERTY TOK_ENUM TOK_TYPEDEF -%token TOK_RAND TOK_CONST +%token TOK_RAND TOK_CONST TOK_CHECKER TOK_ENDCHECKER %type range range_or_multirange non_opt_range non_opt_multirange range_or_signed_int %type wire_type expr basic_expr concat_list rvalue lvalue lvalue_concat_list @@ -465,7 +465,18 @@ 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_property; + always_stmt | TOK_GENERATE module_gen_body TOK_ENDGENERATE | defattr | assert_property | checker_decl; + +checker_decl: + TOK_CHECKER TOK_ID ';' { + AstNode *node = new AstNode(AST_GENBLOCK); + node->str = *$2; + ast_stack.back()->children.push_back(node); + ast_stack.push_back(node); + } module_body TOK_ENDCHECKER { + delete $2; + ast_stack.pop_back(); + }; task_func_decl: attr TOK_DPI_FUNCTION TOK_ID TOK_ID { -- 2.30.2