Verilog: fix upper bound when printing extractbits expressions

The Verilog part-select rendered for an extractbits expression selects
the bits from index to index + width - 1, but the printer emitted
index + width as the upper bound. E.g., bits 4 to 7 of a vector were
printed as a[8:4] instead of a[7:4].

Author: kroening

src/verilog/expr2verilog.cpp

@@ -1122,13 +1122,13 @@ expr2verilogt::resultt expr2verilogt::convert_extractbits(
   if(src.index().is_constant())
   {
     auto index_int = numeric_cast_v<mp_integer>(to_constant_expr(src.index()));
-    dest += integer2string(index_int + width);
+    dest += integer2string(index_int + width - 1);
   }
   else
   {
     dest += convert_rec(src.index()).s;
     dest += " + ";
-    dest += std::to_string(width);
+    dest += std::to_string(width - 1);
   }
 
   dest+=':';

unit/Makefile

@@ -18,6 +18,7 @@ SRC += ebmc/bdd_model_checker.cpp \
        trans-netlist/aig.cpp \
        trans-netlist/id2smv.cpp \
        verilog/convert_literals.cpp \
+       verilog/expr2verilog.cpp \
        verilog/indexed_part_select.cpp \
        verilog/typename.cpp \
        verilog/verilog_expr.cpp \

unit/verilog/expr2verilog.cpp

@@ -0,0 +1,49 @@
+/*******************************************************************\
+
+Module: expr2verilog Unit Tests
+
+Author: Daniel Kroening, kroening@kroening.com
+
+\*******************************************************************/
+
+#include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
+#include <util/bitvector_types.h>
+#include <util/mathematical_types.h>
+#include <util/namespace.h>
+#include <util/symbol_table.h>
+
+#include <testing-utils/use_catch.h>
+#include <verilog/expr2verilog.h>
+
+SCENARIO("Output of extractbits expressions")
+{
+  symbol_tablet symbol_table;
+  namespacet ns{symbol_table};
+
+  GIVEN("an extractbits expression with constant index")
+  {
+    // bits 4 to 7 of a
+    auto src = symbol_exprt{"a", unsignedbv_typet{32}};
+    auto extractbits = extractbits_exprt{
+      src, from_integer(4, integer_typet{}), unsignedbv_typet{4}};
+
+    THEN("the part select has upper bound index + width - 1")
+    {
+      REQUIRE(expr2verilog(extractbits, ns) == "a[7:4]");
+    }
+  }
+
+  GIVEN("an extractbits expression with non-constant index")
+  {
+    // bits i to i + 3 of a
+    auto src = symbol_exprt{"a", unsignedbv_typet{32}};
+    auto index = symbol_exprt{"i", integer_typet{}};
+    auto extractbits = extractbits_exprt{src, index, unsignedbv_typet{4}};
+
+    THEN("the part select has upper bound index + width - 1")
+    {
+      REQUIRE(expr2verilog(extractbits, ns) == "a[i + 3:i]");
+    }
+  }
+}