SystemVerilog: parsing and type checking for default

This adds parsing and type checking for default clocking and default disable
iff.

Synthesis support is still missing.

Author: kroening

regression/verilog/SVA/default_disable1.desc

@@ -1,7 +1,8 @@
-KNOWNBUG
+CORE
 default_disable1.sv
 
-^EXIT=10$
+^file .* line 5: default disable iff is unsupported$
+^EXIT=2$
 ^SIGNAL=0$
 --
 ^warning: ignoring

src/hw_cbmc_irep_ids.h

@@ -80,6 +80,8 @@ IREP_ID_ONE(verilog_array_range)
 IREP_ID_ONE(verilog_assignment_pattern)
 IREP_ID_ONE(verilog_associative_array)
 IREP_ID_ONE(verilog_declarations)
+IREP_ID_ONE(verilog_default_clocking)
+IREP_ID_ONE(verilog_default_disable)
 IREP_ID_ONE(verilog_lifetime)
 IREP_ID_ONE(verilog_logical_equality)
 IREP_ID_ONE(verilog_logical_inequality)

src/verilog/parser.y

@@ -1032,7 +1032,9 @@ module_or_generate_item_declaration:
 	| genvar_declaration
 	| clocking_declaration
 	| TOK_DEFAULT TOK_CLOCKING clocking_identifier ';'
+		{ init($$, ID_verilog_default_clocking); mto($$, $3); }
 	| TOK_DEFAULT TOK_DISABLE TOK_IFF expression_or_dist ';'
+		{ init($$, ID_verilog_default_disable); mto($$, $4); }
 	;
 
 non_port_module_item:

src/verilog/verilog_elaborate.cpp

@@ -850,6 +850,12 @@ void verilog_typecheckt::collect_symbols(
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }
+  else if(module_item.id() == ID_verilog_default_clocking)
+  {
+  }
+  else if(module_item.id() == ID_verilog_default_disable)
+  {
+  }
   else if(module_item.id() == ID_verilog_property_declaration)
   {
     collect_symbols(to_verilog_property_declaration(module_item));

src/verilog/verilog_interfaces.cpp

@@ -306,6 +306,12 @@ void verilog_typecheckt::interface_module_item(
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }
+  else if(module_item.id() == ID_verilog_default_clocking)
+  {
+  }
+  else if(module_item.id() == ID_verilog_default_disable)
+  {
+  }
   else if(module_item.id() == ID_verilog_property_declaration)
   {
   }

src/verilog/verilog_synthesis.cpp

@@ -3282,6 +3282,14 @@ void verilog_synthesist::synth_module_item(
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }
+  else if(module_item.id() == ID_verilog_default_clocking)
+  {
+  }
+  else if(module_item.id() == ID_verilog_default_disable)
+  {
+    throw errort().with_location(module_item.source_location())
+      << "default disable iff is unsupported";
+  }
   else if(module_item.id() == ID_verilog_property_declaration)
   {
   }

src/verilog/verilog_typecheck.cpp

@@ -1740,6 +1740,17 @@ void verilog_typecheckt::convert_module_item(
   else if(module_item.id() == ID_verilog_covergroup)
   {
   }
+  else if(module_item.id() == ID_verilog_default_clocking)
+  {
+    exprt &cond = to_unary_expr(module_item).op();
+    convert_expr(cond);
+  }
+  else if(module_item.id() == ID_verilog_default_disable)
+  {
+    exprt &cond = to_unary_expr(module_item).op();
+    convert_expr(cond);
+    make_boolean(cond);
+  }
   else if(module_item.id() == ID_verilog_property_declaration)
   {
     convert_property_declaration(to_verilog_property_declaration(module_item));