aval/bval lowering for Verilog logical equality

== and != return 'x' when either operand contains x or z.  This lowers the
operator to the aval/bval encoding.

Author: kroening

regression/verilog/expressions/equality1.desc

@@ -1,9 +1,18 @@
-KNOWNBUG
+CORE
 equality1.v
 --bound 0
-^EXIT=0$
+^\[.*\] always 10 == 10 === 1: PROVED up to bound 0$
+^\[.*\] always 10 == 20 === 0: PROVED up to bound 0$
+^\[.*\] always 10 != 20 === 1: PROVED up to bound 0$
+^\[.*\] always 10 == 20 === 0: PROVED up to bound 0$
+^\[.*\] always 1'bx == 10 === 1'bx: PROVED up to bound 0$
+^\[.*\] always 1'bz == 20 === 1'bx: PROVED up to bound 0$
+^\[.*\] always 1'bx != 10 === 1'bx: PROVED up to bound 0$
+^\[.*\] always 1'bz != 20 === 1'bx: PROVED up to bound 0$
+^\[.*\] always 2'b11 == 2'b11 === 0: REFUTED$
+^\[.*\] always 2'sb-1 == 2'sb-1 === 1: PROVED up to bound 0$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-Missing Verilog case equality implementation.

regression/verilog/expressions/equality1.v

@@ -8,7 +8,7 @@ module main;
   always assert property06: ('bz==20)==='bx;
   always assert property07: ('bx!=10)==='bx;
   always assert property08: ('bz!=20)==='bx;
-  always assert property09: ('sb1=='b11)===0; // zero extension
-  always assert property10: ('sb1=='sb11)===1; // sign extension
+  always assert property09: (1'sb1==2'b11)===0; // zero extension
+  always assert property10: (1'sb1==2'sb11)===1; // sign extension
 
 endmodule

regression/verilog/expressions/equality2.desc

@@ -1,9 +1,20 @@
 CORE broken-smt-backend
 equality2.v
 --bound 0
-^EXIT=0$
+^\[.*\] always 10 === 10 == 1: PROVED up to bound 0$
+^\[.*\] always 10 === 20 == 0: PROVED up to bound 0$
+^\[.*\] always 10 !== 10 == 0: PROVED up to bound 0$
+^\[.*\] always 10 !== 20 == 1: PROVED up to bound 0$
+^\[.*\] always 1'bx === 1'bx == 1: PROVED up to bound 0$
+^\[.*\] always 1'bz === 1'bz == 1: PROVED up to bound 0$
+^\[.*\] always 1'bx === 1'bz == 0: PROVED up to bound 0$
+^\[.*\] always 1'bx === 1 == 0: PROVED up to bound 0$
+^\[.*\] always 1'bz === 1 == 0: PROVED up to bound 0$
+^\[.*\] always 1 === 1 == 1: PROVED up to bound 0$
+^\[.*\] always 3'b11 === 3'b111 == 1: REFUTED$
+^\[.*\] always 3'sb-1 === 3'sb-1 == 1: PROVED up to bound 0$
+^EXIT=10$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-Missing Verilog case equality implementation.

regression/verilog/expressions/equality2.v

@@ -10,7 +10,7 @@ module main;
   always assert property08: ('bx==='b1)==0;
   always assert property09: ('bz==='b1)==0;
   always assert property10: ('b1==='b01)==1; // zero extension
-  always assert property11: ('b011==='sb11)==1; // zero extension
-  always assert property12: ('sb011==='sb11)==1; // sign extension
+  always assert property11: (3'b011===2'sb11)==1; // zero extension
+  always assert property12: (3'sb111===2'sb11)==1; // sign extension
 
 endmodule

src/verilog/aval_bval_encoding.cpp

@@ -14,6 +14,8 @@ Author: Daniel Kroening, [email protected]
 #include <util/mathematical_types.h>
 #include <util/std_expr.h>
 
+#include "verilog_types.h"
+
 bv_typet aval_bval_type(std::size_t width, irep_idt source_type)
 {
   PRECONDITION(!source_type.empty());
@@ -34,12 +36,22 @@ bool is_aval_bval(const typet &type)
   return type.id() == ID_bv && !type.get(ID_C_verilog_aval_bval).empty();
 }
 
+bool is_aval_bval(const exprt &expr)
+{
+  return is_aval_bval(expr.type());
+}
+
 std::size_t aval_bval_width(const typet &type)
 {
   PRECONDITION(is_aval_bval(type));
   return to_bv_type(type).get_width() / 2;
 }
 
+std::size_t aval_bval_width(const exprt &expr)
+{
+  return aval_bval_width(expr.type());
+}
+
 typet aval_bval_underlying(const typet &src)
 {
   auto id = src.get(ID_C_verilog_aval_bval);
@@ -198,3 +210,41 @@ exprt aval_bval_concatenation(
 
   return combine_aval_bval(concatenate(new_aval), concatenate(new_bval), type);
 }
+
+/// return true iff 'expr' contains either x or z
+exprt has_xz(const exprt &expr)
+{
+  PRECONDITION(is_aval_bval(expr));
+  auto width = aval_bval_width(expr);
+  return notequal_exprt{bval(expr), bv_typet{width}.all_zeros_expr()};
+}
+
+/// return 'x', one bit
+exprt make_x()
+{
+  auto type = verilog_unsignedbv_typet{1};
+  return lower_to_aval_bval(constant_exprt{"x", type});
+}
+
+exprt aval_bval(const verilog_logical_equality_exprt &expr)
+{
+  auto &type = expr.type();
+  PRECONDITION(type.id() == ID_verilog_unsignedbv);
+  // returns 'x' if either operand contains x or z
+  auto has_xz = or_exprt{::has_xz(expr.lhs()), ::has_xz(expr.rhs())};
+  auto equality = equal_exprt{expr.lhs(), expr.rhs()};
+  return if_exprt{
+    has_xz, make_x(), aval_bval_conversion(equality, lower_to_aval_bval(type))};
+}
+
+exprt aval_bval(const verilog_logical_inequality_exprt &expr)
+{
+  auto &type = expr.type();
+  PRECONDITION(type.id() == ID_verilog_unsignedbv);
+  // returns 'x' if either operand contains x or z
+  auto has_xz = or_exprt{::has_xz(expr.lhs()), ::has_xz(expr.rhs())};
+  auto x = lower_to_aval_bval(constant_exprt{"x", type});
+  auto equality = notequal_exprt{expr.lhs(), expr.rhs()};
+  return if_exprt{
+    has_xz, x, aval_bval_conversion(equality, lower_to_aval_bval(type))};
+}

src/verilog/aval_bval_encoding.h

@@ -10,7 +10,8 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_VERILOG_AVAL_BVAL_H
 
 #include <util/bitvector_types.h>
-#include <util/std_expr.h>
+
+#include "verilog_expr.h"
 
 // bit-concoding for four-valued types
 //
@@ -36,4 +37,7 @@ exprt aval_bval_conversion(const exprt &, const typet &);
 
 exprt aval_bval_concatenation(const exprt::operandst &, const typet &);
 
+exprt aval_bval(const verilog_logical_equality_exprt &);
+exprt aval_bval(const verilog_logical_inequality_exprt &);
+
 #endif

src/verilog/expr2verilog.cpp

@@ -1222,10 +1222,18 @@ expr2verilogt::convert(const exprt &src, verilog_precedencet &precedence)
     return convert_binary(
       to_multi_ary_expr(src), "==", precedence = verilog_precedencet::EQUALITY);
 
+  else if(src.id() == ID_verilog_logical_equality)
+    return convert_binary(
+      to_multi_ary_expr(src), "==", precedence = verilog_precedencet::EQUALITY);
+
   else if(src.id()==ID_notequal)
     return convert_binary(
       to_multi_ary_expr(src), "!=", precedence = verilog_precedencet::EQUALITY);
 
+  else if(src.id() == ID_verilog_logical_inequality)
+    return convert_binary(
+      to_multi_ary_expr(src), "!=", precedence = verilog_precedencet::EQUALITY);
+
   else if(src.id()==ID_verilog_case_equality)
     return convert_binary(
       to_multi_ary_expr(src),

src/verilog/verilog_expr.h

@@ -62,6 +62,52 @@ to_hierarchical_identifier_expr(exprt &expr)
   return static_cast<hierarchical_identifier_exprt &>(expr);
 }
 
+/// ==
+/// returns 'x' if either operand contains x or z
+class verilog_logical_equality_exprt : public equal_exprt
+{
+public:
+};
+
+inline const verilog_logical_equality_exprt &
+to_verilog_logical_equality_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_logical_equality);
+  binary_exprt::check(expr);
+  return static_cast<const verilog_logical_equality_exprt &>(expr);
+}
+
+inline verilog_logical_equality_exprt &
+to_verilog_logical_equality_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_logical_equality);
+  binary_exprt::check(expr);
+  return static_cast<verilog_logical_equality_exprt &>(expr);
+}
+
+/// !=
+/// returns 'x' if either operand contains x or z
+class verilog_logical_inequality_exprt : public equal_exprt
+{
+public:
+};
+
+inline const verilog_logical_inequality_exprt &
+to_verilog_logical_inequality_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_logical_inequality);
+  binary_exprt::check(expr);
+  return static_cast<const verilog_logical_inequality_exprt &>(expr);
+}
+
+inline verilog_logical_inequality_exprt &
+to_verilog_logical_inequality_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_verilog_logical_inequality);
+  binary_exprt::check(expr);
+  return static_cast<verilog_logical_inequality_exprt &>(expr);
+}
+
 class function_call_exprt : public binary_exprt
 {
 public:

src/verilog/verilog_synthesis.cpp

@@ -390,6 +390,18 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
         .with_source_location(expr);
     }
   }
+  else if(expr.id() == ID_verilog_logical_equality)
+  {
+    for(auto &op : expr.operands())
+      op = synth_expr(op, symbol_state);
+    return aval_bval(to_verilog_logical_equality_expr(expr));
+  }
+  else if(expr.id() == ID_verilog_logical_inequality)
+  {
+    for(auto &op : expr.operands())
+      op = synth_expr(op, symbol_state);
+    return aval_bval(to_verilog_logical_inequality_expr(expr));
+  }
   else if(expr.has_operands())
   {
     for(auto &op : expr.operands())