SystemVerilog: streaming concatenation

CHANGELOG

@@ -3,6 +3,7 @@
 * BMC: Cadical support with --cadical
 * BMC: iterative constraint strengthening is now default;
   use --bmc-with-assumptions to re-enable the previous algorithm.
+* SystemVerilog: streaming concatenation {<<{...}} and {>>{...}}
 
 # EBMC 5.3
 

regression/verilog/expressions/streaming_concatenation1.desc

@@ -0,0 +1,12 @@
+CORE
+streaming_concatenation1.sv
+--bound 0
+^\[.*\] always \{<<\{4'b1010\}\} == 4'b0101: PROVED up to bound 0$
+^\[.*\] always \{<<\{1 == 1\}\} == 1: PROVED up to bound 0$
+^\[.*\] always \{<<4\{16'hABCD\}\} == 16'hDCBA: PROVED up to bound 0$
+^\[.*\] always \{<<8\{16'hABCD\}\} == 16'hCDAB: PROVED up to bound 0$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+--

regression/verilog/expressions/streaming_concatenation1.sv

@@ -0,0 +1,15 @@
+module main;
+
+  // reverse bits
+  assert final ({<<{4'b1010}} == 4'b0101);
+
+  // works on booleans
+  assert final ({<<{(1 == 1)}} == 1);
+
+  // reverse nibbles
+  assert final ({<<4{16'habcd}} == 16'hdcba);
+
+  // reverse bytes
+  assert final ({<<8{16'habcd}} == 16'hcdab);
+
+endmodule

src/hw_cbmc_irep_ids.h

@@ -75,6 +75,7 @@ IREP_ID_TWO(C_increasing, #increasing)
 IREP_ID_ONE(ports)
 IREP_ID_ONE(inst)
 IREP_ID_ONE(Verilog)
+IREP_ID_ONE(verilog_array_range)
 IREP_ID_ONE(verilog_assignment_pattern)
 IREP_ID_ONE(verilog_logical_equality)
 IREP_ID_ONE(verilog_logical_inequality)
@@ -92,6 +93,8 @@ IREP_ID_ONE(verilog_indexed_part_select_plus)
 IREP_ID_ONE(verilog_indexed_part_select_minus)
 IREP_ID_ONE(verilog_past)
 IREP_ID_ONE(verilog_property_declaration)
+IREP_ID_ONE(verilog_streaming_concatenation_left_to_right)
+IREP_ID_ONE(verilog_streaming_concatenation_right_to_left)
 IREP_ID_ONE(chandle)
 IREP_ID_ONE(event)
 IREP_ID_ONE(reg)

src/verilog/expr2verilog.cpp

@@ -1166,6 +1166,50 @@ expr2verilogt::convert_array(const exprt &src, verilog_precedencet precedence)
 
 /*******************************************************************\
 
+Function: expr2verilogt::convert_streaming_concatenation
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+expr2verilogt::resultt expr2verilogt::convert_streaming_concatenation(
+  const std::string &name,
+  const verilog_streaming_concatenation_exprt &src)
+{
+  std::string dest = "{";
+
+  dest += name;
+
+  // slice_size?
+  if(src.has_slice_size())
+  {
+    auto tmp = convert_rec(src.slice_size());
+    dest += tmp.s;
+  }
+
+  dest += "{";
+  bool first = true;
+  for(auto &op : src.stream_expressions())
+  {
+    if(first)
+      first = false;
+    else
+      dest += ", ";
+    dest += convert_rec(op).s;
+  }
+  dest += "}";
+
+  dest += "}";
+
+  return {verilog_precedencet::CONCAT, dest};
+}
+
+/*******************************************************************\
+
 Function: expr2verilogt::convert_rec
 
   Inputs:
@@ -1649,6 +1693,14 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
   else if(src.id() == ID_clog2)
     return convert_function("$clog2", src);
 
+  else if(src.id() == ID_verilog_streaming_concatenation_left_to_right)
+    return convert_streaming_concatenation(
+      ">>", to_verilog_streaming_concatenation_expr(src));
+
+  else if(src.id() == ID_verilog_streaming_concatenation_right_to_left)
+    return convert_streaming_concatenation(
+      "<<", to_verilog_streaming_concatenation_expr(src));
+
   // no VERILOG language expression for internal representation 
   return convert_norep(src, precedence);
 }

src/verilog/expr2verilog_class.h

@@ -155,6 +155,10 @@ class expr2verilogt
     const class verilog_indexed_part_select_plus_or_minus_exprt &,
     verilog_precedencet precedence);
 
+  resultt convert_streaming_concatenation(
+    const std::string &name,
+    const class verilog_streaming_concatenation_exprt &);
+
 protected:
   const namespacet &ns;
 };

src/verilog/parser.y

@@ -3618,13 +3618,57 @@ concatenation: '{' expression_brace '}'
 		{ init($$, ID_concatenation); swapop($$, $2); }
 	;
 
-replication:
+multiple_concatenation:
           '{' expression concatenation '}'
 		{ init($$, ID_replication); mto($$, $2); mto($$, $3); }
-        | '{' expression replication '}'
+        | '{' expression multiple_concatenation '}'
 		{ init($$, ID_replication); mto($$, $2); mto($$, $3); }
 	;
 
+streaming_concatenation:
+	  '{' stream_operator stream_concatenation '}'
+		{ $$ = $2; mto($$, $3); }
+	| '{' stream_operator slice_size stream_concatenation '}'
+		{ $$ = $2; mto($$, $3); mto($$, $4); }
+	;
+
+stream_operator:
+	  TOK_GREATERGREATER
+		{ init($$, ID_verilog_streaming_concatenation_left_to_right); }
+	| TOK_LESSLESS
+		{ init($$, ID_verilog_streaming_concatenation_right_to_left); }
+	;
+
+slice_size:
+	  simple_type
+	| primary_literal /* really constant_expression */
+	;
+
+stream_concatenation:
+	  '{' stream_expression_brace '}'
+		{ $$ = $2; }
+	;
+
+stream_expression_brace:
+	  stream_expression
+		{ init($$); mto($$, $1); }
+	| stream_expression_brace ',' stream_expression
+		{ $$ = $1; mto($$, $3); }
+	;
+
+stream_expression:
+	  expression
+	| expression TOK_WITH '[' array_range_expression ']'
+		{ init($$, ID_verilog_array_range); mto($$, $1); mto($$, $4); }
+	;
+
+array_range_expression:
+	  expression
+	| expression TOK_COLON expression
+	| expression TOK_PLUSCOLON expression
+	| expression TOK_MINUSCOLON expression
+	;
+
 expression_brace_opt:
 	  /* Optional */
           { make_nil($$); }
@@ -3835,12 +3879,13 @@ part_select_range:
 primary:  primary_literal
 	| hierarchical_identifier_select
 	| concatenation 
-        | replication
+        | multiple_concatenation
         | function_subroutine_call
 	| '(' mintypmax_expression ')'
 		{ $$ = $2; }
 	| cast
 	| assignment_pattern_expression
+	| streaming_concatenation
         | TOK_NULL { init($$, ID_NULL); }
         | TOK_THIS { init($$, ID_this); }
 	;

src/verilog/verilog_expr.cpp

@@ -305,3 +305,38 @@ exprt verilog_indexed_part_select_plus_or_minus_exprt::lower() const
 {
   return ::lower(*this);
 }
+
+exprt verilog_streaming_concatenation_exprt::lower() const
+{
+  if(id() == ID_verilog_streaming_concatenation_left_to_right)
+  {
+    // slice size does not matter
+    if(stream_expressions().size() == 1)
+      return stream_expressions().front();
+    else
+      PRECONDITION(false);
+  }
+  else if(id() == ID_verilog_streaming_concatenation_right_to_left)
+  {
+    if(stream_expressions().size() == 1)
+    {
+      if(stream_expressions().front().type().id() == ID_bool)
+        return stream_expressions().front();
+      else
+      {
+        auto slice_size_int =
+          has_slice_size()
+            ? numeric_cast_v<std::size_t>(to_constant_expr(slice_size()))
+            : std::size_t(1);
+        if(slice_size_int == 1)
+          return bitreverse_exprt{stream_expressions().front()};
+        else
+          return bswap_exprt{stream_expressions().front(), slice_size_int};
+      }
+    }
+    else
+      PRECONDITION(false);
+  }
+  else
+    PRECONDITION(false);
+}

src/verilog/verilog_expr.h

@@ -2475,4 +2475,40 @@ to_verilog_property_declaration(exprt &expr)
   return static_cast<verilog_property_declarationt &>(expr);
 }
 
+class verilog_streaming_concatenation_exprt : public exprt
+{
+public:
+  bool has_slice_size() const
+  {
+    return operands().size() == 2;
+  }
+
+  // optional
+  const exprt &slice_size() const
+  {
+    PRECONDITION(has_slice_size());
+    return op0();
+  }
+
+  const exprt::operandst &stream_expressions() const
+  {
+    return has_slice_size() ? op1().operands() : op0().operands();
+  }
+
+  // lower to bitreverse or similar
+  exprt lower() const;
+};
+
+inline const verilog_streaming_concatenation_exprt &
+to_verilog_streaming_concatenation_expr(const exprt &expr)
+{
+  return static_cast<const verilog_streaming_concatenation_exprt &>(expr);
+}
+
+inline verilog_streaming_concatenation_exprt &
+to_verilog_streaming_concatenation_expr(exprt &expr)
+{
+  return static_cast<verilog_streaming_concatenation_exprt &>(expr);
+}
+
 #endif

src/verilog/verilog_synthesis.cpp

@@ -348,6 +348,14 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
 
     return expr;
   }
+  else if(
+    expr.id() == ID_verilog_streaming_concatenation_left_to_right ||
+    expr.id() == ID_verilog_streaming_concatenation_right_to_left)
+  {
+    auto &streaming_concatenation =
+      to_verilog_streaming_concatenation_expr(expr);
+    return streaming_concatenation.lower();
+  }
   else if(expr.id() == ID_verilog_non_indexed_part_select)
   {
     auto &part_select = to_verilog_non_indexed_part_select_expr(expr);

src/verilog/verilog_typecheck_expr.cpp

@@ -2596,6 +2596,16 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
     convert_expr(expr.op());
     expr.id(ID_typecast);
   }
+  else if(
+    expr.id() == ID_verilog_streaming_concatenation_left_to_right ||
+    expr.id() == ID_verilog_streaming_concatenation_right_to_left)
+  {
+    // slice_size is defaulted to 1
+    PRECONDITION(expr.op().operands().size() == 1);
+    convert_expr(expr.op().operands()[0]);
+    expr.type() = expr.op().operands()[0].type();
+    return std::move(expr);
+  }
   else
   {
     convert_expr(expr.op());
@@ -3145,6 +3155,30 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
     expr.type() = bool_typet();
     return std::move(expr);
   }
+  else if(
+    expr.id() == ID_verilog_streaming_concatenation_left_to_right ||
+    expr.id() == ID_verilog_streaming_concatenation_right_to_left)
+  {
+    auto slice_size = convert_integer_constant_expression(expr.op0());
+
+    if(slice_size < 1)
+    {
+      // 1800-2017 11.4.14.2 "it shall be an error for the
+      // value of the expression to be zero or negative"
+      throw errort().with_location(expr.source_location())
+        << "size slice must be 1 or greater";
+    }
+
+    expr.op0() = from_integer(slice_size, natural_typet());
+
+    convert_expr(expr.op0());
+    PRECONDITION(expr.op1().operands().size() == 1);
+    for(auto &op : expr.op1().operands())
+      convert_expr(op);
+    expr.type() = expr.op1().operands().front().type();
+
+    return std::move(expr);
+  }
   else
   {
     // type is guessed for now