Verilog: use zero_extend_exprt

regression/ebmc/smv-word-level/verilog6.desc

@@ -0,0 +1,7 @@
+CORE
+verilog6.sv
+--smv-word-level
+^CTLSPEC 0ud8_1 \+ 0ub6_000000 :: -0sd2_1 = 0ud8_4$
+^EXIT=0$
+^SIGNAL=0$
+--

regression/ebmc/smv-word-level/verilog6.sv

@@ -0,0 +1,6 @@
+module main(input clk, input in);
+
+  // The RHS of the addition will be zero-extended
+  initial p1: assert property (8'b1 + 2'sb11 == 8'b100);
+
+endmodule

src/smvlang/expr2smv.cpp

@@ -350,6 +350,25 @@ expr2smvt::resultt expr2smvt::convert_typecast(const typecast_exprt &expr)
 
 /*******************************************************************\
 
+Function: expr2smvt::convert_zero_extend
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2smvt::resultt expr2smvt::convert_zero_extend(const zero_extend_exprt &expr)
+{
+  // Both "extend" and "resize" do sign extension.
+  // Hence, use lowering.
+  return convert_rec(expr.lower());
+}
+
+/*******************************************************************\
+
 Function: expr2smvt::convert_rtctl
 
   Inputs:
@@ -662,6 +681,20 @@ expr2smvt::resultt expr2smvt::convert_constant(const constant_exprt &src)
     dest = minus + std::string("0") + sign_specifier + 'd' +
            std::to_string(word_width) + '_' + integer2string(value_abs);
   }
+  else if(type.id() == ID_bv)
+  {
+    auto &bv_type = to_bv_type(type);
+    auto width = bv_type.width();
+    auto &src_value = src.get_value();
+    dest = std::string("0ub");
+    dest += std::to_string(width);
+    dest += '_';
+    for(std::size_t i = 0; i < width; i++)
+    {
+      bool bit = get_bvrep_bit(src_value, width, width - i - 1);
+      dest += bit ? '1' : '0';
+    }
+  }
   else
     return convert_norep(src);
 
@@ -912,6 +945,9 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
     return convert_typecast(to_typecast_expr(src));
   }
 
+  else if(src.id() == ID_zero_extend)
+    return convert_zero_extend(to_zero_extend_expr(src));
+
   else // no SMV language expression for internal representation
     return convert_norep(src);
 }

src/smvlang/expr2smv_class.h

@@ -131,6 +131,8 @@ class expr2smvt
 
   resultt convert_typecast(const typecast_exprt &);
 
+  resultt convert_zero_extend(const zero_extend_exprt &);
+
   resultt convert_norep(const exprt &);
 };
 

src/verilog/expr2verilog.cpp

@@ -2007,6 +2007,9 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
     return convert_function(src.id_string(), src);
   }
 
+  else if(src.id() == ID_zero_extend)
+    return convert_rec(to_zero_extend_expr(src).op());
+
   // no VERILOG language expression for internal representation
   return convert_norep(src);
 }

src/verilog/verilog_typecheck_expr.cpp

@@ -302,39 +302,6 @@ void verilog_typecheck_exprt::assignment_conversion(
 
 /*******************************************************************\
 
-Function: zero_extend
-
-  Inputs:
-
- Outputs:
-
- Purpose:
-
-\*******************************************************************/
-
-static exprt zero_extend(const exprt &expr, const typet &type)
-{
-  auto old_width = expr.type().id() == ID_bool ? 1
-                   : expr.type().id() == ID_integer
-                     ? 32
-                     : to_bitvector_type(expr.type()).get_width();
-
-  // first make unsigned
-  typet tmp_type;
-
-  if(type.id() == ID_unsignedbv)
-    tmp_type = unsignedbv_typet{old_width};
-  else if(type.id() == ID_verilog_unsignedbv)
-    tmp_type = verilog_unsignedbv_typet{old_width};
-  else
-    PRECONDITION(false);
-
-  return typecast_exprt::conditional_cast(
-    typecast_exprt::conditional_cast(expr, tmp_type), type);
-}
-
-/*******************************************************************\
-
 Function: verilog_typecheck_exprt::downwards_type_progatation
 
   Inputs:
@@ -411,7 +378,7 @@ void verilog_typecheck_exprt::downwards_type_propagation(
     // "If the operand shall be extended, then it shall be sign-extended only
     // if the propagated type is signed."
     // A typecast from signed to a larger unsigned would sign extend.
-    expr = zero_extend(expr, type);
+    expr = zero_extend_exprt{expr, type};
   }
   else
   {