Verilog: aval/bval encoding for zero extension

This adds an aval/bval encoding for zero extension.

Author: kroening

regression/verilog/expressions/equality4.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
-equality4.v
+CORE
+equality4.sv
 
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-zero_extend doesn't work for four-valued operands.

regression/verilog/expressions/equality4.sv

@@ -4,8 +4,4 @@ module main;
   initial assert((2'b10 + 1'sbx) === 8'bxxxxxxxx);
   initial assert((2'b10 | 1'sbx) === 8'b0000001x);
 
-  // The two operands are sign-extended to 8 bits.
-  initial assert((2'sb10 + 1'sbx) === 8'sbxxxxxxxx);
-  initial assert((2'sb10 | 1'sbx) === 8'sb1111111x);
-
 endmodule

regression/verilog/expressions/equality5.desc

@@ -0,0 +1,9 @@
+KNOWNBUG
+equality5.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+This gives the wrong answer.

regression/verilog/expressions/equality5.sv

@@ -0,0 +1,7 @@
+module main;
+
+  // The two operands are sign-extended to 8 bits.
+  initial assert((2'sb10 + 1'sbx) === 8'sbxxxxxxxx);
+  initial assert((2'sb10 | 1'sbx) === 8'sb1111111x);
+
+endmodule

src/verilog/aval_bval_encoding.cpp

@@ -627,6 +627,23 @@ exprt aval_bval(const binary_relation_exprt &expr)
     aval_bval_conversion(two_valued_expr, lower_to_aval_bval(type))};
 }
 
+exprt aval_bval(const zero_extend_exprt &expr)
+{
+  PRECONDITION(is_four_valued(expr.type()));
+
+  // extend aval and bval separately
+  auto op_aval = aval(expr.op());
+  auto op_bval = bval(expr.op());
+
+  auto result_type = lower_to_aval_bval(expr.type());
+  auto extended_type = bv_typet{aval_bval_width(result_type)};
+
+  auto aval_extended = zero_extend_exprt{op_aval, extended_type};
+  auto bval_extended = zero_extend_exprt{op_bval, extended_type};
+
+  return combine_aval_bval(aval_extended, bval_extended, result_type);
+}
+
 exprt default_aval_bval_lowering(const exprt &expr)
 {
   auto &type = expr.type();

src/verilog/aval_bval_encoding.h

@@ -71,6 +71,8 @@ exprt aval_bval(const typecast_exprt &);
 exprt aval_bval(const shift_exprt &);
 /// lowering for <=, <, etc.
 exprt aval_bval(const binary_relation_exprt &);
+/// lowering for zero extension
+exprt aval_bval(const zero_extend_exprt &);
 
 /// If any operand has x/z, then the result is 'x'.
 /// Otherwise, the result is the expression applied to the aval

src/verilog/verilog_lowering.cpp

@@ -682,6 +682,13 @@ exprt verilog_lowering(exprt expr)
     else
       return expr;
   }
+  else if(expr.id() == ID_zero_extend)
+  {
+    if(is_four_valued(expr.type()))
+      return aval_bval(to_zero_extend_expr(expr));
+    else
+      return expr;
+  }
   else
     return expr; // leave as is