Verilog: lowering for four-valued zero-extend

This adds a lowering for zero_extend expressions for four-valued operands.

Author: kroening

src/verilog/aval_bval_encoding.cpp

@@ -470,3 +470,8 @@ exprt aval_bval(const shift_exprt &expr)
   auto x = make_x(expr.type());
   return if_exprt{distance_has_xz, x, combined};
 }
+
+exprt aval_bval(const zero_extend_exprt &expr)
+{
+  abort();
+}

src/verilog/aval_bval_encoding.h

@@ -65,5 +65,7 @@ exprt aval_bval(const verilog_implies_exprt &);
 exprt aval_bval(const typecast_exprt &);
 /// lowering for shifts
 exprt aval_bval(const shift_exprt &);
+/// lowering for zero extension
+exprt aval_bval(const zero_extend_exprt &);
 
 #endif

src/verilog/verilog_lowering.cpp

@@ -625,6 +625,20 @@ exprt verilog_lowering(exprt expr)
     else
       return expr;
   }
+  else if(expr.id() == ID_zero_extend)
+  {
+    auto &zero_extend = to_zero_extend_expr(expr);
+
+    if(
+      is_four_valued(zero_extend.type()) ||
+      is_four_valued(zero_extend.op().type()))
+    {
+      // encode into aval/bval
+      return aval_bval(zero_extend);
+    }
+    else
+      return expr; // leave as is
+  }
   else
     return expr; // leave as is