Merge pull request #629 from diffblue/reduction1

Verilog: constant folding for reduction operators

Author: kroening

regression/verilog/expressions/reduction1.desc

@@ -0,0 +1,7 @@
+CORE broken-smt-backend
+reduction1.v
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/verilog/expressions/reduction1.v

@@ -0,0 +1,52 @@
+module main(input [31:0] in);
+
+  // reduction and
+  always assert reduction_and1:
+    &3'b111 == 1 && &3'b101 == 0;
+
+  // constant folding
+  wire [&3'b111:0] wire_and;
+
+  // reduction nand
+  always assert reduction_nand1:
+    ~&in == !(&in);
+
+  // constant folding
+  wire [~&3'b111:0] wire_nand;
+
+  // reduction or
+  always assert reduction_or1:
+    |3'b000 == 0 && |3'b101 == 1;
+
+  // constant folding
+  wire [|3'b101:0] wire_or;
+
+  // reduction nor
+  always assert reduction_nor1:
+    ~|in == !(|in);
+
+  // constant folding
+  wire [~|3'b000:0] wire_nor;
+
+  // reduction xor
+  always assert reduction_xor1:
+    ^3'b000 == 0 && ^3'b111 == 1;
+
+  // constant folding
+  wire [^3'b111:0] wire_xor;
+
+  // reduction xnor, variant 1
+  always assert reduction_xnor1:
+    ~^in == !(^in);
+
+  // constant folding
+  wire [~^3'b000:0] wire_xnor1;
+
+  // reduction xnor, variant 2
+  always assert reduction_xnor2:
+    ^~in == !(^in);
+
+  // constant folding
+  wire [^~3'b000:0] wire_xnor2;
+
+endmodule

src/verilog/verilog_typecheck_expr.cpp

@@ -1545,13 +1545,68 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression(exprt expr)
     if(!operands_are_constant)
       return expr; // give up
 
+    auto make_all_ones = [](const typet &type) -> exprt
+    {
+      if(type.id() == ID_unsignedbv)
+      {
+        return from_integer(
+          power(2, to_unsignedbv_type(type).get_width()) - 1, type);
+      }
+      else if(type.id() == ID_signedbv)
+      {
+        return from_integer(-1, type);
+      }
+      else if(type.id() == ID_bool)
+        return true_exprt{};
+      else
+        PRECONDITION(false);
+    };
+
     if(expr.id() == ID_reduction_or)
     {
       // The simplifier doesn't know how to simplify reduction_or
       auto &reduction_or = to_unary_expr(expr);
       expr = notequal_exprt(
         reduction_or.op(), from_integer(0, reduction_or.op().type()));
     }
+    else if(expr.id() == ID_reduction_nor)
+    {
+      // The simplifier doesn't know how to simplify reduction_nor
+      auto &reduction_nor = to_unary_expr(expr);
+      expr = equal_exprt(
+        reduction_nor.op(), from_integer(0, reduction_nor.op().type()));
+    }
+    else if(expr.id() == ID_reduction_and)
+    {
+      // The simplifier doesn't know how to simplify reduction_and
+      auto &reduction_and = to_unary_expr(expr);
+      expr = equal_exprt{
+        reduction_and.op(), make_all_ones(reduction_and.op().type())};
+    }
+    else if(expr.id() == ID_reduction_nand)
+    {
+      // The simplifier doesn't know how to simplify reduction_nand
+      auto &reduction_nand = to_unary_expr(expr);
+      expr = notequal_exprt{
+        reduction_nand.op(), make_all_ones(reduction_nand.op().type())};
+    }
+    else if(expr.id() == ID_reduction_xor)
+    {
+      // The simplifier doesn't know how to simplify reduction_xor
+      // Lower to countones.
+      auto &reduction_xor = to_unary_expr(expr);
+      auto ones = countones(to_constant_expr(reduction_xor.op()));
+      expr = extractbit_exprt{ones, from_integer(0, natural_typet{})};
+    }
+    else if(expr.id() == ID_reduction_xnor)
+    {
+      // The simplifier doesn't know how to simplify reduction_xnor
+      // Lower to countones.
+      auto &reduction_xnor = to_unary_expr(expr);
+      auto ones = countones(to_constant_expr(reduction_xnor.op()));
+      expr =
+        not_exprt{extractbit_exprt{ones, from_integer(0, natural_typet{})}};
+    }
     else if(expr.id() == ID_replication)
     {
       auto &replication = to_replication_expr(expr);