Skip to content

Commit 947006e

Browse files
kroeningkroening
committed
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.
1 parent 66892c1 commit 947006e

File tree

11 files changed

+248
-3
lines changed

11 files changed

+248
-3
lines changed

‎CHANGELOG‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3,6 +3,7 @@
33
* BMC: Cadical support with --cadical
44
* BMC: iterative constraint strengthening is now default;
55
use --bmc-with-assumptions to re-enable the previous algorithm.
6+
* SystemVerilog: streaming concatenation {<<{...}} and {>>{...}}
67

78
# EBMC 5.3
89

‎regression/verilog/expressions/streaming_concatenation1.desc‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
CORE
2+
streaming_concatenation1.sv
3+
--bound 0
4+
^\[.*\] always \{<<\{4'b1010\}\} == 4'b0101: PROVED up to bound 0$
5+
^\[.*\] always \{<<\{1 == 1\}\} == 1: PROVED up to bound 0$
6+
^\[.*\] always \{<<4\{16'hABCD\}\} == 16'hDCBA: PROVED up to bound 0$
7+
^\[.*\] always \{<<8\{16'hABCD\}\} == 16'hCDAB: PROVED up to bound 0$
8+
^EXIT=0$
9+
^SIGNAL=0$
10+
--
11+
^warning: ignoring
12+
--

‎regression/verilog/expressions/streaming_concatenation1.sv‎

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
module main;
2+
3+
// reverse bits
4+
assert final ({<<{4'b1010}} == 4'b0101);
5+
6+
// works on booleans
7+
assert final ({<<{(1 == 1)}} == 1);
8+
9+
// reverse nibbles
10+
assert final ({<<4{16'habcd}} == 16'hdcba);
11+
12+
// reverse bytes
13+
assert final ({<<8{16'habcd}} == 16'hcdab);
14+
15+
endmodule

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,7 @@ IREP_ID_TWO(C_increasing, #increasing)
7575
IREP_ID_ONE(ports)
7676
IREP_ID_ONE(inst)
7777
IREP_ID_ONE(Verilog)
78+
IREP_ID_ONE(verilog_array_range)
7879
IREP_ID_ONE(verilog_assignment_pattern)
7980
IREP_ID_ONE(verilog_logical_equality)
8081
IREP_ID_ONE(verilog_logical_inequality)
@@ -92,6 +93,8 @@ IREP_ID_ONE(verilog_indexed_part_select_plus)
9293
IREP_ID_ONE(verilog_indexed_part_select_minus)
9394
IREP_ID_ONE(verilog_past)
9495
IREP_ID_ONE(verilog_property_declaration)
96+
IREP_ID_ONE(verilog_streaming_concatenation_left_to_right)
97+
IREP_ID_ONE(verilog_streaming_concatenation_right_to_left)
9598
IREP_ID_ONE(chandle)
9699
IREP_ID_ONE(event)
97100
IREP_ID_ONE(reg)

‎src/verilog/expr2verilog.cpp‎

Lines changed: 52 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1166,6 +1166,50 @@ expr2verilogt::convert_array(const exprt &src, verilog_precedencet precedence)
11661166

11671167
/*******************************************************************\
11681168
1169+
Function: expr2verilogt::convert_streaming_concatenation
1170+
1171+
Inputs:
1172+
1173+
Outputs:
1174+
1175+
Purpose:
1176+
1177+
\*******************************************************************/
1178+
1179+
expr2verilogt::resultt expr2verilogt::convert_streaming_concatenation(
1180+
const std::string &name,
1181+
const verilog_streaming_concatenation_exprt &src)
1182+
{
1183+
std::string dest = "{";
1184+
1185+
dest += name;
1186+
1187+
// slice_size?
1188+
if(src.has_slice_size())
1189+
{
1190+
auto tmp = convert_rec(src.slice_size());
1191+
dest += tmp.s;
1192+
}
1193+
1194+
dest += "{";
1195+
bool first = true;
1196+
for(auto &op : src.stream_expressions())
1197+
{
1198+
if(first)
1199+
first = false;
1200+
else
1201+
dest += ", ";
1202+
dest += convert_rec(op).s;
1203+
}
1204+
dest += "}";
1205+
1206+
dest += "}";
1207+
1208+
return {verilog_precedencet::CONCAT, dest};
1209+
}
1210+
1211+
/*******************************************************************\
1212+
11691213
Function: expr2verilogt::convert_rec
11701214
11711215
Inputs:
@@ -1649,6 +1693,14 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
16491693
else if(src.id() == ID_clog2)
16501694
return convert_function("$clog2", src);
16511695

1696+
else if(src.id() == ID_verilog_streaming_concatenation_left_to_right)
1697+
return convert_streaming_concatenation(
1698+
">>", to_verilog_streaming_concatenation_expr(src));
1699+
1700+
else if(src.id() == ID_verilog_streaming_concatenation_right_to_left)
1701+
return convert_streaming_concatenation(
1702+
"<<", to_verilog_streaming_concatenation_expr(src));
1703+
16521704
// no VERILOG language expression for internal representation
16531705
return convert_norep(src, precedence);
16541706
}

‎src/verilog/expr2verilog_class.h‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -155,6 +155,10 @@ class expr2verilogt
155155
const class verilog_indexed_part_select_plus_or_minus_exprt &,
156156
verilog_precedencet precedence);
157157

158+
resultt convert_streaming_concatenation(
159+
const std::string &name,
160+
const class verilog_streaming_concatenation_exprt &);
161+
158162
protected:
159163
const namespacet &ns;
160164
};

‎src/verilog/parser.y‎

Lines changed: 48 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -3618,13 +3618,57 @@ concatenation: '{' expression_brace '}'
36183618
{ init($$, ID_concatenation); swapop($$, $2); }
36193619
;
36203620

3621-
replication:
3621+
multiple_concatenation:
36223622
'{' expression concatenation '}'
36233623
{ init($$, ID_replication); mto($$, $2); mto($$, $3); }
3624-
| '{' expression replication '}'
3624+
| '{' expression multiple_concatenation '}'
36253625
{ init($$, ID_replication); mto($$, $2); mto($$, $3); }
36263626
;
36273627

3628+
streaming_concatenation:
3629+
'{' stream_operator stream_concatenation '}'
3630+
{ $$ = $2; mto($$, $3); }
3631+
| '{' stream_operator slice_size stream_concatenation '}'
3632+
{ $$ = $2; mto($$, $3); mto($$, $4); }
3633+
;
3634+
3635+
stream_operator:
3636+
TOK_GREATERGREATER
3637+
{ init($$, ID_verilog_streaming_concatenation_left_to_right); }
3638+
| TOK_LESSLESS
3639+
{ init($$, ID_verilog_streaming_concatenation_right_to_left); }
3640+
;
3641+
3642+
slice_size:
3643+
simple_type
3644+
| primary_literal /* really constant_expression */
3645+
;
3646+
3647+
stream_concatenation:
3648+
'{' stream_expression_brace '}'
3649+
{ $$ = $2; }
3650+
;
3651+
3652+
stream_expression_brace:
3653+
stream_expression
3654+
{ init($$); mto($$, $1); }
3655+
| stream_expression_brace ',' stream_expression
3656+
{ $$ = $1; mto($$, $3); }
3657+
;
3658+
3659+
stream_expression:
3660+
expression
3661+
| expression TOK_WITH '[' array_range_expression ']'
3662+
{ init($$, ID_verilog_array_range); mto($$, $1); mto($$, $4); }
3663+
;
3664+
3665+
array_range_expression:
3666+
expression
3667+
| expression TOK_COLON expression
3668+
| expression TOK_PLUSCOLON expression
3669+
| expression TOK_MINUSCOLON expression
3670+
;
3671+
36283672
expression_brace_opt:
36293673
/* Optional */
36303674
{ make_nil($$); }
@@ -3835,12 +3879,13 @@ part_select_range:
38353879
primary: primary_literal
38363880
| hierarchical_identifier_select
38373881
| concatenation
3838-
| replication
3882+
| multiple_concatenation
38393883
| function_subroutine_call
38403884
| '(' mintypmax_expression ')'
38413885
{ $$ = $2; }
38423886
| cast
38433887
| assignment_pattern_expression
3888+
| streaming_concatenation
38443889
| TOK_NULL { init($$, ID_NULL); }
38453890
| TOK_THIS { init($$, ID_this); }
38463891
;

‎src/verilog/verilog_expr.cpp‎

Lines changed: 35 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -305,3 +305,38 @@ exprt verilog_indexed_part_select_plus_or_minus_exprt::lower() const
305305
{
306306
return ::lower(*this);
307307
}
308+
309+
exprt verilog_streaming_concatenation_exprt::lower() const
310+
{
311+
if(id() == ID_verilog_streaming_concatenation_left_to_right)
312+
{
313+
// slice size does not matter
314+
if(stream_expressions().size() == 1)
315+
return stream_expressions().front();
316+
else
317+
PRECONDITION(false);
318+
}
319+
else if(id() == ID_verilog_streaming_concatenation_right_to_left)
320+
{
321+
if(stream_expressions().size() == 1)
322+
{
323+
if(stream_expressions().front().type().id() == ID_bool)
324+
return stream_expressions().front();
325+
else
326+
{
327+
auto slice_size_int =
328+
has_slice_size()
329+
? numeric_cast_v<std::size_t>(to_constant_expr(slice_size()))
330+
: std::size_t(1);
331+
if(slice_size_int == 1)
332+
return bitreverse_exprt{stream_expressions().front()};
333+
else
334+
return bswap_exprt{stream_expressions().front(), slice_size_int};
335+
}
336+
}
337+
else
338+
PRECONDITION(false);
339+
}
340+
else
341+
PRECONDITION(false);
342+
}

‎src/verilog/verilog_expr.h‎

Lines changed: 36 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2475,4 +2475,40 @@ to_verilog_property_declaration(exprt &expr)
24752475
return static_cast<verilog_property_declarationt &>(expr);
24762476
}
24772477

2478+
class verilog_streaming_concatenation_exprt : public exprt
2479+
{
2480+
public:
2481+
bool has_slice_size() const
2482+
{
2483+
return operands().size() == 2;
2484+
}
2485+
2486+
// optional
2487+
const exprt &slice_size() const
2488+
{
2489+
PRECONDITION(has_slice_size());
2490+
return op0();
2491+
}
2492+
2493+
const exprt::operandst &stream_expressions() const
2494+
{
2495+
return has_slice_size() ? op1().operands() : op0().operands();
2496+
}
2497+
2498+
// lower to bitreverse or similar
2499+
exprt lower() const;
2500+
};
2501+
2502+
inline const verilog_streaming_concatenation_exprt &
2503+
to_verilog_streaming_concatenation_expr(const exprt &expr)
2504+
{
2505+
return static_cast<const verilog_streaming_concatenation_exprt &>(expr);
2506+
}
2507+
2508+
inline verilog_streaming_concatenation_exprt &
2509+
to_verilog_streaming_concatenation_expr(exprt &expr)
2510+
{
2511+
return static_cast<verilog_streaming_concatenation_exprt &>(expr);
2512+
}
2513+
24782514
#endif

‎src/verilog/verilog_synthesis.cpp‎

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -348,6 +348,14 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
348348

349349
return expr;
350350
}
351+
else if(
352+
expr.id() == ID_verilog_streaming_concatenation_left_to_right ||
353+
expr.id() == ID_verilog_streaming_concatenation_right_to_left)
354+
{
355+
auto &streaming_concatenation =
356+
to_verilog_streaming_concatenation_expr(expr);
357+
return streaming_concatenation.lower();
358+
}
351359
else if(expr.id() == ID_verilog_non_indexed_part_select)
352360
{
353361
auto &part_select = to_verilog_non_indexed_part_select_expr(expr);

0 commit comments

Comments
 (0)