SystemVerilog: event data type

This adds 1800-2017 6.17 event.

Author: kroening

regression/verilog/data-types/event1.desc

@@ -0,0 +1,6 @@
+CORE
+event1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--

regression/verilog/data-types/event1.sv

@@ -0,0 +1,15 @@
+module main;
+
+  // IEEE 1800-2017 6.17
+  event done;
+  event empty = null;
+
+  task trigger_done;
+    -> done;
+  endtask
+
+  task wait_until_done;
+    @ done;
+  endtask
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -106,7 +106,8 @@ IREP_ID_ONE(verilog_streaming_concatenation_left_to_right)
 IREP_ID_ONE(verilog_streaming_concatenation_right_to_left)
 IREP_ID_ONE(verilog_chandle)
 IREP_ID_ONE(verilog_null)
-IREP_ID_ONE(event)
+IREP_ID_ONE(verilog_event)
+IREP_ID_ONE(verilog_event_trigger)
 IREP_ID_ONE(reg)
 IREP_ID_ONE(macromodule)
 IREP_ID_ONE(output_register)

src/verilog/expr2verilog.cpp

@@ -1208,7 +1208,7 @@ expr2verilogt::resultt expr2verilogt::convert_constant(
     ieee_float.from_expr(tmp);
     return {precedence, ieee_float.to_ansi_c_string()};
   }
-  else if(type.id() == ID_verilog_chandle)
+  else if(type.id() == ID_verilog_chandle || type.id() == ID_verilog_event)
   {
     if(src.get_value() == ID_NULL)
     {
@@ -1989,6 +1989,8 @@ std::string expr2verilogt::convert(const typet &type)
   }
   else if(type.id() == ID_verilog_chandle)
     return "chandle";
+  else if(type.id() == ID_verilog_event)
+    return "event";
   else if(type.id() == ID_verilog_genvar)
     return "genvar";
   else if(type.id()==ID_integer)

src/verilog/parser.y

@@ -1482,7 +1482,7 @@ data_type:
                   $$ = $2; }
 //	| class_type
 	| TOK_EVENT
-	        { init($$, ID_event); }
+	        { init($$, ID_verilog_event); }
 	/*
 	| ps_covergroup_identifier
 	*/
@@ -3382,7 +3382,7 @@ event_control:
 
 ored_event_expression:
 	  event_expression
-		{ init($$, ID_event); mto($$, $1); }
+		{ init($$, ID_verilog_event); mto($$, $1); }
 	| ored_event_expression TOK_OR event_expression
 		{ $$=$1; mto($$, $3); }
 	| ored_event_expression ',' event_expression
@@ -3857,6 +3857,7 @@ function_subroutine_call: subroutine_call
         ;
 
 event_trigger: TOK_MINUSGREATER hierarchical_event_identifier ';'
+		{ init($$, ID_verilog_event_trigger); mto($$, $2); }
 	;
 
 // System Verilog standard 1800-2017

src/verilog/verilog_elaborate.cpp

@@ -751,6 +751,9 @@ void verilog_typecheckt::collect_symbols(const verilog_statementt &statement)
   else if(statement.id() == ID_wait)
   {
   }
+  else if(statement.id() == ID_verilog_event_trigger)
+  {
+  }
   else
     DATA_INVARIANT(false, "unexpected statement: " + statement.id_string());
 }

src/verilog/verilog_elaborate_type.cpp

@@ -256,6 +256,10 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
     result.set(ID_C_identifier, enum_type.identifier());
     return result.with_source_location(source_location);
   }
+  else if(src.id() == ID_verilog_event)
+  {
+    return src;
+  }
   else if(src.id() == ID_verilog_packed_array)
   {
     return convert_packed_array_type(to_type_with_subtype(src));

src/verilog/verilog_lowering.cpp

@@ -189,6 +189,11 @@ exprt verilog_lowering(exprt expr)
       // this is 'null'
       return to_verilog_chandle_type(expr.type()).null_expr();
     }
+    else if(expr.type().id() == ID_verilog_event)
+    {
+      // this is 'null'
+      return to_verilog_event_type(expr.type()).null_expr();
+    }
 
     return expr;
   }
@@ -201,6 +206,11 @@ exprt verilog_lowering(exprt expr)
       return symbol_exprt{
         symbol_expr.get_identifier(), chandle_type.encoding()};
     }
+    else if(expr.type().id() == ID_verilog_event)
+    {
+      auto &event_type = to_verilog_event_type(expr.type());
+      return symbol_exprt{symbol_expr.get_identifier(), event_type.encoding()};
+    }
     else
       return expr;
   }
@@ -441,6 +451,8 @@ typet verilog_lowering(typet type)
     return lower_to_aval_bval(type);
   else if(type.id() == ID_verilog_chandle)
     return to_verilog_chandle_type(type).encoding();
+  else if(type.id() == ID_verilog_event)
+    return to_verilog_event_type(type).encoding();
   else
     return type;
 }

src/verilog/verilog_synthesis.cpp

@@ -3185,6 +3185,10 @@ void verilog_synthesist::synth_statement(
   }
   else if(statement.id() == ID_verilog_label_statement)
     synth_statement(to_verilog_label_statement(statement).statement());
+  else if(statement.id() == ID_verilog_event_trigger)
+  {
+    // not synthesized
+  }
   else
   {
     throw errort().with_location(statement.source_location())
@@ -3348,8 +3352,6 @@ void verilog_synthesist::synth_assignments(
 
   auto lhs = symbol_expr(symbol, curr_or_next);
 
-  if(lhs.type() != new_value.type())
-    throw errort() << lhs.pretty() << "\nVS\n" << new_value.pretty();
   DATA_INVARIANT(
     lhs.type() == new_value.type(), "synth_assignments type consistency");
 

src/verilog/verilog_typecheck.cpp

@@ -1613,6 +1613,10 @@ void verilog_typecheckt::convert_statement(
   else if(statement.id() == ID_wait)
   {
   }
+  else if(statement.id() == ID_verilog_event_trigger)
+  {
+    convert_expr(to_unary_expr(statement).op());
+  }
   else
   {
     throw errort().with_location(statement.source_location())