From 8861599829dae552720fee71d7c4854ff3db3c36 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 16 Sep 2024 12:03:56 -0700
Subject: [PATCH] Verilog: synthesis for power expressions with constant rhs

The Verilog synthesis now lowers power expressions with constant rhs to the
equivalent multiplication.
---
 regression/verilog/expressions/power2.desc |  8 +++++++
 regression/verilog/expressions/power2.sv   |  9 ++++++++
 src/verilog/verilog_synthesis.cpp          | 25 ++++++++++++++++++++++
 3 files changed, 42 insertions(+)
 create mode 100644 regression/verilog/expressions/power2.desc
 create mode 100644 regression/verilog/expressions/power2.sv

diff --git a/regression/verilog/expressions/power2.desc b/regression/verilog/expressions/power2.desc
new file mode 100644
index 000000000..f17da1400
--- /dev/null
+++ b/regression/verilog/expressions/power2.desc
@@ -0,0 +1,8 @@
+CORE
+power2.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/expressions/power2.sv b/regression/verilog/expressions/power2.sv
new file mode 100644
index 000000000..0e2b3931c
--- /dev/null
+++ b/regression/verilog/expressions/power2.sv
@@ -0,0 +1,9 @@
+module main;
+
+  // powers with constant rhs
+  property1: assert final (3**0==1);
+  property2: assert final (3**1==3);
+  property3: assert final ((-3)**1==-3);
+  property4: assert final (3**3==27);
+
+endmodule
diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp
index 2b997afd1..a27b93175 100644
--- a/src/verilog/verilog_synthesis.cpp
+++ b/src/verilog/verilog_synthesis.cpp
@@ -244,6 +244,31 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
       symbol_state);
     return expr;
   }
+  else if(expr.id() == ID_power)
+  {
+    auto &power_expr = to_binary_expr(expr);
+    DATA_INVARIANT(
+      power_expr.lhs().type() == power_expr.type(),
+      "power expression type consistency");
+    power_expr.lhs() = synth_expr(power_expr.lhs(), symbol_state);
+    power_expr.rhs() = synth_expr(power_expr.rhs(), symbol_state);
+    auto rhs_int = numeric_cast<std::size_t>(power_expr.rhs());
+    if(rhs_int.has_value())
+    {
+      if(*rhs_int == 0)
+        return from_integer(1, expr.type());
+      else if(*rhs_int == 1)
+        return power_expr.lhs();
+      else // >= 2
+      {
+        auto factors = exprt::operandst{rhs_int.value(), power_expr.lhs()};
+        // would prefer appropriate mult_exprt constructor
+        return multi_ary_exprt{ID_mult, factors, expr.type()};
+      }
+    }
+    else
+      return expr;
+  }
   else if(expr.id()==ID_typecast)
   {
     {