From 5d4d6055457bbcf9c05fbf330317ed177d29a9d1 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 15 Jan 2025 16:12:48 -0800
Subject: [PATCH] aval/bval lowering for reduction operators

This adds the aval/bval encoding for four-valued reduction operators.
---
 .../verilog/expressions/reduction3.desc       |  8 +++
 regression/verilog/expressions/reduction3.sv  | 22 ++++++
 src/verilog/aval_bval_encoding.cpp            | 69 +++++++++++++++++++
 src/verilog/aval_bval_encoding.h              |  2 +
 src/verilog/verilog_lowering.cpp              | 11 +++
 5 files changed, 112 insertions(+)
 create mode 100644 regression/verilog/expressions/reduction3.desc
 create mode 100644 regression/verilog/expressions/reduction3.sv

diff --git a/regression/verilog/expressions/reduction3.desc b/regression/verilog/expressions/reduction3.desc
new file mode 100644
index 00000000..2a847105
--- /dev/null
+++ b/regression/verilog/expressions/reduction3.desc
@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+reduction3.sv
+
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/expressions/reduction3.sv b/regression/verilog/expressions/reduction3.sv
new file mode 100644
index 00000000..78989676
--- /dev/null
+++ b/regression/verilog/expressions/reduction3.sv
@@ -0,0 +1,22 @@
+module main;
+
+  assert final ( & 4'b1001 === 'b0);
+  assert final ( & 4'bx111 === 'bx);
+  assert final ( & 4'bz111 === 'bx);
+  assert final (~& 4'b1001 === 'b1);
+  assert final (~& 4'bx001 === 'b1);
+  assert final (~& 4'bz001 === 'b1);
+  assert final ( | 4'b1001 === 'b1);
+  assert final ( | 4'bx000 === 'bx);
+  assert final ( | 4'bz000 === 'bx);
+  assert final (~| 4'b1001 === 'b0);
+  assert final (~| 4'bx001 === 'b0);
+  assert final (~| 4'bz001 === 'b0);
+  assert final ( ^ 4'b1001 === 'b0);
+  assert final ( ^ 4'bx001 === 'bx);
+  assert final ( ^ 4'bz001 === 'bx);
+  assert final (~^ 4'b1001 === 'b1);
+  assert final (~^ 4'bx001 === 'bx);
+  assert final (~^ 4'bz001 === 'bx);
+
+endmodule
diff --git a/src/verilog/aval_bval_encoding.cpp b/src/verilog/aval_bval_encoding.cpp
index 3970d4f1..36ff72ab 100644
--- a/src/verilog/aval_bval_encoding.cpp
+++ b/src/verilog/aval_bval_encoding.cpp
@@ -337,6 +337,75 @@ exprt aval_bval(const not_exprt &expr)
   return if_exprt{has_xz, x, aval_bval_conversion(not_expr, x.type())};
 }
 
+exprt aval_bval_reduction(const unary_exprt &expr)
+{
+  auto &type = expr.type();
+  auto type_aval_bval = lower_to_aval_bval(type);
+  PRECONDITION(is_four_valued(type));
+  PRECONDITION(is_aval_bval(expr.op()));
+
+  auto has_xz = ::has_xz(expr.op());
+  auto x = make_x(type);
+  auto op_aval = aval(expr.op());
+  auto op_bval = bval(expr.op());
+
+  if(expr.id() == ID_reduction_xor || expr.id() == ID_reduction_xnor)
+  {
+    auto reduction_expr = unary_exprt{expr.id(), op_aval, bool_typet{}};
+    return if_exprt{has_xz, x, aval_bval_conversion(reduction_expr, x.type())};
+  }
+  else if(expr.id() == ID_reduction_and || expr.id() == ID_reduction_nand)
+  {
+    auto has_zero = notequal_exprt{
+      bitor_exprt{op_aval, op_bval},
+      to_bv_type(op_aval.type()).all_ones_expr()};
+
+    auto one = combine_aval_bval(
+      bv_typet{1}.all_ones_expr(),
+      bv_typet{1}.all_zeros_expr(),
+      type_aval_bval);
+    auto zero = combine_aval_bval(
+      bv_typet{1}.all_zeros_expr(),
+      bv_typet{1}.all_zeros_expr(),
+      type_aval_bval);
+
+    if(expr.id() == ID_reduction_and)
+    {
+      return if_exprt{has_zero, zero, if_exprt{has_xz, x, one}};
+    }
+    else // nand
+    {
+      return if_exprt{has_zero, one, if_exprt{has_xz, x, zero}};
+    }
+  }
+  else if(expr.id() == ID_reduction_or || expr.id() == ID_reduction_nor)
+  {
+    auto has_one = notequal_exprt{
+      bitand_exprt{op_aval, bitnot_exprt{op_bval}},
+      to_bv_type(op_aval.type()).all_zeros_expr()};
+
+    auto one = combine_aval_bval(
+      bv_typet{1}.all_ones_expr(),
+      bv_typet{1}.all_zeros_expr(),
+      type_aval_bval);
+    auto zero = combine_aval_bval(
+      bv_typet{1}.all_zeros_expr(),
+      bv_typet{1}.all_zeros_expr(),
+      type_aval_bval);
+
+    if(expr.id() == ID_reduction_or)
+    {
+      return if_exprt{has_one, one, if_exprt{has_xz, x, zero}};
+    }
+    else // nor
+    {
+      return if_exprt{has_one, zero, if_exprt{has_xz, x, one}};
+    }
+  }
+  else
+    PRECONDITION(false);
+}
+
 exprt aval_bval(const bitnot_exprt &expr)
 {
   auto &type = expr.type();
diff --git a/src/verilog/aval_bval_encoding.h b/src/verilog/aval_bval_encoding.h
index 3f8c873b..4e0eac51 100644
--- a/src/verilog/aval_bval_encoding.h
+++ b/src/verilog/aval_bval_encoding.h
@@ -51,6 +51,8 @@ exprt aval_bval(const not_exprt &);
 exprt aval_bval(const bitnot_exprt &);
 /// lowering for &, |, ^, ^~
 exprt aval_bval_bitwise(const multi_ary_exprt &);
+/// lowering for reduction operators
+exprt aval_bval_reduction(const unary_exprt &);
 /// lowering for ==?
 exprt aval_bval(const verilog_wildcard_equality_exprt &);
 /// lowering for !=?
diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp
index 0927f616..e290abee 100644
--- a/src/verilog/verilog_lowering.cpp
+++ b/src/verilog/verilog_lowering.cpp
@@ -525,6 +525,17 @@ exprt verilog_lowering(exprt expr)
     else
       return expr; // leave as is
   }
+  else if(
+    expr.id() == ID_reduction_or || expr.id() == ID_reduction_and ||
+    expr.id() == ID_reduction_nor || expr.id() == ID_reduction_nand ||
+    expr.id() == ID_reduction_xor || expr.id() == ID_reduction_xnor)
+  {
+    // encode into aval/bval
+    if(is_four_valued(expr.type()))
+      return aval_bval_reduction(to_unary_expr(expr));
+    else
+      return expr; // leave as is
+  }
   else if(expr.id() == ID_verilog_iff)
   {
     auto &iff = to_verilog_iff_expr(expr);