From 9a46e5455cc2c4968fc8df19bfaffb33d276bb7a Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Thu, 9 Oct 2025 12:58:24 -0700
Subject: [PATCH] SMV: conversion for extractbits operator

This adds conversion for the IR extractbits operator to SMV for the case
when the low index is an integer constant.
---
 regression/ebmc/smv-word-level/verilog4.desc |  7 +++
 regression/ebmc/smv-word-level/verilog4.sv   | 12 +++++
 src/smvlang/expr2smv.cpp                     | 49 ++++++++++++++++++++
 src/smvlang/expr2smv_class.h                 |  3 ++
 4 files changed, 71 insertions(+)
 create mode 100644 regression/ebmc/smv-word-level/verilog4.desc
 create mode 100644 regression/ebmc/smv-word-level/verilog4.sv

diff --git a/regression/ebmc/smv-word-level/verilog4.desc b/regression/ebmc/smv-word-level/verilog4.desc
new file mode 100644
index 000000000..ddac5c5e2
--- /dev/null
+++ b/regression/ebmc/smv-word-level/verilog4.desc
@@ -0,0 +1,7 @@
+CORE
+verilog4.sv
+--smv-word-level
+^LTLSPEC X X extend\(main\.x\[31:1\], 1\) = unsigned\(0sd32_1\)$
+^EXIT=0$
+^SIGNAL=0$
+--
diff --git a/regression/ebmc/smv-word-level/verilog4.sv b/regression/ebmc/smv-word-level/verilog4.sv
new file mode 100644
index 000000000..176e31af0
--- /dev/null
+++ b/regression/ebmc/smv-word-level/verilog4.sv
@@ -0,0 +1,12 @@
+module main(input clk);
+
+  reg [31:0] x;
+
+  initial x = 0;
+
+  always @(posedge clk)
+    x = x + 1;
+
+  initial assert property (nexttime[2] x[31:1] == 1);
+
+endmodule
diff --git a/src/smvlang/expr2smv.cpp b/src/smvlang/expr2smv.cpp
index 13aab16c9..6e3b66ed5 100644
--- a/src/smvlang/expr2smv.cpp
+++ b/src/smvlang/expr2smv.cpp
@@ -479,6 +479,52 @@ expr2smvt::convert_index(const index_exprt &src, precedencet precedence)
 
 /*******************************************************************\
 
+Function: expr2smvt::convert_extractbits
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2smvt::resultt expr2smvt::convert_extractbits(const extractbits_exprt &expr)
+{
+  const precedencet precedence = precedencet::INDEX;
+  auto op_rec = convert_rec(expr.src());
+
+  std::string dest;
+
+  if(precedence >= op_rec.p)
+    dest += '(';
+  dest += op_rec.s;
+  if(precedence >= op_rec.p)
+    dest += ')';
+
+  dest += '[';
+
+  // We can only do constant indices.
+  if(expr.index().is_constant())
+  {
+    auto index_int = numeric_cast_v<mp_integer>(to_constant_expr(expr.index()));
+    auto width = to_unsignedbv_type(expr.type()).get_width();
+    dest += integer2string(index_int + width - 1);
+    dest += ':';
+    dest += integer2string(index_int);
+  }
+  else
+  {
+    dest += "?:?";
+  }
+
+  dest += ']';
+
+  return {precedence, std::move(dest)};
+}
+
+/*******************************************************************\
+
 Function: expr2smvt::convert_if
 
   Inputs:
@@ -825,6 +871,9 @@ expr2smvt::resultt expr2smvt::convert_rec(const exprt &src)
     return convert_binary(to_binary_expr(src), ">>", precedencet::SHIFT);
   }
 
+  else if(src.id() == ID_extractbits)
+    return convert_extractbits(to_extractbits_expr(src));
+
   else if(src.id() == ID_smv_extend)
     return convert_function_application("extend", src);
 
diff --git a/src/smvlang/expr2smv_class.h b/src/smvlang/expr2smv_class.h
index caed6efde..49d735d50 100644
--- a/src/smvlang/expr2smv_class.h
+++ b/src/smvlang/expr2smv_class.h
@@ -10,6 +10,7 @@ Author: Daniel Kroening, dkr@amazon.com
 #define CPROVER_SMV_EXPR2SMV_CLASS_H
 
 #include <util/arith_tools.h>
+#include <util/bitvector_expr.h>
 #include <util/bitvector_types.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
@@ -111,6 +112,8 @@ class expr2smvt
   resultt
   convert_unary(const unary_exprt &, const std::string &symbol, precedencet);
 
+  resultt convert_extractbits(const extractbits_exprt &);
+
   resultt convert_index(const index_exprt &, precedencet);
 
   resultt convert_if(const if_exprt &, precedencet);