Verilog: lowering for concatenation of aval/bval encoded vectors

regression/verilog/case/case3.v

@@ -14,9 +14,9 @@ module main(input clk, x, y);
 
   always @(posedge clk)
     casez (cnt1)
-      10'b0z00:;
-      10'b0z01:;
-      10'b0z1z: out=1;
+      {10'b0z, 2'b00}:;
+      {10'b0z, 2'b01}:;
+      {10'b0z, 2'b1z}: out=1;
     endcase
 
   always assert p1: out==0;

regression/verilog/case/case4.v

@@ -4,7 +4,7 @@ module m(input [7:0] i, output reg [31:0] x);
     casex(i)
       8'b1x: x=1;
       8'bxx: x=2;
-      8'b11xx: x=3;
+      { 'b11, 'bx, 'bx }: x=3;
       default: x=4;
     endcase
 

regression/verilog/expressions/concatenation3.desc

@@ -0,0 +1,8 @@
+CORE broken-smt-backend
+concatenation3.sv
+--bound 0
+^EXIT=0$
+^SIGNAL=0$
+^\[.*\] always \(\{ 5'bxz01\?, 4'b10zx \}\) === 9'bxz01\?10zx: PROVED up to bound 0$
+--
+^warning: ignoring

regression/verilog/expressions/concatenation3.sv

@@ -0,0 +1,3 @@
+module main;
+  assert property ({5'bxz01?, 4'b10zx} === 9'bxz01?10zx);
+endmodule

src/verilog/aval_bval_encoding.cpp

@@ -93,32 +93,44 @@ constant_exprt lower_to_aval_bval(const constant_exprt &src)
 
 exprt aval(const exprt &src)
 {
-  PRECONDITION(is_aval_bval(src.type()));
-  auto width = aval_bval_width(src.type());
-  return extractbits_exprt{
-    src, from_integer(0, integer_typet()), bv_typet{width}};
+  if(is_aval_bval(src.type()))
+  {
+    auto width = aval_bval_width(src.type());
+    return extractbits_exprt{src, 0, bv_typet{width}};
+  }
+  else
+  {
+    auto width = to_bitvector_type(src.type()).get_width();
+    return typecast_exprt::conditional_cast(src, bv_typet{width});
+  }
 }
 
 exprt bval(const exprt &src)
 {
-  PRECONDITION(is_aval_bval(src.type()));
-  auto width = aval_bval_width(src.type());
-  return extractbits_exprt{
-    src, from_integer(width, integer_typet()), bv_typet{width}};
+  if(is_aval_bval(src.type()))
+  {
+    auto width = aval_bval_width(src.type());
+    return extractbits_exprt{src, width, bv_typet{width}};
+  }
+  else
+  {
+    // zeros, signaling 0/1
+    auto width = to_bitvector_type(src.type()).get_width();
+    return bv_typet{width}.all_zeros_expr();
+  }
 }
 
 static exprt adjust_size(const exprt &src, std::size_t dest_width)
 {
   auto src_width = to_bv_type(src.type()).get_width();
   if(dest_width > src_width)
   {
-    auto zeros = from_integer(0, bv_typet{dest_width - src_width});
+    auto zeros = bv_typet{dest_width - src_width}.all_zeros_expr();
     return concatenation_exprt{{zeros, src}, bv_typet{dest_width}};
   }
   else if(dest_width < src_width)
   {
-    return extractbits_exprt{
-      src, from_integer(0, integer_typet{}), bv_typet{dest_width}};
+    return extractbits_exprt{src, 0, bv_typet{dest_width}};
   }
   else
     return src;
@@ -152,3 +164,27 @@ exprt aval_bval_conversion(const exprt &src, const typet &dest)
     return combine_aval_bval(new_aval, new_bval, dest);
   }
 }
+
+static exprt concatenate(const exprt::operandst &operands)
+{
+  std::size_t width = 0;
+  for(auto &op : operands)
+    width += to_bv_type(op.type()).get_width();
+
+  return concatenation_exprt{operands, bv_typet{width}};
+}
+
+exprt aval_bval_concatenation(
+  const exprt::operandst &operands,
+  const typet &type)
+{
+  exprt::operandst new_aval, new_bval;
+
+  for(auto &op : operands)
+  {
+    new_aval.push_back(aval(op));
+    new_bval.push_back(bval(op));
+  }
+
+  return combine_aval_bval(concatenate(new_aval), concatenate(new_bval), type);
+}

src/verilog/aval_bval_encoding.h

@@ -34,4 +34,6 @@ exprt bval(const exprt &);
 
 exprt aval_bval_conversion(const exprt &, const typet &);
 
+exprt aval_bval_concatenation(const exprt::operandst &, const typet &);
+
 #endif

src/verilog/verilog_synthesis.cpp

@@ -217,6 +217,22 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
 
     return expr;
   }
+  else if(expr.id() == ID_concatenation)
+  {
+    for(auto &op : expr.operands())
+      op = synth_expr(op, symbol_state);
+
+    if(
+      expr.type().id() == ID_verilog_unsignedbv ||
+      expr.type().id() == ID_verilog_signedbv)
+    {
+      return aval_bval_concatenation(
+        to_concatenation_expr(expr).operands(),
+        lower_to_aval_bval(expr.type()));
+    }
+
+    return expr;
+  }
   else if(expr.id()==ID_function_call)
   {
     return expand_function_call(to_function_call_expr(expr));