Merge pull request #839 from diffblue/verilog_event

SystemVerilog: `event` data type

Author: kroening

CHANGELOG

@@ -6,7 +6,7 @@
 * Verilog: fix for nor/nand/xnor primitive gates
 * SystemVerilog: $bitstoreal/$bitstoshortreal, $realtobits/$shortrealtobits
 * SystemVerilog: $itor, $rtoi
-* SystemVerilog: chandle
+* SystemVerilog: chandle, event
 
 # EBMC 5.4
 

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,18 @@
+module main;
+
+  // IEEE 1800-2017 6.17
+  event done;
+  event empty = null;
+
+  task trigger_done;
+    -> done;
+  endtask
+
+  task wait_until_done;
+    @ done;
+  endtask
+
+  p0: assert final (empty == null);
+  p1: assert final ($typename(event) == "event");
+
+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

@@ -1260,7 +1260,7 @@ expr2verilogt::resultt expr2verilogt::convert_constant(
 
     dest += '"';
   }
-  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)
     {
@@ -2041,6 +2041,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

@@ -1486,7 +1486,7 @@ data_type:
                   $$ = $2; }
 //	| class_type
 	| TOK_EVENT
-	        { init($$, ID_event); }
+	        { init($$, ID_verilog_event); }
 	/*
 	| ps_covergroup_identifier
 	*/
@@ -3403,7 +3403,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
@@ -3878,6 +3878,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

@@ -302,6 +302,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

@@ -47,6 +47,10 @@ typet verilog_lowering(typet type)
   {
     return to_verilog_chandle_type(type).encoding();
   }
+  else if(type.id() == ID_verilog_event)
+  {
+    return to_verilog_event_type(type).encoding();
+  }
   else
     return type;
 }
@@ -357,6 +361,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;
   }
@@ -369,6 +378,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;
   }

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())