From 11a386fb2714f9c75568abc82f983a010166a947 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Tue, 28 Oct 2025 13:50:31 -0700
Subject: [PATCH] Verilog: aval/bval lowering for replication operator

This adds the aval/bval lowering for the replication operator.
---
 .../asic-world-operators/replication.desc     |  3 +--
 .../asic-world-operators/replication.sv       |  4 ++--
 src/verilog/aval_bval_encoding.cpp            | 24 +++++++++++++++++++
 src/verilog/aval_bval_encoding.h              |  2 ++
 src/verilog/verilog_lowering.cpp              | 10 ++++++++
 5 files changed, 39 insertions(+), 4 deletions(-)

diff --git a/regression/verilog/asic-world-operators/replication.desc b/regression/verilog/asic-world-operators/replication.desc
index 2f49cfc20..a38016a72 100644
--- a/regression/verilog/asic-world-operators/replication.desc
+++ b/regression/verilog/asic-world-operators/replication.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 replication.sv
 --module main --bound 0
 ^EXIT=0$
@@ -6,4 +6,3 @@ replication.sv
 --
 ^warning: ignoring
 --
-z-related tests fail
diff --git a/regression/verilog/asic-world-operators/replication.sv b/regression/verilog/asic-world-operators/replication.sv
index fb580eced..7d3d36809 100644
--- a/regression/verilog/asic-world-operators/replication.sv
+++ b/regression/verilog/asic-world-operators/replication.sv
@@ -4,7 +4,7 @@ module main(input[31:0] in1, in2, in3);
   // http://www.asic-world.com/verilog/operators2.html
 
   // replication
-  always assert repli_p1: {4{4'b1001}}      == 'b1001100110011001;
-  always assert repli_p2: {4{4'b1001,1'bz}} == 'b1001z1001z1001z1001z;
+  initial repli_p1: assert({4{4'b1001}}      === 'b1001100110011001);
+  initial repli_p2: assert({4{4'b1001,1'bz}} === 'b1001z1001z1001z1001z);
 
 endmodule
diff --git a/src/verilog/aval_bval_encoding.cpp b/src/verilog/aval_bval_encoding.cpp
index 69b03b4d2..d7e3a91b8 100644
--- a/src/verilog/aval_bval_encoding.cpp
+++ b/src/verilog/aval_bval_encoding.cpp
@@ -483,6 +483,30 @@ exprt aval_bval_bitwise(const multi_ary_exprt &expr)
   return combine_aval_bval(aval, bval, lower_to_aval_bval(expr.type()));
 }
 
+exprt aval_bval_replication(const replication_exprt &expr)
+{
+  auto &type = expr.type();
+  PRECONDITION(is_four_valued(type));
+  PRECONDITION(!is_four_valued(expr.times()));
+
+  auto times_int = numeric_cast_v<mp_integer>(expr.times());
+
+  // separately replicate aval and bval
+  auto op_aval = aval(expr.op());
+  auto op_bval = bval(expr.op());
+
+  auto replication_type = bv_typet{numeric_cast_v<std::size_t>(
+    to_bitvector_type(op_aval.type()).width() * times_int)};
+
+  auto aval_replicated =
+    replication_exprt{expr.times(), op_aval, replication_type};
+  auto bval_replicated =
+    replication_exprt{expr.times(), op_bval, replication_type};
+
+  return combine_aval_bval(
+    aval_replicated, bval_replicated, lower_to_aval_bval(type));
+}
+
 exprt aval_bval(const power_exprt &expr)
 {
   PRECONDITION(is_four_valued(expr.type()));
diff --git a/src/verilog/aval_bval_encoding.h b/src/verilog/aval_bval_encoding.h
index cb0c179d9..75ef6794c 100644
--- a/src/verilog/aval_bval_encoding.h
+++ b/src/verilog/aval_bval_encoding.h
@@ -53,6 +53,8 @@ exprt aval_bval(const bitnot_exprt &);
 exprt aval_bval_bitwise(const multi_ary_exprt &);
 /// lowering for reduction operators
 exprt aval_bval_reduction(const unary_exprt &);
+/// lowering for replication
+exprt aval_bval_replication(const replication_exprt &);
 /// lowering for ==?
 exprt aval_bval(const verilog_wildcard_equality_exprt &);
 /// lowering for !=?
diff --git a/src/verilog/verilog_lowering.cpp b/src/verilog/verilog_lowering.cpp
index 510644d1b..31dc7eb5a 100644
--- a/src/verilog/verilog_lowering.cpp
+++ b/src/verilog/verilog_lowering.cpp
@@ -571,6 +571,16 @@ exprt verilog_lowering(exprt expr)
     else
       return expr; // leave as is
   }
+  else if(expr.id() == ID_replication)
+  {
+    auto &replication_expr = to_replication_expr(expr);
+
+    // encode into aval/bval
+    if(is_four_valued(expr.type()))
+      return aval_bval_replication(replication_expr);
+    else
+      return expr; // leave as is
+  }
   else if(
     expr.id() == ID_reduction_or || expr.id() == ID_reduction_and ||
     expr.id() == ID_reduction_nor || expr.id() == ID_reduction_nand ||