Merge pull request #1369 from diffblue/aval_bval_replication

Verilog: aval/bval lowering for replication operator

Author: tautschnig

regression/verilog/asic-world-operators/replication.desc

@@ -1,9 +1,8 @@
-KNOWNBUG
+CORE
 replication.sv
 --module main --bound 0
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-z-related tests fail

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

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()));

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 !=?

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