SystemVerilog checkers

CHANGELOG

@@ -10,6 +10,7 @@
 * SystemVerilog: $itor, $rtoi
 * SystemVerilog: chandle, event, string
 * SystemVerilog: package scope operator
+* SystemVerilog: checkers
 
 # EBMC 5.4
 

regression/verilog/checker/checker2.desc

@@ -0,0 +1,7 @@
+CORE
+checker2.sv
+--bound 20
+^\[main\.c\.assert\.1\] always myChecker\.data != 10: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--

regression/verilog/checker/checker2.sv

@@ -0,0 +1,9 @@
+checker myChecker(input logic [31:0] data);
+  assert property (data != 10);
+endchecker
+
+module main(input clk);
+  reg [31:0] counter = 0;
+  always_ff @(posedge clk) counter++;
+  myChecker c(counter);
+endmodule

regression/verilog/checker/checker3.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+checker3.sv
+--bound 20
+^\[main\.c\.assert\.1\] always myChecker\.data != 10: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Support for property parameters for checkers is missing.

regression/verilog/checker/checker3.sv

@@ -0,0 +1,14 @@
+checker myChecker(property p);
+  assert property (p);
+endchecker
+
+module main(input clk);
+  reg [31:0] counter = 0;
+  always_ff @(posedge clk) counter++;
+
+  property my_prop;
+    counter != 10
+  endproperty;
+
+  myChecker c(my_prop);
+endmodule

regression/verilog/checker/checker4.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+checker4.sv
+--bound 20
+^\[main\.c\.assert\.1\] always myChecker\.data != 10: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Support for untyped checker parameters is missing.

regression/verilog/checker/checker4.sv

@@ -0,0 +1,9 @@
+checker myChecker(untyped x);
+  assert property (x != 10);
+endchecker
+
+module main(input clk);
+  reg [31:0] counter = 0;
+  always_ff @(posedge clk) counter++;
+  myChecker c(counter);
+endmodule

src/hw_cbmc_irep_ids.h

@@ -100,6 +100,7 @@ IREP_ID_ONE(verilog_indexed_part_select_minus)
 IREP_ID_ONE(verilog_past)
 IREP_ID_ONE(verilog_property_declaration)
 IREP_ID_ONE(verilog_sequence_declaration)
+IREP_ID_ONE(verilog_sequence)
 IREP_ID_ONE(verilog_value_range)
 IREP_ID_ONE(verilog_void)
 IREP_ID_ONE(verilog_streaming_concatenation_left_to_right)

src/verilog/parser.y

@@ -750,19 +750,68 @@ program_declaration:
         ;
 
 checker_declaration:
-	  TOK_CHECKER checker_identifier
-		{
-		  init($$, ID_verilog_checker);
-		  stack_expr($$).set(ID_base_name, stack_expr($2).id());
-		}
-	  ';'
+	  TOK_CHECKER { init($$); } checker_identifier
+	  checker_port_list_paren_opt ';'
 	  checker_or_generate_item_brace
 	  TOK_ENDCHECKER
 		{
-		  $$ = $3;
+		  init($$);
+		  irept attributes;
+		  exprt parameter_port_list;
+		  stack_expr($$) = verilog_parse_treet::create_module(
+		    attributes, // attributes,
+		    stack_expr($2), // module_keyword
+		    stack_expr($3), // name
+		    parameter_port_list, // parameter_port_list
+		    stack_expr($4), // ports
+		    stack_expr($6)  // module_items
+		  );
+		  stack_expr($$).id(ID_verilog_checker);
 		}
 	;
 
+checker_port_list_paren_opt:
+	  /* Optional */
+		{ init($$); }
+	| '(' checker_port_list_opt ')'
+		{ $$ = $2; }
+	;
+
+checker_port_list_opt:
+	  /* Optional */
+		{ init($$); }
+	| checker_port_list
+	;
+
+checker_port_list:
+	  checker_port_item
+		{ init($$); mts($$, $1); }
+	| checker_port_list checker_port_item
+		{ $$ = $1; mts($$, $2); }
+	;
+
+checker_port_item:
+	  attribute_instance_brace
+	  checker_port_direction_opt
+	  property_formal_type
+	  formal_port_identifier
+	  variable_dimension_brace
+		{ init($$, ID_decl);
+                  stack_expr($$).set(ID_class, stack_expr($2).id());
+                  addswap($$, ID_type, $3);
+		  mto($$, $4); /* declarator */
+		}
+	;
+
+checker_port_direction_opt:
+	  /* Optional */
+		{ init($$); }
+	| TOK_INPUT
+		{ init($$, ID_input); }
+	| TOK_OUTPUT
+		{ init($$, ID_output); }
+	;
+
 class_declaration:
 	  TOK_CLASS class_identifier
 	  ';'
@@ -1030,7 +1079,9 @@ non_port_interface_item:
 
 checker_or_generate_item_brace:
 	  /* Optional */
+		{ init($$); }
 	| checker_or_generate_item_brace attribute_instance_brace checker_or_generate_item
+		{ $$ = $1; mts($$, $3); }
 	;
 
 checker_or_generate_item:
@@ -2323,7 +2374,8 @@ property_port_item:
 	;
 
 property_formal_type:
-	  TOK_PROPERTY
+	  sequence_formal_type
+	| TOK_PROPERTY
 	;
 
 property_spec:
@@ -2334,6 +2386,14 @@ property_spec:
 	| property_expr
 	;
 
+sequence_formal_type:
+	  data_type
+	| TOK_SEQUENCE
+		{ init($$, ID_verilog_sequence); }
+	| TOK_UNTYPED
+		{ init($$, ID_verilog_untyped); }
+	;
+
 // The 1800-2017 grammar has an ambiguity where
 // '(' expression ')' can either be an expression or a property_expr,
 // which yields a reduce/reduce conflict. Hence, we split the rules

src/verilog/verilog_expr.cpp

@@ -124,6 +124,13 @@ void verilog_checkert::show(std::ostream &out) const
 {
   out << "Checker: " << base_name() << '\n';
 
+  out << "  Ports:\n";
+
+  for(auto &port : ports())
+    out << "    " << port.pretty() << '\n';
+
+  out << '\n';
+
   out << "  Items:\n";
 
   for(auto &item : items())

src/verilog/verilog_expr.h

@@ -2354,6 +2354,18 @@ class verilog_checkert : public verilog_item_containert
   {
   }
 
+  using portst = std::vector<verilog_declt>;
+
+  portst &ports()
+  {
+    return (portst &)(add(ID_ports).get_sub());
+  }
+
+  const portst &ports() const
+  {
+    return (const portst &)(find(ID_ports).get_sub());
+  }
+
   void show(std::ostream &) const;
 };
 

src/verilog/verilog_parse_tree.cpp

@@ -61,7 +61,7 @@ void verilog_parse_treet::modules_provided(
 {
   for(auto &item : items)
   {
-    if(item.id() == ID_verilog_module)
+    if(item.id() == ID_verilog_module || item.id() == ID_verilog_checker)
     {
       module_set.insert(id2string(
         verilog_module_symbol(to_verilog_module_source(item).base_name())));
@@ -92,7 +92,7 @@ void verilog_parse_treet::build_item_map()
 
   for(const auto &item : items)
   {
-    if(item.id() == ID_verilog_module)
+    if(item.id() == ID_verilog_module || item.id() == ID_verilog_checker)
     {
       auto &verilog_module = to_verilog_module_source(item);
       item_map[verilog_module.base_name()] = &verilog_module;