From 56778dd2e37f68500aff963e25e7e42cddfd1efc Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Fri, 12 Jul 2024 17:06:18 -0700
Subject: [PATCH] Verilog logical (in)equality expression

The Verilog logical equality and inequality now have their own ID as they
return a four-valued result when applied to four-valued logic.

When applied to two-valued logic, the typechecker maps these to mathematical
equality.
---
 src/hw_cbmc_irep_ids.h                 |  2 ++
 src/verilog/parser.y                   |  4 +--
 src/verilog/verilog_typecheck_expr.cpp | 37 ++++++++++++++++++++++++++
 3 files changed, 41 insertions(+), 2 deletions(-)

diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index 6f506352c..55719ea1b 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/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)
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index 6ca367af8..e3a14df2e 100644
--- a/src/verilog/parser.y
+++ b/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
diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp
index dc8b30cf7..5e14cd46a 100644
--- a/src/verilog/verilog_typecheck_expr.cpp
+++ b/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)