Verilog: four-valued size casts

This adds support for doing size casts of four-valued data types.

Author: kroening

regression/verilog/expressions/signed2.sv

@@ -12,7 +12,7 @@ module main;
   // base 8
   pB0: assert final ('so7 == -1);
   pB1: assert final ('so1 == 1);
-  pB2: assert final ('so7x === 'so3777777777x);
+  pB2: assert final ('so7x === 32'so3777777777x);
   pB3: assert final ($bits('so1) == 32);
   pB4: assert final ('so77 == -1);
   pB5: assert final (4'so7 == 7);

regression/verilog/expressions/size_cast2.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 size_cast2.sv
 --module main
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-This is not yet implemented.

src/verilog/aval_bval_encoding.cpp

@@ -188,22 +188,45 @@ exprt aval_bval_conversion(const exprt &src, const typet &dest)
 
   if(is_aval_bval(src.type()))
   {
+    // four-valued to four-valued
     auto src_width = aval_bval_width(src.type());
 
     if(src_width == dest_width)
     {
       // same size
       return typecast_exprt{src, dest};
     }
-    else
+    else if(src_width > dest_width)
     {
+      // shrink
       auto new_aval = adjust_size(aval(src), dest_width);
       auto new_bval = adjust_size(bval(src), dest_width);
       return combine_aval_bval(new_aval, new_bval, dest);
     }
+    else
+    {
+      // extend
+      auto underlying_src = aval_bval_underlying(src.type());
+      auto underlying_dest = aval_bval_underlying(dest);
+      
+      if(underlying_src.id() == ID_signedbv)
+      {
+        // sign extend both aval and bval
+        auto new_aval = typecast_exprt{typecast_exprt{typecast_exprt{aval(src), underlying_src}, underlying_dest}, bv_typet{dest_width}};
+        auto new_bval = typecast_exprt{typecast_exprt{typecast_exprt{bval(src), underlying_src}, underlying_dest}, bv_typet{dest_width}};
+        return combine_aval_bval(new_aval, new_bval, dest);
+      }
+      else
+      {
+        auto new_aval = adjust_size(aval(src), dest_width);
+        auto new_bval = adjust_size(bval(src), dest_width);      
+        return combine_aval_bval(new_aval, new_bval, dest);
+      }
+    }
   }
   else
   {
+    // two-valued to four-valued
     const bv_typet bv_type{dest_width};
     auto aval =
       typecast_exprt{typecast_exprt{src, aval_bval_underlying(dest)}, bv_type};
@@ -501,14 +524,25 @@ exprt aval_bval(const verilog_implies_exprt &expr)
 
 exprt aval_bval(const typecast_exprt &expr)
 {
-  // 'true' is defined as a "nonzero known value" (1800-2017 12.4).
+  auto &dest_type = expr.type();
+
   PRECONDITION(is_aval_bval(expr.op()));
-  PRECONDITION(expr.type().id() == ID_bool);
 
-  auto op_has_xz = ::has_xz(expr.op());
-  auto op_aval = aval(expr.op());
-  auto op_aval_zero = to_bv_type(op_aval.type()).all_zeros_expr();
-  return and_exprt{not_exprt{op_has_xz}, notequal_exprt{op_aval, op_aval_zero}};
+  if(dest_type.id() == ID_bool)
+  {
+    // 'true' is defined as a "nonzero known value" (1800-2017 12.4).
+    auto op_has_xz = ::has_xz(expr.op());
+    auto op_aval = aval(expr.op());
+    auto op_aval_zero = to_bv_type(op_aval.type()).all_zeros_expr();
+    return and_exprt{not_exprt{op_has_xz}, notequal_exprt{op_aval, op_aval_zero}};
+  }
+  else if(dest_type.id() == ID_verilog_unsignedbv || dest_type.id() == ID_verilog_signedbv)
+  {
+    auto aval_bval_type = lower_to_aval_bval(dest_type);
+    return aval_bval_conversion(expr.op(), aval_bval_type);
+  }
+  else
+    PRECONDITION(false);
 }
 
 exprt aval_bval(const shift_exprt &expr)

src/verilog/verilog_lowering.cpp

@@ -303,7 +303,7 @@ exprt verilog_lowering_cast(typecast_exprt expr)
     return std::move(new_cast);
   }
 
-  if(is_aval_bval(src_type) && dest_type.id() == ID_bool)
+  if(is_aval_bval(src_type))
   {
     // When casting a four-valued scalar to bool,
     // 'true' is defined as a "nonzero known value" (1800-2017 12.4).
@@ -480,7 +480,7 @@ exprt verilog_lowering(exprt expr)
   }
   else if(expr.id() == ID_verilog_explicit_size_cast)
   {
-    return to_verilog_explicit_size_cast_expr(expr).lower();
+    return verilog_lowering(to_verilog_explicit_size_cast_expr(expr).lower());
   }
   else if(
     expr.id() == ID_verilog_streaming_concatenation_left_to_right ||

src/verilog/verilog_typecheck_expr.cpp

@@ -3309,10 +3309,18 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     {
       expr.type() = signedbv_typet{new_size_int};
     }
+    else if(op_type.id() == ID_verilog_signedbv)
+    {
+      expr.type() = verilog_signedbv_typet{new_size_int};
+    }
     else if(op_type.id() == ID_unsignedbv || op_type.id() == ID_bool)
     {
       expr.type() = unsignedbv_typet{new_size_int};
     }
+    else if(op_type.id() == ID_verilog_unsignedbv)
+    {
+      expr.type() = verilog_unsignedbv_typet{new_size_int};
+    }
     else
     {
       throw errort().with_location(expr.source_location())