Merge pull request #787 from diffblue/part-select-constant

Verilog: constant folding for indexed part select expressions

Author: kroening

regression/verilog/expressions/part-select-constant1.sv

@@ -3,7 +3,9 @@ module main;
   // part-select expressions yield constants
   parameter p = 'b1010;
   parameter q = p[3:1];
+  parameter r = p[1 +: 3];
 
   assert final (q == 'b101);
+  assert final (r == 'b101);
 
 endmodule

src/verilog/verilog_expr.cpp

@@ -228,3 +228,80 @@ exprt verilog_non_indexed_part_select_exprt::lower() const
 {
   return ::lower(*this);
 }
+
+static exprt
+lower(const verilog_indexed_part_select_plus_or_minus_exprt &part_select)
+{
+  auto get_width = [](const typet &t) -> mp_integer
+  {
+    if(t.id() == ID_bool)
+      return 1;
+
+    if(
+      t.id() == ID_unsignedbv || t.id() == ID_signedbv ||
+      t.id() == ID_verilog_signedbv || t.id() == ID_verilog_unsignedbv)
+    {
+      return to_bitvector_type(t).get_width();
+    }
+
+    PRECONDITION(false);
+  };
+
+  PRECONDITION(
+    part_select.id() == ID_verilog_indexed_part_select_plus ||
+    part_select.id() == ID_verilog_indexed_part_select_minus);
+
+  const exprt &src = part_select.src();
+
+  mp_integer src_width = get_width(src.type());
+  mp_integer src_offset = string2integer(src.type().get_string(ID_C_offset));
+
+  // The width of the indexed part select must be an
+  // elaboration-time constant.
+  auto width =
+    numeric_cast_v<mp_integer>(to_constant_expr(part_select.width()));
+
+  // The index need not be a constant.
+  const exprt &index = part_select.index();
+
+  if(index.is_constant())
+  {
+    auto index_int = numeric_cast_v<mp_integer>(to_constant_expr(index));
+
+    // Construct the extractbits expression
+    mp_integer bottom;
+
+    if(part_select.id() == ID_verilog_indexed_part_select_plus)
+    {
+      bottom = index_int - src_offset;
+    }
+    else // ID_verilog_indexed_part_select_minus
+    {
+      bottom = bottom - width + 1;
+    }
+
+    return extractbits_exprt{
+      std::move(src), from_integer(bottom, integer_typet{}), part_select.type()}
+      .with_source_location(part_select);
+  }
+  else
+  {
+    // Index not constant.
+    // Use logical right-shift followed by (constant) extractbits.
+    auto index_adjusted =
+      minus_exprt{index, from_integer(src_offset, index.type())};
+
+    auto src_shifted = lshr_exprt(src, index_adjusted);
+
+    return extractbits_exprt{
+      std::move(src_shifted),
+      from_integer(0, integer_typet{}),
+      part_select.type()}
+      .with_source_location(part_select);
+  }
+}
+
+exprt verilog_indexed_part_select_plus_or_minus_exprt::lower() const
+{
+  return ::lower(*this);
+}

src/verilog/verilog_expr.h

@@ -2417,6 +2417,8 @@ class verilog_indexed_part_select_plus_or_minus_exprt : public ternary_exprt
   {
     return op2();
   }
+
+  exprt lower() const;
 };
 
 inline const verilog_indexed_part_select_plus_or_minus_exprt &

src/verilog/verilog_synthesis.cpp

@@ -358,54 +358,7 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
     expr.id() == ID_verilog_indexed_part_select_minus)
   {
     auto &part_select = to_verilog_indexed_part_select_plus_or_minus_expr(expr);
-    exprt &src = part_select.src();
-
-    mp_integer src_width = get_width(src.type());
-    mp_integer src_offset = string2integer(src.type().get_string(ID_C_offset));
-
-    // The width of the indexed part select must be an
-    // elaboration-time constant.
-    auto width =
-      numeric_cast_v<mp_integer>(to_constant_expr(part_select.width()));
-
-    // The index need not be a constant.
-    exprt &index = part_select.index();
-
-    if(index.is_constant())
-    {
-      auto index_int = numeric_cast_v<mp_integer>(to_constant_expr(index));
-
-      // Construct the extractbits expression
-      mp_integer bottom, top;
-
-      if(part_select.id() == ID_verilog_indexed_part_select_plus)
-      {
-        bottom = index_int - src_offset;
-        top = bottom + width - 1;
-      }
-      else // ID_verilog_indexed_part_select_minus
-      {
-        top = index_int - src_offset;
-        bottom = bottom - width + 1;
-      }
-
-      return extractbits_exprt{
-        std::move(src), from_integer(bottom, integer_typet{}), expr.type()}
-        .with_source_location(expr);
-    }
-    else
-    {
-      // Index not constant.
-      // Use logical right-shift followed by (constant) extractbits.
-      auto index_adjusted =
-        minus_exprt{index, from_integer(src_offset, index.type())};
-
-      auto src_shifted = lshr_exprt(src, index_adjusted);
-
-      return extractbits_exprt{
-        std::move(src_shifted), from_integer(0, integer_typet{}), expr.type()}
-        .with_source_location(expr);
-    }
+    return part_select.lower();
   }
   else if(expr.id() == ID_verilog_logical_equality)
   {

src/verilog/verilog_typecheck_expr.cpp

@@ -1660,6 +1660,15 @@ exprt verilog_typecheck_exprt::elaborate_constant_expression(exprt expr)
       auto &part_select = to_verilog_non_indexed_part_select_expr(expr);
       expr = part_select.lower();
     }
+    else if(
+      expr.id() == ID_verilog_indexed_part_select_plus ||
+      expr.id() == ID_verilog_indexed_part_select_minus)
+    {
+      // Our simplifier does not know these, do lowering.
+      auto &part_select =
+        to_verilog_indexed_part_select_plus_or_minus_expr(expr);
+      expr = part_select.lower();
+    }
     else if(expr.id() == ID_reduction_or)
     {
       // The simplifier doesn't know how to simplify reduction_or