Merge pull request #831 from diffblue/checker1

SystemVerilog: grammar for checkers
diffblue · Nov 20, 2024 · 8642dd3 · 8642dd3
2 parents f7c3108 + fae82ea
commit 8642dd3
Show file tree

Hide file tree

Showing 7 changed files with 106 additions and 1 deletion.
diff --git a/regression/verilog/checker/checker1.desc b/regression/verilog/checker/checker1.desc
@@ -0,0 +1,7 @@
+CORE
+checker1.sv
+--show-parse
+^Checker: myChecker$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/verilog/checker/checker1.sv b/regression/verilog/checker/checker1.sv
@@ -0,0 +1,5 @@
+checker myChecker;
+endchecker
+
+module main;
+endmodule
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
@@ -119,6 +119,7 @@ IREP_ID_ONE(negedge)
 IREP_ID_ONE(posedge)
 IREP_ID_ONE(event_guard)
 IREP_ID_ONE(verilog_star_event)
+IREP_ID_ONE(verilog_checker)
 IREP_ID_ONE(verilog_cycle_delay)
 IREP_ID_ONE(delay)
 IREP_ID_ONE(verilog_non_blocking_assign)

diff --git a/src/verilog/parser.y b/src/verilog/parser.y
@@ -746,6 +746,20 @@ program_declaration:
           TOK_PROGRAM TOK_ENDPROGRAM
         ;
 
+checker_declaration:
+	  TOK_CHECKER checker_identifier
+		{
+		  init($$, ID_verilog_checker);
+		  stack_expr($$).set(ID_base_name, stack_expr($2).id());
+		}
+	  ';'
+	  checker_or_generate_item_brace
+	  TOK_ENDCHECKER
+		{
+		  $$ = $3;
+		}
+	;
+
 class_declaration:
 	  TOK_CLASS class_identifier
 	  ';'
@@ -1007,6 +1021,42 @@ non_port_interface_item:
 	| interface_declaration
 	/* | timeunits_declaration */
 	;
+
+// System Verilog standard 1800-2017
+// A.1.9 Checker items
+
+checker_or_generate_item_brace:
+	  /* Optional */
+	| checker_or_generate_item_brace attribute_instance_brace checker_or_generate_item
+	;
+
+checker_or_generate_item:
+	  checker_or_generate_item_declaration
+	| initial_construct
+	| always_construct
+	| final_construct
+	| assertion_item
+	| continuous_assign
+	| checker_generate_item
+	;
+
+checker_or_generate_item_declaration:
+	  data_declaration
+	| function_declaration
+	| checker_declaration
+	| assertion_item_declaration
+	| covergroup_declaration
+	| genvar_declaration
+	| TOK_DEFAULT TOK_CLOCKING clocking_identifier ';'
+	| TOK_DEFAULT TOK_DISABLE TOK_IFF expression_or_dist ';'
+	| ';'
+	;
+
+checker_generate_item:
+	  loop_generate_construct
+	| conditional_generate_construct
+	| generate_region
+	;
 
 // System Verilog standard 1800-2017
 // A.1.9 Class items
@@ -1170,6 +1220,7 @@ package_or_generate_item_declaration:
 	| data_declaration
 	| task_declaration
 	| function_declaration
+	| checker_declaration
 	| class_declaration
 	| local_parameter_declaration ';'
 	| parameter_declaration ';'
@@ -4076,6 +4127,10 @@ endmodule_identifier_opt:
 	| TOK_COLON module_identifier
 	;
 
+clocking_identifier: TOK_NON_TYPE_IDENTIFIER;
+
+checker_identifier: TOK_NON_TYPE_IDENTIFIER;
+
 net_identifier: identifier;
 
 package_identifier: TOK_NON_TYPE_IDENTIFIER;

diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp
@@ -112,6 +112,18 @@ std::vector<irep_idt> verilog_item_containert::dependencies() const
   return result;
 }
 
+void verilog_checkert::show(std::ostream &out) const
+{
+  out << "Checker: " << base_name() << '\n';
+
+  out << "  Items:\n";
+
+  for(auto &item : items())
+    out << "    " << item.pretty() << '\n';
+
+  out << '\n';
+}
+
 void verilog_packaget::show(std::ostream &out) const
 {
   out << "Pacakge: " << base_name() << '\n';

diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h
@@ -2143,6 +2143,29 @@ inline verilog_module_sourcet &to_verilog_module_source(irept &irep)
   return static_cast<verilog_module_sourcet &>(irep);
 }
 
+class verilog_checkert : public verilog_item_containert
+{
+public:
+  explicit verilog_checkert(irep_idt _base_name)
+    : verilog_item_containert(ID_verilog_module, _base_name)
+  {
+  }
+
+  void show(std::ostream &) const;
+};
+
+inline const verilog_checkert &to_verilog_checker(const irept &irep)
+{
+  PRECONDITION(irep.id() == ID_verilog_checker);
+  return static_cast<const verilog_checkert &>(irep);
+}
+
+inline verilog_checkert &to_verilog_checker(irept &irep)
+{
+  PRECONDITION(irep.id() == ID_verilog_checker);
+  return static_cast<verilog_checkert &>(irep);
+}
+
 class verilog_packaget : public verilog_item_containert
 {
 public:

diff --git a/src/verilog/verilog_parse_tree.cpp b/src/verilog/verilog_parse_tree.cpp
@@ -131,7 +131,9 @@ Function: verilog_parse_treet::show
 
 void verilog_parse_treet::show(const itemt &item, std::ostream &out) const
 {
-  if(item.id() == ID_verilog_class)
+  if(item.id() == ID_verilog_checker)
+    to_verilog_checker(item).show(out);
+  else if(item.id() == ID_verilog_class)
     to_verilog_class(item).show(out);
   else if(item.id() == ID_verilog_interface)
     to_verilog_interface(item).show(out);