Verilog: synthesis for power expressions with constant rhs

The Verilog synthesis now lowers power expressions with constant rhs to the
equivalent multiplication.

Author: kroening

regression/verilog/expressions/power2.desc

@@ -0,0 +1,8 @@
+CORE
+power2.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

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

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)
   {
     {