Merge pull request #593 from diffblue/verilog_equality

Verilog logical (in)equality expression

Author: kroening

src/hw_cbmc_irep_ids.h

@@ -51,6 +51,8 @@ IREP_ID_ONE(ports)
 IREP_ID_ONE(inst)
 IREP_ID_ONE(Verilog)
 IREP_ID_ONE(verilog_assignment_pattern)
+IREP_ID_ONE(verilog_logical_equality)
+IREP_ID_ONE(verilog_logical_inequality)
 IREP_ID_ONE(verilog_explicit_cast)
 IREP_ID_ONE(verilog_size_cast)
 IREP_ID_ONE(verilog_implicit_typecast)

src/verilog/parser.y

@@ -3541,9 +3541,9 @@ expression:
 	| expression TOK_PERCENT expression
 		{ init($$, ID_mod); mto($$, $1); mto($$, $3); }
 	| expression TOK_EQUALEQUAL expression
-		{ init($$, ID_equal); mto($$, $1); mto($$, $3); }
+		{ init($$, ID_verilog_logical_equality); mto($$, $1); mto($$, $3); }
 	| expression TOK_EXCLAMEQUAL expression
-		{ init($$, ID_notequal); mto($$, $1); mto($$, $3); }
+		{ init($$, ID_verilog_logical_inequality); mto($$, $1); mto($$, $3); }
 	| expression TOK_EQUALEQUALEQUAL expression
 		{ init($$, ID_verilog_case_equality); mto($$, $1); mto($$, $3); }
 	| expression TOK_EXCLAMEQUALEQUAL expression

src/verilog/verilog_typecheck_expr.cpp

@@ -2404,9 +2404,46 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
 
     return std::move(expr);
   }
+  else if(
+    expr.id() == ID_verilog_logical_equality ||
+    expr.id() == ID_verilog_logical_inequality)
+  {
+    // == and !=
+    Forall_operands(it, expr)
+      convert_expr(*it);
+
+    tc_binary_expr(expr);
+
+    // This returns 'x' if either of the operands contains x or z.
+    if(
+      expr.lhs().type().id() == ID_verilog_signedbv ||
+      expr.lhs().type().id() == ID_verilog_unsignedbv ||
+      expr.rhs().type().id() == ID_verilog_signedbv ||
+      expr.rhs().type().id() == ID_verilog_unsignedbv)
+    {
+      // Four-valued case. The ID stays
+      // ID_verilog_logical_equality or
+      // ID_verilog_logical_inequality.
+      expr.type() = verilog_unsignedbv_typet(1);
+    }
+    else
+    {
+      // On two-valued logic, it's the same as proper equality.
+      expr.type() = bool_typet();
+      if(expr.id() == ID_verilog_logical_equality)
+        expr.id(ID_equal);
+      else
+        expr.id(ID_notequal);
+    }
+
+    return std::move(expr);
+  }
   else if(expr.id()==ID_verilog_case_equality ||
           expr.id()==ID_verilog_case_inequality)
   {
+    // === and !==
+    // The result is always Boolean, and semantically
+    // a proper equality is performed.
     expr.type()=bool_typet();
 
     Forall_operands(it, expr)