Add checker support to verilog front-end

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

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; }

frontends/verilog/verilog_parser.y

@@ -116,7 +116,7 @@ static void free_attr(std::map<std::string, AstNode*> *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 <ast> range range_or_multirange  non_opt_range non_opt_multirange range_or_signed_int
 %type <ast> 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 {