diff --git a/regression/verilog/data-types/chandle1.desc b/regression/verilog/data-types/chandle1.desc
new file mode 100644
index 000000000..c2bebfac1
--- /dev/null
+++ b/regression/verilog/data-types/chandle1.desc
@@ -0,0 +1,6 @@
+CORE
+chandle1.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/verilog/data-types/chandle1.sv b/regression/verilog/data-types/chandle1.sv
new file mode 100644
index 000000000..bf7f6048b
--- /dev/null
+++ b/regression/verilog/data-types/chandle1.sv
@@ -0,0 +1,9 @@
+module main;
+
+  // IEEE 1800-2017 6.14
+  chandle some_handle = null;
+
+  assert final (!some_handle);
+  assert final ($typename(some_handle) == "chandle");
+
+endmodule
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index 5bacb381b..032cfd77f 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -97,7 +97,8 @@ IREP_ID_ONE(verilog_property_declaration)
 IREP_ID_ONE(verilog_value_range)
 IREP_ID_ONE(verilog_streaming_concatenation_left_to_right)
 IREP_ID_ONE(verilog_streaming_concatenation_right_to_left)
-IREP_ID_ONE(chandle)
+IREP_ID_ONE(verilog_chandle)
+IREP_ID_ONE(verilog_null)
 IREP_ID_ONE(event)
 IREP_ID_ONE(reg)
 IREP_ID_ONE(macromodule)
diff --git a/src/verilog/Makefile b/src/verilog/Makefile
index 706413f09..74725a31c 100644
--- a/src/verilog/Makefile
+++ b/src/verilog/Makefile
@@ -25,6 +25,7 @@ SRC = aval_bval_encoding.cpp \
       verilog_typecheck_base.cpp \
       verilog_typecheck_expr.cpp \
       verilog_typecheck_sva.cpp \
+      verilog_types.cpp \
       verilog_y.tab.cpp \
       vtype.cpp
 
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
index 228488f21..3009b3979 100644
--- a/src/verilog/expr2verilog.cpp
+++ b/src/verilog/expr2verilog.cpp
@@ -1878,6 +1878,8 @@ std::string expr2verilogt::convert(const typet &type)
 
     return dest;
   }
+  else if(type.id() == ID_verilog_chandle)
+    return "chandle";
   else if(type.id() == ID_verilog_genvar)
     return "genvar";
   else if(type.id()==ID_integer)
@@ -1888,6 +1890,8 @@ std::string expr2verilogt::convert(const typet &type)
     return "real";
   else if(type.id()==ID_verilog_realtime)
     return "realtime";
+  else if(type.id() == ID_verilog_null)
+    return "null";
   else if(type.id() == ID_verilog_enum)
   {
     return "enum";
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index 5fbc846fd..e521daa3c 100644
--- a/src/verilog/parser.y
+++ b/src/verilog/parser.y
@@ -1453,7 +1453,7 @@ data_type:
 	| TOK_STRING
 	        { init($$, ID_string); }
 	| TOK_CHANDLE
-	        { init($$, ID_chandle); }
+	        { init($$, ID_verilog_chandle); }
 	| TOK_VIRTUAL interface_opt interface_identifier
 	        { init($$, "virtual_interface"); }
 	| /*scope_opt*/ type_identifier packed_dimension_brace
@@ -3955,7 +3955,7 @@ primary:  primary_literal
 	| cast
 	| assignment_pattern_expression
 	| streaming_concatenation
-        | TOK_NULL { init($$, ID_NULL); }
+        | TOK_NULL { init($$, ID_verilog_null); }
         | TOK_THIS { init($$, ID_this); }
 	;
 
diff --git a/src/verilog/verilog_elaborate_type.cpp b/src/verilog/verilog_elaborate_type.cpp
index 823354e64..de7218f74 100644
--- a/src/verilog/verilog_elaborate_type.cpp
+++ b/src/verilog/verilog_elaborate_type.cpp
@@ -333,6 +333,10 @@ typet verilog_typecheck_exprt::elaborate_type(const typet &src)
   {
     return src;
   }
+  else if(src.id() == ID_verilog_chandle)
+  {
+    return src;
+  }
   else
   {
     throw errort().with_location(source_location)
diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp
index 4be7fa22a..133464363 100644
--- a/src/verilog/verilog_lowering.cpp
+++ b/src/verilog/verilog_lowering.cpp
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "aval_bval_encoding.h"
 #include "verilog_bits.h"
 #include "verilog_expr.h"
+#include "verilog_types.h"
 
 exprt extract(
   const exprt &src,
@@ -157,9 +158,24 @@ exprt verilog_lowering(exprt expr)
     {
       return lower_to_aval_bval(to_constant_expr(expr));
     }
+    else if(expr.type().id() == ID_verilog_chandle)
+    {
+      // this is 'null'
+      return to_verilog_chandle_type(expr.type()).null_expr();
+    }
 
     return expr;
   }
+  else if(expr.id() == ID_symbol)
+  {
+    auto &symbol_expr = to_symbol_expr(expr);
+    if(expr.type().id() == ID_verilog_chandle)
+    {
+      return symbol_exprt{symbol_expr.get_identifier(), unsignedbv_typet{32}};
+    }
+    else
+      return expr;
+  }
   else if(expr.id() == ID_concatenation)
   {
     if(
diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp
index 2698d4796..f14ff51dd 100644
--- a/src/verilog/verilog_synthesis.cpp
+++ b/src/verilog/verilog_synthesis.cpp
@@ -3343,7 +3343,9 @@ void verilog_synthesist::synth_assignments(
   if(!symbol.is_state_var)
     post_process_wire(symbol.name, new_value);
 
-  equal_exprt equality_expr{symbol_expr(symbol, curr_or_next), new_value};
+  auto lhs = symbol_expr(symbol, curr_or_next);
+
+  equal_exprt equality_expr{std::move(lhs), new_value};
 
   constraints.add_to_operands(std::move(equality_expr));
 }
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index 983c073b9..56ab5f928 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/src/verilog/verilog_typecheck_expr.cpp
@@ -1004,6 +1004,11 @@ exprt verilog_typecheck_exprt::convert_nullary_expr(nullary_exprt expr)
     throw errort().with_location(expr.source_location())
       << "'this' outside of method";
   }
+  else if(expr.id() == ID_verilog_null)
+  {
+    return constant_exprt{ID_NULL, typet{ID_verilog_null}}.with_source_location(
+      expr.source_location());
+  }
   else
   {
     throw errort().with_location(expr.source_location())
@@ -2027,6 +2032,17 @@ void verilog_typecheck_exprt::implicit_typecast(
       return;
     }
   }
+  else if(src_type.id() == ID_verilog_null)
+  {
+    if(dest_type.id() == ID_verilog_chandle)
+    {
+      if(expr.id() == ID_constant)
+      {
+        expr.type() = dest_type;
+        return;
+      }
+    }
+  }
 
   throw errort().with_location(expr.source_location())
     << "failed to convert `" << to_string(src_type) << "' to `"
diff --git a/src/verilog/verilog_types.cpp b/src/verilog/verilog_types.cpp
new file mode 100644
index 000000000..75ecf9edc
--- /dev/null
+++ b/src/verilog/verilog_types.cpp
@@ -0,0 +1,16 @@
+/*******************************************************************\
+
+Module: Verilog Types
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include "verilog_types.h"
+
+#include <util/std_expr.h>
+
+constant_exprt verilog_chandle_typet::null_expr() const
+{
+  return encoding().all_zeros_expr();
+}
diff --git a/src/verilog/verilog_types.h b/src/verilog/verilog_types.h
index 24d076e46..40f4ec411 100644
--- a/src/verilog/verilog_types.h
+++ b/src/verilog/verilog_types.h
@@ -544,4 +544,41 @@ inline verilog_union_typet &to_verilog_union_type(typet &type)
   return static_cast<verilog_union_typet &>(type);
 }
 
+/// a pointer type
+class verilog_chandle_typet : public typet
+{
+public:
+  inline verilog_chandle_typet() : typet(ID_verilog_chandle)
+  {
+  }
+
+  bv_typet encoding() const
+  {
+    return bv_typet{32};
+  }
+
+  constant_exprt null_expr() const;
+};
+
+/// \brief Cast a typet to a \ref verilog_chandle_typet
+///
+/// This is an unchecked conversion. \a type must be known to be \ref
+/// verilog_chandle_typet. Will fail with a precondition violation if type
+/// doesn't match.
+///
+/// \param type: Source type.
+/// \return Object of type \ref verilog_chandle_typet
+inline const verilog_chandle_typet &to_verilog_chandle_type(const typet &type)
+{
+  PRECONDITION(type.id() == ID_verilog_chandle);
+  return static_cast<const verilog_chandle_typet &>(type);
+}
+
+/// \copydoc to_chandle_type(const typet &)
+inline verilog_chandle_typet &to_verilog_chandle_type(typet &type)
+{
+  PRECONDITION(type.id() == ID_verilog_chandle);
+  return static_cast<verilog_chandle_typet &>(type);
+}
+
 #endif