SystemVerilog: clocking declarations

This adds parsing for 1800-2017 14.3 clocking block declarations.

Author: kroening

CHANGELOG

@@ -11,6 +11,7 @@
 * SystemVerilog: chandle, event, string
 * SystemVerilog: package scope operator
 * SystemVerilog: checkers
+* SystemVerilog: clocking block declarations
 
 # EBMC 5.4
 

regression/verilog/clocking/clocking1.desc

@@ -0,0 +1,9 @@
+CORE
+clocking1.sv
+
+^no properties$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/clocking/clocking1.sv

@@ -0,0 +1,10 @@
+module main(input clk);
+
+  clocking my_clocking @(posedge clk);
+  endclocking
+
+  // The identifier is optional.
+  default clocking @(posedge clk);
+  endclocking
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -132,6 +132,7 @@ IREP_ID_ONE(posedge)
 IREP_ID_ONE(event_guard)
 IREP_ID_ONE(verilog_star_event)
 IREP_ID_ONE(verilog_checker)
+IREP_ID_ONE(verilog_clocking)
 IREP_ID_ONE(verilog_cycle_delay)
 IREP_ID_ONE(delay)
 IREP_ID_ONE(verilog_non_blocking_assign)

src/verilog/parser.y

@@ -1024,6 +1024,9 @@ module_or_generate_item:
 module_or_generate_item_declaration:
           package_or_generate_item_declaration
 	| genvar_declaration
+	| clocking_declaration
+	| TOK_DEFAULT TOK_CLOCKING clocking_identifier ';'
+	| TOK_DEFAULT TOK_DISABLE TOK_IFF expression_or_dist ';'
 	;
 
 non_port_module_item:
@@ -1106,6 +1109,7 @@ checker_or_generate_item_declaration:
 	| assertion_item_declaration
 	| covergroup_declaration
 	| genvar_declaration
+	| clocking_declaration
 	| TOK_DEFAULT TOK_CLOCKING clocking_identifier ';'
 	| TOK_DEFAULT TOK_DISABLE TOK_IFF expression_or_dist ';'
 	| ';'
@@ -3483,6 +3487,12 @@ delay_or_event_control:
 	        { init($$, ID_repeat); }
 	;
 
+
+delay_control_opt:
+	  /* Optional */
+	| delay_control
+	;
+
 delay_control:
 	  '#' delay_value
 		{ init($$, ID_delay); mto($$, $2); }
@@ -3754,11 +3764,73 @@ procedural_timing_control:
 // System Verilog standard 1800-2017
 // A.6.11 Clocking block
 
+clocking_declaration:
+	  TOK_DEFAULT TOK_CLOCKING clocking_identifier_opt clocking_event ';'
+	  clocking_item_brace
+	  TOK_ENDCLOCKING
+		{ init($$, ID_verilog_clocking); }
+	| TOK_CLOCKING clocking_identifier_opt clocking_event ';'
+	  clocking_item_brace
+	  TOK_ENDCLOCKING
+		{ init($$, ID_verilog_clocking); }
+	| TOK_GLOBAL TOK_CLOCKING clocking_identifier_opt clocking_event ';'
+	  TOK_ENDCLOCKING
+		{ init($$, ID_verilog_clocking); }
+	;
+
+clocking_identifier_opt:
+	  /* Optional */
+	| clocking_identifier
+	;
+
 clocking_event:
 	  '@' identifier
 	| '@' '(' event_expression ')'
 	;
 
+clocking_item_brace:
+	  /* Optional */
+	| clocking_item_brace clocking_item
+	;
+
+clocking_item:
+	  TOK_DEFAULT default_skew ';'
+	| attribute_instance_brace assertion_item_declaration
+	;
+
+default_skew:
+	  TOK_INPUT clocking_skew
+	| TOK_OUTPUT clocking_skew
+	| TOK_INPUT clocking_skew TOK_OUTPUT clocking_skew
+	;
+
+clocking_direction:
+	  TOK_INPUT clocking_skew_opt
+	| TOK_OUTPUT clocking_skew_opt
+	| TOK_INPUT clocking_skew_opt TOK_OUTPUT clocking_skew_opt
+	| TOK_INOUT
+	;
+
+list_of_clocking_decl_assign:
+	  clocking_decl_assign
+	| list_of_clocking_decl_assign ',' clocking_decl_assign
+	;
+
+clocking_decl_assign:
+	  signal_identifier
+	| signal_identifier '=' expression
+	;
+
+clocking_skew_opt:
+	  /* Optional */
+	| clocking_skew
+	;
+
+clocking_skew:
+	  edge_identifier delay_control_opt
+	| delay_control
+	;
+
 cycle_delay:
           "##" number
                 { init($$, ID_verilog_cycle_delay); mto($$, $2); }
@@ -4297,6 +4369,8 @@ class_identifier: TOK_NON_TYPE_IDENTIFIER;
 
 constraint_identifier: TOK_NON_TYPE_IDENTIFIER;
 
+edge_identifier: identifier;
+
 formal_port_identifier: identifier;
 
 genvar_identifier: identifier;
@@ -4335,6 +4409,8 @@ memory_identifier: identifier;
 
 method_identifier: identifier;
 
+signal_identifier: identifier;
+
 type_identifier: TOK_TYPE_IDENTIFIER
 		{
 		  init($$, ID_typedef_type);

src/verilog/verilog_elaborate.cpp

@@ -844,6 +844,9 @@ void verilog_typecheckt::collect_symbols(
   else if(module_item.id() == ID_verilog_package_import)
   {
   }
+  else if(module_item.id() == ID_verilog_clocking)
+  {
+  }
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }

src/verilog/verilog_interfaces.cpp

@@ -300,6 +300,9 @@ void verilog_typecheckt::interface_module_item(
   else if(module_item.id() == ID_verilog_package_import)
   {
   }
+  else if(module_item.id() == ID_verilog_clocking)
+  {
+  }
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }

src/verilog/verilog_synthesis.cpp

@@ -3276,6 +3276,9 @@ void verilog_synthesist::synth_module_item(
   {
     // done already
   }
+  else if(module_item.id() == ID_verilog_clocking)
+  {
+  }
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }

src/verilog/verilog_typecheck.cpp

@@ -1734,6 +1734,9 @@ void verilog_typecheckt::convert_module_item(
   else if(module_item.id() == ID_verilog_package_import)
   {
   }
+  else if(module_item.id() == ID_verilog_clocking)
+  {
+  }
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }