Verilog: four-valued <=, <, >=, >

This adds the aval/bval lowering for the relational operators.

Author: kroening

regression/verilog/asic-world-operators/relational.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 relational.sv
 --module main --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-x-related tests fail

src/verilog/aval_bval_encoding.cpp

@@ -610,6 +610,23 @@ exprt aval_bval(const shift_exprt &expr)
   return if_exprt{distance_has_xz, x, combined};
 }
 
+exprt aval_bval(const binary_relation_exprt &expr)
+{
+  auto &type = expr.type();
+
+  PRECONDITION(type.id() == ID_verilog_unsignedbv);
+
+  auto has_xz = or_exprt{::has_xz(expr.lhs()), ::has_xz(expr.rhs())};
+
+  exprt two_valued_expr = binary_predicate_exprt{
+    aval_underlying(expr.lhs()), expr.id(), aval_underlying(expr.rhs())};
+
+  return if_exprt{
+    has_xz,
+    make_x(type),
+    aval_bval_conversion(two_valued_expr, lower_to_aval_bval(type))};
+}
+
 exprt default_aval_bval_lowering(const exprt &expr)
 {
   auto &type = expr.type();

src/verilog/aval_bval_encoding.h

@@ -69,6 +69,8 @@ exprt aval_bval(const verilog_implies_exprt &);
 exprt aval_bval(const typecast_exprt &);
 /// lowering for shifts
 exprt aval_bval(const shift_exprt &);
+/// lowering for <=, <, etc.
+exprt aval_bval(const binary_relation_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

@@ -421,6 +421,17 @@ exprt verilog_lowering(exprt expr)
     else
       return expr;
   }
+  else if(
+    expr.id() == ID_le || expr.id() == ID_ge || expr.id() == ID_lt ||
+    expr.id() == ID_ge)
+  {
+    if(is_four_valued(expr))
+    {
+      return aval_bval(to_binary_relation_expr(expr));
+    }
+    else
+      return expr;
+  }
   else if(expr.id() == ID_concatenation)
   {
     if(

src/verilog/verilog_typecheck_expr.cpp

@@ -3203,11 +3203,19 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
   else if(expr.id()==ID_lt || expr.id()==ID_gt ||
           expr.id()==ID_le || expr.id()==ID_ge)
   {
-    expr.type()=bool_typet();
-
     convert_relation(expr);
     no_bool_ops(expr);
 
+    // This returns 'x' if either of the operands contains x or z.
+    if(is_four_valued(expr.lhs().type()) || is_four_valued(expr.rhs().type()))
+    {
+      expr.type() = verilog_unsignedbv_typet(1);
+    }
+    else
+    {
+      expr.type() = bool_typet{};
+    }
+
     return std::move(expr);
   }
   else if(expr.id() == ID_power)