Verilog: fix semantics of relations

This replaces the custom code for type checking the operands of relations by
the code used for other binary expressions.  This fixes the downwards
type/size propagation.

Author: kroening

regression/verilog/assignments/assignment-with-function-call1.sv

@@ -10,8 +10,8 @@ module top(input [7:0] a, input [7:0] b);
   wire [7:0] sum_a_b = fn(a, b),
              sum_1_2 = fn(1, 2),
              sum_2_3 = fn(2, 3);
-  
-  assert property (sum_a_b==a[2:0]+b[2:0]);
+
+  assert property (sum_a_b[2:0]==a[2:0]+b[2:0]);
 
   assert property (sum_1_2==3);
 

regression/verilog/expressions/equality1.desc

@@ -10,7 +10,7 @@ equality1.v
 ^\[.*\] always 32'b0000000000000000000000000000000x != 10 === 32'b0000000000000000000000000000000x: PROVED .*$
 ^\[.*\] always 32'b0000000000000000000000000000000z != 20 === 32'b0000000000000000000000000000000x: PROVED .*$
 ^\[.*\] always 1'sb1 == 2'b11 === 0: PROVED .*$
-^\[.*\] always 2'sb11 == 2'sb11 === 1: PROVED .*$
+^\[.*\] always 1'sb1 == 2'sb11 === 1: PROVED .*$
 ^\[.*\] always 1\.1 == 1\.1 == 1: PROVED .*$
 ^\[.*\] always 1\.1 == 1 == 0: PROVED .*$
 ^EXIT=0$

regression/verilog/expressions/equality2.desc

@@ -12,7 +12,7 @@ equality2.v
 ^\[.*\] always 32'b0000000000000000000000000000000z === 1 == 0: PROVED .*$
 ^\[.*\] always 1 === 1 == 1: PROVED .*$
 ^\[.*\] always 3'b011 === 2'sb11 == 1: PROVED .*$
-^\[.*\] always 3'sb111 === 3'sb111 == 1: PROVED .*$
+^\[.*\] always 3'sb111 === 2'sb11 == 1: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/expressions/shl4.desc

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

regression/verilog/expressions/wildcard_equality1.desc

@@ -10,7 +10,7 @@ wildcard_equality1.sv
 ^\[main\.property07\] always 2'b00 !=\? 2'b0x === 0: PROVED .*$
 ^\[main\.property08\] always 2'b10 !=\? 2'b0x === 1: PROVED .*$
 ^\[main\.property09\] always 1'sb1 ==\? 2'b11 === 0: PROVED .*$
-^\[main\.property10\] always 2'sb11 ==\? 2'sb11 === 1: PROVED .*$
+^\[main\.property10\] always 1'sb1 ==\? 2'sb11 === 1: PROVED .*$
 ^EXIT=0$
 ^SIGNAL=0$
 --

src/verilog/verilog_typecheck_expr.cpp

@@ -2554,43 +2554,11 @@ Function: verilog_typecheck_exprt::convert_relation
 
 void verilog_typecheck_exprt::convert_relation(binary_exprt &expr)
 {
-  auto &lhs = expr.lhs();
-  auto &rhs = expr.rhs();
-
-  convert_expr(lhs);
-  convert_expr(rhs);
-
-  union_decay(lhs);
-  union_decay(rhs);
-
-  // Relations are special-cased in 1800-2017 11.8.2.
-  const typet new_type =
-    max_type(enum_decay(lhs.type()), enum_decay(rhs.type()));
-
-  if(new_type.is_nil())
-  {
-    throw errort().with_location(expr.source_location())
-      << "expected operands of compatible type but got:\n"
-      << "  " << to_string(lhs.type()) << '\n'
-      << "  " << to_string(rhs.type());
-  }
+  convert_expr(expr.lhs());
+  convert_expr(expr.rhs());
 
-  // If both operands are signed, both are sign-extended to the max width.
-  // Otherwise, both are zero-extended to the max width.
-  // In particular, signed operands are then _not_ sign extended,
-  // which a typecast would do.
-  if(new_type.id() == ID_verilog_unsignedbv || new_type.id() == ID_unsignedbv)
-  {
-    // zero extend both operands
-    lhs = zero_extend(lhs, new_type);
-    rhs = zero_extend(rhs, new_type);
-  }
-  else
-  {
-    // convert
-    implicit_typecast(lhs, new_type);
-    implicit_typecast(rhs, new_type);
-  }
+  // determine the max of the operand types and propagate it downwards
+  tc_binary_expr(expr);
 }
 
 /*******************************************************************\