Skip to content

Commit 72058bb

Browse files
kroeningkroening
committed
SystemVerilog: set membership operator
This adds the set membership operator, 1800-2017 11.4.13.
1 parent d6449b1 commit 72058bb

File tree

10 files changed

+244
-2
lines changed

10 files changed

+244
-2
lines changed

‎regression/verilog/expressions/inside1.desc‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE broken-smt-backend
2+
inside1.sv
3+
--bound 0
4+
^\[.*\] always 2 inside \{1, 2, 3\}: PROVED up to bound 0$
5+
^\[.*\] always 2 inside \{3'b0\?0\}: PROVED up to bound 0$
6+
^\[.*\] always !\(2 inside \{3'b0\?1\}\): PROVED up to bound 0$
7+
^\[.*\] always 2 inside \{\[1:3\], \[6:8\]\}: PROVED up to bound 0$
8+
^\[.*\] always !\(4 inside \{\[1:3\], \[6:8\]\}\): PROVED up to bound 0$
9+
^\[.*\] always \(1 && 1\) inside \{1, 2, 3\}: PROVED up to bound 0$
10+
^EXIT=0$
11+
^SIGNAL=0$
12+
--
13+
^warning: ignoring

‎regression/verilog/expressions/inside1.sv‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
module main;
2+
3+
assert final (2 inside {1, 2, 3});
4+
assert final (2 inside {3'b0?0});
5+
assert final (!(2 inside {3'b0?1}));
6+
assert final (2 inside {[1:3], [6:8]});
7+
assert final (!(4 inside {[1:3], [6:8]}));
8+
assert final ((1&&1) inside {1, 2, 3});
9+
10+
endmodule

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -84,6 +84,7 @@ IREP_ID_ONE(verilog_wildcard_inequality)
8484
IREP_ID_ONE(verilog_explicit_cast)
8585
IREP_ID_ONE(verilog_size_cast)
8686
IREP_ID_ONE(verilog_implicit_typecast)
87+
IREP_ID_ONE(verilog_inside)
8788
IREP_ID_ONE(verilog_unique)
8889
IREP_ID_ONE(verilog_unique0)
8990
IREP_ID_ONE(verilog_priority)
@@ -93,6 +94,7 @@ IREP_ID_ONE(verilog_indexed_part_select_plus)
9394
IREP_ID_ONE(verilog_indexed_part_select_minus)
9495
IREP_ID_ONE(verilog_past)
9596
IREP_ID_ONE(verilog_property_declaration)
97+
IREP_ID_ONE(verilog_value_range)
9698
IREP_ID_ONE(verilog_streaming_concatenation_left_to_right)
9799
IREP_ID_ONE(verilog_streaming_concatenation_right_to_left)
98100
IREP_ID_ONE(chandle)

‎src/verilog/expr2verilog.cpp‎

Lines changed: 68 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1210,6 +1210,68 @@ expr2verilogt::resultt expr2verilogt::convert_streaming_concatenation(
12101210

12111211
/*******************************************************************\
12121212
1213+
Function: expr2verilogt::convert_inside
1214+
1215+
Inputs:
1216+
1217+
Outputs:
1218+
1219+
Purpose:
1220+
1221+
\*******************************************************************/
1222+
1223+
expr2verilogt::resultt
1224+
expr2verilogt::convert_inside(const verilog_inside_exprt &src)
1225+
{
1226+
std::string dest;
1227+
auto precedence = verilog_precedencet::RELATION;
1228+
1229+
auto op = convert_rec(src.op());
1230+
1231+
if(precedence > op.p)
1232+
dest += '(';
1233+
dest += op.s;
1234+
if(precedence > op.p)
1235+
dest += ')';
1236+
1237+
dest += " inside {";
1238+
bool first = true;
1239+
for(auto &op : src.range_list())
1240+
{
1241+
if(first)
1242+
first = false;
1243+
else
1244+
dest += ", ";
1245+
dest += convert_rec(op).s;
1246+
}
1247+
dest += "}";
1248+
1249+
return {precedence, dest};
1250+
}
1251+
1252+
/*******************************************************************\
1253+
1254+
Function: expr2verilogt::convert_value_range
1255+
1256+
Inputs:
1257+
1258+
Outputs:
1259+
1260+
Purpose:
1261+
1262+
\*******************************************************************/
1263+
1264+
expr2verilogt::resultt
1265+
expr2verilogt::convert_value_range(const verilog_value_range_exprt &src)
1266+
{
1267+
std::string dest =
1268+
'[' + convert_rec(src.lhs()).s + ':' + convert_rec(src.rhs()).s + ']';
1269+
1270+
return {verilog_precedencet::MEMBER, dest};
1271+
}
1272+
1273+
/*******************************************************************\
1274+
12131275
Function: expr2verilogt::convert_rec
12141276
12151277
Inputs:
@@ -1701,6 +1763,12 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
17011763
return convert_streaming_concatenation(
17021764
"<<", to_verilog_streaming_concatenation_expr(src));
17031765

1766+
else if(src.id() == ID_verilog_inside)
1767+
return convert_inside(to_verilog_inside_expr(src));
1768+
1769+
else if(src.id() == ID_verilog_value_range)
1770+
return convert_value_range(to_verilog_value_range_expr(src));
1771+
17041772
// no VERILOG language expression for internal representation
17051773
return convert_norep(src, precedence);
17061774
}

‎src/verilog/expr2verilog_class.h‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ enum class verilog_precedencet
3030
MULT = 15, // * / %
3131
ADD = 14, // + -
3232
SHIFT = 13, // << >> <<< >>>
33-
RELATION = 12, // > >= < <=
33+
RELATION = 12, // > >= < <= inside dist
3434
EQUALITY = 11, // == != === !== ==? !=?
3535
BITAND = 10, // &
3636
XOR = 9, // ^ ~^ ^~ (binary)
@@ -159,6 +159,10 @@ class expr2verilogt
159159
const std::string &name,
160160
const class verilog_streaming_concatenation_exprt &);
161161

162+
resultt convert_inside(const class verilog_inside_exprt &);
163+
164+
resultt convert_value_range(const class verilog_value_range_exprt &);
165+
162166
protected:
163167
const namespacet &ns;
164168
};

‎src/verilog/parser.y‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3360,6 +3360,15 @@ case_item:
33603360
mto($$, $2); }
33613361
;
33623362

3363+
open_range_list:
3364+
open_value_range
3365+
{ init($$); mto($$, $1); }
3366+
| open_range_list ',' open_value_range
3367+
{ $$=$1; mto($$, $3); }
3368+
;
3369+
3370+
open_value_range: value_range;
3371+
33633372
// System Verilog standard 1800-2017
33643373
// A.6.7.1 Patterns
33653374

@@ -3854,11 +3863,18 @@ expression:
38543863
{ init($$, ID_if); mto($$, $1); mto($$, $3); mto($$, $5); }
38553864
| TOK_QSTRING
38563865
{ init($$, ID_constant); stack_expr($$).type()=typet(ID_string); addswap($$, ID_value, $1); }
3866+
| inside_expression
3867+
;
3868+
3869+
inside_expression:
3870+
expression TOK_INSIDE '{' open_range_list '}'
3871+
{ init($$, ID_verilog_inside); mto($$, $1); mto($$, $4); }
38573872
;
38583873

38593874
value_range:
38603875
expression
38613876
| '[' expression TOK_COLON expression ']'
3877+
{ init($$, ID_verilog_value_range); mto($$, $2); mto($$, $4); }
38623878
;
38633879

38643880
indexed_range:

‎src/verilog/verilog_expr.cpp‎

Lines changed: 51 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -15,6 +15,18 @@ Author: Daniel Kroening, kroening@kroening.com
1515
#include <util/prefix.h>
1616

1717
#include "verilog_typecheck_base.h"
18+
#include "verilog_types.h"
19+
20+
verilog_wildcard_equality_exprt::verilog_wildcard_equality_exprt(
21+
exprt lhs,
22+
exprt rhs)
23+
: binary_exprt(
24+
std::move(lhs),
25+
ID_verilog_wildcard_equality,
26+
std::move(rhs),
27+
verilog_unsignedbv_typet{1})
28+
{
29+
}
1830

1931
typet verilog_declaratort::merged_type(const typet &declaration_type) const
2032
{
@@ -340,3 +352,42 @@ exprt verilog_streaming_concatenation_exprt::lower() const
340352
else
341353
PRECONDITION(false);
342354
}
355+
356+
exprt verilog_inside_exprt::lower() const
357+
{
358+
exprt::operandst disjuncts;
359+
360+
for(auto &range : range_list())
361+
{
362+
if(range.id() == ID_verilog_value_range)
363+
{
364+
auto &range_expr = to_verilog_value_range_expr(range);
365+
DATA_INVARIANT(
366+
op().type() == range_expr.lhs().type(),
367+
"inside_exprt type consistency");
368+
DATA_INVARIANT(
369+
op().type() == range_expr.rhs().type(),
370+
"inside_exprt type consistency");
371+
disjuncts.push_back(and_exprt{
372+
binary_relation_exprt{op(), ID_ge, range_expr.lhs()},
373+
binary_relation_exprt{op(), ID_le, range_expr.rhs()}});
374+
}
375+
else
376+
{
377+
DATA_INVARIANT(
378+
op().type() == range.type(), "inside_exprt type consistency");
379+
auto &range_type = range.type();
380+
if(
381+
range_type.id() == ID_verilog_unsignedbv ||
382+
range_type.id() == ID_verilog_signedbv)
383+
{
384+
disjuncts.push_back(typecast_exprt{
385+
verilog_wildcard_equality_exprt{op(), range}, bool_typet()});
386+
}
387+
else
388+
disjuncts.push_back(equal_exprt{op(), range});
389+
}
390+
}
391+
392+
return disjunction(disjuncts);
393+
}

‎src/verilog/verilog_expr.h‎

Lines changed: 55 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -109,9 +109,10 @@ to_verilog_logical_inequality_expr(exprt &expr)
109109
}
110110

111111
/// ==?
112-
class verilog_wildcard_equality_exprt : public equal_exprt
112+
class verilog_wildcard_equality_exprt : public binary_exprt
113113
{
114114
public:
115+
verilog_wildcard_equality_exprt(exprt, exprt);
115116
};
116117

117118
inline const verilog_wildcard_equality_exprt &
@@ -2511,4 +2512,57 @@ to_verilog_streaming_concatenation_expr(exprt &expr)
25112512
return static_cast<verilog_streaming_concatenation_exprt &>(expr);
25122513
}
25132514

2515+
class verilog_inside_exprt : public binary_exprt
2516+
{
2517+
public:
2518+
const exprt &op() const
2519+
{
2520+
return op0();
2521+
}
2522+
2523+
const exprt::operandst &range_list() const
2524+
{
2525+
return op1().operands();
2526+
}
2527+
2528+
// lower to ==, ==?, >=, <=
2529+
exprt lower() const;
2530+
};
2531+
2532+
inline const verilog_inside_exprt &to_verilog_inside_expr(const exprt &expr)
2533+
{
2534+
PRECONDITION(expr.id() == ID_verilog_inside);
2535+
verilog_inside_exprt::check(expr);
2536+
return static_cast<const verilog_inside_exprt &>(expr);
2537+
}
2538+
2539+
inline verilog_inside_exprt &to_verilog_inside_expr(exprt &expr)
2540+
{
2541+
PRECONDITION(expr.id() == ID_verilog_inside);
2542+
verilog_inside_exprt::check(expr);
2543+
return static_cast<verilog_inside_exprt &>(expr);
2544+
}
2545+
2546+
class verilog_value_range_exprt : public binary_exprt
2547+
{
2548+
public:
2549+
// lower to >=, <=
2550+
exprt lower() const;
2551+
};
2552+
2553+
inline const verilog_value_range_exprt &
2554+
to_verilog_value_range_expr(const exprt &expr)
2555+
{
2556+
PRECONDITION(expr.id() == ID_verilog_value_range);
2557+
verilog_value_range_exprt::check(expr);
2558+
return static_cast<const verilog_value_range_exprt &>(expr);
2559+
}
2560+
2561+
inline verilog_value_range_exprt &to_verilog_value_range_expr(exprt &expr)
2562+
{
2563+
PRECONDITION(expr.id() == ID_verilog_value_range);
2564+
verilog_value_range_exprt::check(expr);
2565+
return static_cast<verilog_value_range_exprt &>(expr);
2566+
}
2567+
25142568
#endif

‎src/verilog/verilog_synthesis.cpp‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -208,6 +208,12 @@ exprt verilog_synthesist::synth_expr(exprt expr, symbol_statet symbol_state)
208208
to_hierarchical_identifier_expr(expr), symbol_state);
209209
return expr;
210210
}
211+
else if(expr.id() == ID_verilog_inside)
212+
{
213+
// The lowering uses wildcard equality, which needs to be further lowered
214+
auto &inside = to_verilog_inside_expr(expr);
215+
expr = inside.lower();
216+
}
211217

212218
// Do the operands recursively
213219
for(auto &op : expr.operands())

‎src/verilog/verilog_typecheck_expr.cpp‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -3179,6 +3179,24 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
31793179

31803180
return std::move(expr);
31813181
}
3182+
else if(expr.id() == ID_verilog_inside)
3183+
{
3184+
convert_expr(expr.op0());
3185+
for(auto &op : expr.op1().operands())
3186+
{
3187+
convert_expr(op);
3188+
if(op.id() == ID_verilog_value_range)
3189+
{
3190+
auto &value_range = to_verilog_value_range_expr(op);
3191+
tc_binary_expr(expr, value_range.lhs(), op);
3192+
tc_binary_expr(expr, value_range.rhs(), op);
3193+
}
3194+
else
3195+
tc_binary_expr(expr, expr.op0(), op);
3196+
}
3197+
expr.type() = bool_typet{};
3198+
return std::move(expr);
3199+
}
31823200
else
31833201
{
31843202
// type is guessed for now

0 commit comments

Comments
 (0)