From 947006e0fd8c15ff4858070a47d8f199dec70c9b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Wed, 13 Nov 2024 12:06:28 +0000 Subject: [PATCH] SystemVerilog: streaming concatenation This adds SystemVerilog's streaming concatenation operators {<<{...}} and {>>{...}}. Lowering is implemented for slice size 1 (the default) via bitreverse expressions, and via bswap expressions for other slice sizes. --- CHANGELOG | 1 + .../expressions/streaming_concatenation1.desc | 12 +++++ .../expressions/streaming_concatenation1.sv | 15 ++++++ src/hw_cbmc_irep_ids.h | 3 ++ src/verilog/expr2verilog.cpp | 52 +++++++++++++++++++ src/verilog/expr2verilog_class.h | 4 ++ src/verilog/parser.y | 51 ++++++++++++++++-- src/verilog/verilog_expr.cpp | 35 +++++++++++++ src/verilog/verilog_expr.h | 36 +++++++++++++ src/verilog/verilog_synthesis.cpp | 8 +++ src/verilog/verilog_typecheck_expr.cpp | 34 ++++++++++++ 11 files changed, 248 insertions(+), 3 deletions(-) create mode 100644 regression/verilog/expressions/streaming_concatenation1.desc create mode 100644 regression/verilog/expressions/streaming_concatenation1.sv diff --git a/CHANGELOG b/CHANGELOG index 963968718..dc60b0654 100644 --- a/CHANGELOG +++ b/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 diff --git a/regression/verilog/expressions/streaming_concatenation1.desc b/regression/verilog/expressions/streaming_concatenation1.desc new file mode 100644 index 000000000..2c6516b59 --- /dev/null +++ b/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 +-- diff --git a/regression/verilog/expressions/streaming_concatenation1.sv b/regression/verilog/expressions/streaming_concatenation1.sv new file mode 100644 index 000000000..a47f7b477 --- /dev/null +++ b/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 diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h index 715f92cf0..589ba4563 100644 --- a/src/hw_cbmc_irep_ids.h +++ b/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) diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp index a33c97de1..054fc5e21 100644 --- a/src/verilog/expr2verilog.cpp +++ b/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); } diff --git a/src/verilog/expr2verilog_class.h b/src/verilog/expr2verilog_class.h index 805ffdd1d..fdffcf850 100644 --- a/src/verilog/expr2verilog_class.h +++ b/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; }; diff --git a/src/verilog/parser.y b/src/verilog/parser.y index 904471734..d001ff5e6 100644 --- a/src/verilog/parser.y +++ b/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); } ; diff --git a/src/verilog/verilog_expr.cpp b/src/verilog/verilog_expr.cpp index 50e2bf75c..258e7f6fd 100644 --- a/src/verilog/verilog_expr.cpp +++ b/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(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); +} diff --git a/src/verilog/verilog_expr.h b/src/verilog/verilog_expr.h index 6f6c06e0f..36b3823b0 100644 --- a/src/verilog/verilog_expr.h +++ b/src/verilog/verilog_expr.h @@ -2475,4 +2475,40 @@ to_verilog_property_declaration(exprt &expr) return static_cast(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(expr); +} + +inline verilog_streaming_concatenation_exprt & +to_verilog_streaming_concatenation_expr(exprt &expr) +{ + return static_cast(expr); +} + #endif diff --git a/src/verilog/verilog_synthesis.cpp b/src/verilog/verilog_synthesis.cpp index 3c7925499..e87cd9185 100644 --- a/src/verilog/verilog_synthesis.cpp +++ b/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); diff --git a/src/verilog/verilog_typecheck_expr.cpp b/src/verilog/verilog_typecheck_expr.cpp index 21083262b..befab2870 100644 --- a/src/verilog/verilog_typecheck_expr.cpp +++ b/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