Verilog: typechecking for relations

Relations are special-cased in 1800-2017 11.8.2.

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.

Author: kroening

regression/ebmc/example1/example1.sv

@@ -11,6 +11,6 @@ module main(input a, input b);
 
   my_add adder(a, b, result);
 
-  assert final (a+b==result);
+  assert final (2'(a)+b==result);
 
 endmodule

regression/verilog/SVA/immediate3.desc

@@ -1,7 +1,7 @@
 CORE
 immediate3.sv
 --bound 0
-^\[full_adder\.assert\.1\] always \{ full_adder\.carry, full_adder\.sum \} == full_adder\.a \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
+^\[full_adder\.assert\.1\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/immediate3.sv

@@ -4,6 +4,6 @@ module full_adder(input a, b, c, output sum, carry);
   assign carry = a & b | (a ^ b) & c;
 
   always @(*)
-    assert final({carry, sum} == a + b + c);
+    assert final({carry, sum} == {1'b0, a} + b + c);
 
 endmodule

regression/verilog/SVA/static_final1.desc

@@ -1,7 +1,7 @@
 CORE
 static_final1.sv
 --bound 0
-^\[full_adder\.p0\] always \{ full_adder\.carry, full_adder\.sum \} == full_adder\.a \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
+^\[full_adder\.p0\] always \{ full_adder\.carry, full_adder\.sum \} == \{ 1'b0, full_adder\.a \} \+ full_adder\.b \+ full_adder\.c: PROVED up to bound 0$
 ^EXIT=0$
 ^SIGNAL=0$
 --

regression/verilog/SVA/static_final1.sv

@@ -5,6 +5,6 @@ module full_adder(input a, b, c, output sum, carry);
 
   // 1800-2017
   // 16.4.3 Deferred assertions outside procedural code
-  p0: assert final ({carry, sum} == a + b + c);
+  p0: assert final ({carry, sum} == {1'b0, a} + b + c);
 
 endmodule

regression/verilog/expressions/concatenation1.v

@@ -7,7 +7,7 @@ module main(in1, in2);
   always @in1
     out = { in2, in1 };
 
-  always assert property1: out == ((in2<<16)|in1);
+  always assert property1: out == (({16'b0, in2}<<16)|in1);
 
   always assert property2: {4'b1001,4'b1011}==8'b10011011;
 

regression/verilog/expressions/equality1.desc

@@ -9,9 +9,9 @@ equality1.v
 ^\[.*\] always 32'b0000000000000000000000000000000z == 20 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$
 ^\[.*\] always 32'b0000000000000000000000000000000x != 10 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$
 ^\[.*\] always 32'b0000000000000000000000000000000z != 20 === 32'b0000000000000000000000000000000x: PROVED up to bound 0$
-^\[.*\] always 2'b11 == 2'b11 === 0: REFUTED$
+^\[.*\] always 1'sb1 == 2'b11 === 0: PROVED up to bound 0$
 ^\[.*\] always 2'sb11 == 2'sb11 === 1: PROVED up to bound 0$
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/verilog/expressions/equality2.desc

@@ -11,9 +11,9 @@ equality2.v
 ^\[.*\] always 32'b0000000000000000000000000000000x === 1 == 0: PROVED up to bound 0$
 ^\[.*\] always 32'b0000000000000000000000000000000z === 1 == 0: PROVED up to bound 0$
 ^\[.*\] always 1 === 1 == 1: PROVED up to bound 0$
-^\[.*\] always 3'b011 === 3'b111 == 1: REFUTED$
+^\[.*\] always 3'b011 === 2'sb11 == 1: PROVED up to bound 0$
 ^\[.*\] always 3'sb111 === 3'sb111 == 1: PROVED up to bound 0$
-^EXIT=10$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring

regression/verilog/expressions/replication1.v

@@ -7,7 +7,7 @@ module main(in);
     out = { 4 { in } };
 
   always assert property1:
-    out==(in | (in<<8) | (in<<16) | (in<<24));
+    out==({24'b0, in} | (in<<8) | (in<<16) | (in<<24));
 
   // 1-replication
   always assert property2:

src/verilog/verilog_typecheck_expr.cpp

@@ -2118,6 +2118,33 @@ void verilog_typecheck_exprt::convert_range(
 
 /*******************************************************************\
 
+Function: verilog_typecheck_exprt::enum_decay
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+typet verilog_typecheck_exprt::enum_decay(const typet &type)
+{
+  // Verilog enum types decay to their base type when used in relational
+  // or arithmetic expressions.
+  if(type.get(ID_C_verilog_type) == ID_verilog_enum)
+  {
+    typet result = type;
+    result.remove(ID_C_verilog_type);
+    result.remove(ID_C_identifier);
+    return result;
+  }
+  else
+    return type;
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::tc_binary_expr
 
   Inputs:
@@ -2132,20 +2159,7 @@ void verilog_typecheck_exprt::tc_binary_expr(
   const exprt &expr,
   exprt &op0, exprt &op1)
 {
-  // Verilog enum types decay to their base type when used in relational
-  // or arithmetic expressions.
-  auto enum_decay = [](const typet &type) {
-    if(type.get(ID_C_verilog_type) == ID_verilog_enum)
-    {
-      typet result = type;
-      result.remove(ID_C_verilog_type);
-      result.remove(ID_C_identifier);
-      return result;
-    }
-    else
-      return type;
-  };
-
+  // follows 1800-2017 11.8.2
   const typet new_type =
     max_type(enum_decay(op0.type()), enum_decay(op1.type()));
 
@@ -2163,6 +2177,84 @@ void verilog_typecheck_exprt::tc_binary_expr(
 
 /*******************************************************************\
 
+Function: zero_extend
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static exprt zero_extend(const exprt &expr, const typet &type)
+{
+  auto old_width = expr.type().id() == ID_bool ?
+    1 : to_bitvector_type(expr.type()).get_width();
+
+  // first make unsigned
+  typet tmp_type;
+
+  if(type.id() == ID_unsignedbv)
+    tmp_type = unsignedbv_typet{old_width};
+  else if(type.id() == ID_verilog_unsignedbv)
+    tmp_type = verilog_unsignedbv_typet{old_width};
+  else
+    PRECONDITION(false);
+
+  return typecast_exprt::conditional_cast(
+    typecast_exprt::conditional_cast(expr, tmp_type), type);
+}
+
+/*******************************************************************\
+
+Function: verilog_typecheck_exprt::typecheck_relation
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+void verilog_typecheck_exprt::typecheck_relation(binary_exprt &expr)
+{
+  auto &lhs = expr.lhs();
+  auto &rhs = expr.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());
+  }
+
+  // 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);
+  }
+}
+
+/*******************************************************************\
+
 Function: verilog_typecheck_exprt::max_type
 
   Inputs:
@@ -2561,7 +2653,7 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     Forall_operands(it, expr)
       convert_expr(*it);
 
-    tc_binary_expr(expr);
+    typecheck_relation(expr);
 
     return std::move(expr);
   }
@@ -2573,7 +2665,7 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     Forall_operands(it, expr)
       convert_expr(*it);
 
-    tc_binary_expr(expr);
+    typecheck_relation(expr);
 
     // This returns 'x' if either of the operands contains x or z.
     if(
@@ -2610,7 +2702,7 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     Forall_operands(it, expr)
       convert_expr(*it);
 
-    tc_binary_expr(expr);
+    typecheck_relation(expr);
 
     return std::move(expr);
   }
@@ -2622,7 +2714,7 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     Forall_operands(it, expr)
       convert_expr(*it);
 
-    tc_binary_expr(expr);
+    typecheck_relation(expr);
     no_bool_ops(expr);
 
     return std::move(expr);