Merge pull request #839 from diffblue/verilog_event

SystemVerilog: `event` data type

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

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

src/verilog/verilog_typecheck_expr.cpp

@@ -345,7 +345,7 @@ exprt verilog_typecheck_exprt::convert_expr_rec(exprt expr)
 {
   // variable number of operands
 
-  if(expr.id() == ID_event)
+  if(expr.id() == ID_verilog_event)
   {
     expr.type() = bool_typet();
 
@@ -757,6 +757,10 @@ exprt verilog_typecheck_exprt::typename_string(const exprt &expr)
   {
     s = "chandle";
   }
+  else if(type.id() == ID_verilog_event)
+  {
+    s = "event";
+  }
   else
     s = "?";
 
@@ -2052,7 +2056,9 @@ void verilog_typecheck_exprt::implicit_typecast(
   }
   else if(src_type.id() == ID_verilog_null)
   {
-    if(dest_type.id() == ID_verilog_chandle)
+    if(
+      dest_type.id() == ID_verilog_chandle ||
+      dest_type.id() == ID_verilog_event)
     {
       if(expr.id() == ID_constant)
       {
@@ -2319,6 +2325,12 @@ typet verilog_typecheck_exprt::max_type(
   if(vt0.is_chandle() || vt1.is_null())
     return t0;
 
+  if(vt0.is_null() || vt1.is_event())
+    return t1;
+
+  if(vt0.is_event() || vt1.is_null())
+    return t0;
+
   if(vt0.is_other() || vt1.is_other())
     return static_cast<const typet &>(get_nil_irep());
 

src/verilog/verilog_types.cpp

@@ -14,3 +14,8 @@ constant_exprt verilog_chandle_typet::null_expr() const
 {
   return encoding().all_zeros_expr();
 }
+
+constant_exprt verilog_event_typet::null_expr() const
+{
+  return encoding().all_zeros_expr();
+}

src/verilog/verilog_types.h

@@ -581,4 +581,41 @@ inline verilog_chandle_typet &to_verilog_chandle_type(typet &type)
   return static_cast<verilog_chandle_typet &>(type);
 }
 
+/// The SystemVerilog event type
+class verilog_event_typet : public typet
+{
+public:
+  verilog_event_typet() : typet(ID_verilog_event)
+  {
+  }
+
+  constant_exprt null_expr() const;
+
+  bv_typet encoding() const
+  {
+    return bv_typet{32};
+  }
+};
+
+/// \brief Cast a typet to a \ref verilog_event_typet
+///
+/// This is an unchecked conversion. \a type must be known to be \ref
+/// verilog_event_typet. Will fail with a precondition violation if type
+/// doesn't match.
+///
+/// \param type: Source type.
+/// \return Object of type \ref verilog_event_typet
+inline const verilog_event_typet &to_verilog_event_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_verilog_event);
+  return static_cast<const verilog_event_typet &>(type);
+}
+
+/// \copydoc to_event_type(const typet &)
+inline verilog_event_typet &to_verilog_event_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_verilog_event);
+  return static_cast<verilog_event_typet &>(type);
+}
+
 #endif

src/verilog/vtype.cpp

@@ -78,6 +78,11 @@ vtypet::vtypet(const typet &type)
     vtype = CHANDLE;
     width = 32;
   }
+  else if(type.id() == ID_verilog_event)
+  {
+    vtype = EVENT;
+    width = 32;
+  }
   else 
   {
     width=0;
@@ -122,16 +127,18 @@ std::ostream &operator << (std::ostream &out, const vtypet &vtype)
   case vtypet::VERILOG_REAL:
     return out << "real";
 
+  case vtypet::NULL_TYPE:
+    return out << "null";
+
   case vtypet::CHANDLE:
     return out << "chandle";
 
-  case vtypet::NULL_TYPE:
-    return out << "null";
+  case vtypet::EVENT:
+    return out << "event";
 
   case vtypet::UNKNOWN:
   case vtypet::OTHER:
   default:
     return out << "?";
   }
 }
-

src/verilog/vtype.h

@@ -31,13 +31,17 @@ class vtypet
   {
     return vtype == VERILOG_REAL;
   }
+  bool is_null() const
+  {
+    return vtype == NULL_TYPE;
+  }
   bool is_chandle() const
   {
     return vtype == CHANDLE;
   }
-  bool is_null() const
+  inline bool is_event() const
   {
-    return vtype == NULL_TYPE;
+    return vtype == EVENT;
   }
   inline bool is_other() const { return vtype==OTHER; }
 
@@ -52,8 +56,9 @@ class vtypet
     VERILOG_SIGNED,
     VERILOG_UNSIGNED,
     VERILOG_REAL,
-    CHANDLE,
     NULL_TYPE,
+    CHANDLE,
+    EVENT,
     OTHER
   } _vtypet;
   _vtypet vtype;