Skip to content

Commit 72d9130

Browse files
kroeningkroening
committed
SVA: replace sva_sequence_concatenation_exprt
This replaces the sva_sequence_concatenation_exprt by multi-operand variants of sva_cycle_delay_exprt, sva_cycle_delay_plus_exprt and sva_cycle_delay_star_exprt. This simplifies the implementation of the SystemVerilog concatenation rules.
1 parent 8f220ab commit 72d9130

File tree

11 files changed

+93
-192
lines changed

11 files changed

+93
-192
lines changed

‎src/hw_cbmc_irep_ids.h

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -60,7 +60,6 @@ IREP_ID_ONE(sva_cycle_delay)
6060
IREP_ID_ONE(sva_cycle_delay_star)
6161
IREP_ID_ONE(sva_cycle_delay_plus)
6262
IREP_ID_ONE(sva_disable_iff)
63-
IREP_ID_ONE(sva_sequence_concatenation)
6463
IREP_ID_ONE(sva_sequence_first_match)
6564
IREP_ID_ONE(sva_sequence_goto_repetition)
6665
IREP_ID_ONE(sva_sequence_intersect)

‎src/temporal-logic/ltl_sva_to_string.cpp

Lines changed: 42 additions & 48 deletions
Original file line numberDiff line numberDiff line change
@@ -327,22 +327,49 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
327327
PRECONDITION(mode == PROPERTY || mode == SVA_SEQUENCE);
328328
return rec(to_sva_boolean_expr(expr).op(), BOOLEAN);
329329
}
330-
else if(expr.id() == ID_sva_sequence_concatenation)
330+
else if(expr.id() == ID_sva_cycle_delay)
331331
{
332332
PRECONDITION(mode == SVA_SEQUENCE);
333-
// SVA sequence concatenation is overlapping, whereas
334-
// the ; operator is nonoverlapping. We special-case
335-
// the following for better readability:
336-
// f ##0 g --> f : g
337-
// f ##1 g --> f ; g
338-
// f ##n g --> f ; 1[*n-1] ; b
339-
auto &concatenation = to_sva_sequence_concatenation_expr(expr);
340-
if(concatenation.rhs().id() == ID_sva_cycle_delay)
333+
auto &delay = to_sva_cycle_delay_expr(expr);
334+
335+
if(delay.lhs().is_nil())
341336
{
342-
auto &delay = to_sva_cycle_delay_expr(concatenation.rhs());
337+
auto new_expr = unary_exprt{expr.id(), delay.op()};
343338

344-
auto new_expr = concatenation;
345-
new_expr.rhs() = delay.op();
339+
if(delay.is_range()) // ##[from:to] rhs
340+
{
341+
auto from = numeric_cast_v<mp_integer>(delay.from());
342+
343+
if(delay.is_unbounded()) // ##[n:$] rhs
344+
{
345+
return prefix(
346+
"1[*" + integer2string(from) + "..] ; ", new_expr, mode);
347+
}
348+
else
349+
{
350+
auto to = numeric_cast_v<mp_integer>(delay.to());
351+
PRECONDITION(to >= 0);
352+
return prefix(
353+
"1[*" + integer2string(from) + ".." + integer2string(to) + "] ; ",
354+
new_expr,
355+
mode);
356+
}
357+
}
358+
else // ##n rhs
359+
{
360+
auto i = numeric_cast_v<mp_integer>(delay.from());
361+
PRECONDITION(i >= 0);
362+
return prefix("1[*" + integer2string(i) + "] ; ", new_expr, mode);
363+
}
364+
}
365+
else // lhs is not nil
366+
{
367+
// We special-case the following for better readability:
368+
// f ##0 g --> f : g
369+
// f ##1 g --> f ; g
370+
// f ##n g --> f ; 1[*n-1] ; b
371+
auto new_expr =
372+
binary_exprt{delay.lhs(), delay.id(), delay.rhs(), delay.type()};
346373

347374
if(delay.is_range())
348375
{
@@ -354,12 +381,12 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
354381
throw ebmc_errort{}
355382
<< "cannot convert 0.. ranged sequence concatenation to Buechi";
356383
}
357-
else if(delay.is_unbounded())
384+
else if(delay.is_unbounded()) // f ##[n:$] g
358385
{
359386
return infix(
360387
" ; 1[*" + integer2string(from - 1) + "..] ; ", new_expr, mode);
361388
}
362-
else
389+
else // f ##[from:to] g
363390
{
364391
auto to = numeric_cast_v<mp_integer>(delay.to());
365392
PRECONDITION(to >= 0);
@@ -370,7 +397,7 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
370397
mode);
371398
}
372399
}
373-
else
400+
else // f ##n g
374401
{
375402
auto n = numeric_cast_v<mp_integer>(delay.from());
376403
PRECONDITION(n >= 0);
@@ -385,39 +412,6 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
385412
}
386413
}
387414
}
388-
else
389-
return infix(":", expr, mode);
390-
}
391-
else if(expr.id() == ID_sva_cycle_delay)
392-
{
393-
PRECONDITION(mode == SVA_SEQUENCE);
394-
auto &delay = to_sva_cycle_delay_expr(expr);
395-
unary_exprt new_expr{expr.id(), delay.op()};
396-
397-
if(delay.is_range())
398-
{
399-
auto from = numeric_cast_v<mp_integer>(delay.from());
400-
401-
if(delay.is_unbounded())
402-
{
403-
return prefix("1[*" + integer2string(from) + "..] ; ", new_expr, mode);
404-
}
405-
else
406-
{
407-
auto to = numeric_cast_v<mp_integer>(delay.to());
408-
PRECONDITION(to >= 0);
409-
return prefix(
410-
"1[*" + integer2string(from) + ".." + integer2string(to) + "] ; ",
411-
new_expr,
412-
mode);
413-
}
414-
}
415-
else // singleton
416-
{
417-
auto i = numeric_cast_v<mp_integer>(delay.from());
418-
PRECONDITION(i >= 0);
419-
return prefix("1[*" + integer2string(i) + "] ; ", new_expr, mode);
420-
}
421415
}
422416
else if(expr.id() == ID_sva_cycle_delay_star) // ##[*] something
423417
{

‎src/temporal-logic/sva_sequence_match.cpp

Lines changed: 39 additions & 39 deletions
Original file line numberDiff line numberDiff line change
@@ -58,26 +58,6 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
5858
// atomic proposition
5959
return {sva_sequence_matcht{to_sva_boolean_expr(sequence).op()}};
6060
}
61-
else if(sequence.id() == ID_sva_sequence_concatenation)
62-
{
63-
auto &concatenation = to_sva_sequence_concatenation_expr(sequence);
64-
auto matches_lhs = LTL_sequence_matches(concatenation.lhs());
65-
auto matches_rhs = LTL_sequence_matches(concatenation.rhs());
66-
67-
std::vector<sva_sequence_matcht> result;
68-
69-
// cross product
70-
for(auto &match_lhs : matches_lhs)
71-
for(auto &match_rhs : matches_rhs)
72-
{
73-
// Sequence concatenation is overlapping
74-
auto new_match = overlapping_concat(match_lhs, match_rhs);
75-
CHECK_RETURN(
76-
new_match.length() == match_lhs.length() + match_rhs.length() - 1);
77-
result.push_back(std::move(new_match));
78-
}
79-
return result;
80-
}
8161
else if(sequence.id() == ID_sva_sequence_repetition_star) // [*n], [*n:m]
8262
{
8363
auto &repetition = to_sva_sequence_repetition_star_expr(sequence);
@@ -119,41 +99,61 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
11999
else if(sequence.id() == ID_sva_cycle_delay)
120100
{
121101
auto &delay = to_sva_cycle_delay_expr(sequence);
122-
auto matches = LTL_sequence_matches(delay.op());
123-
auto from_int = numeric_cast_v<mp_integer>(delay.from());
124102

125-
if(!delay.is_range())
103+
// These have an optional LHS and a RHS.
104+
std::vector<sva_sequence_matcht> lhs_matches;
105+
106+
if(delay.lhs().is_nil())
126107
{
127-
// delay as instructed
128-
auto delay_sequence = sva_sequence_matcht::true_match(from_int);
108+
// If the LHS is not given, it's equivalent to 'true'.
109+
lhs_matches = {sva_sequence_matcht::true_match(1)};
110+
}
111+
else
112+
{
113+
lhs_matches = LTL_sequence_matches(delay.lhs());
114+
}
129115

130-
for(auto &match : matches)
131-
match = concat(delay_sequence, match);
116+
// The delay in between lhs and rhs
117+
std::vector<sva_sequence_matcht> delay_matches;
118+
119+
auto from_int = numeric_cast_v<mp_integer>(delay.from());
132120

133-
return matches;
121+
if(!delay.is_range()) // f ##n g
122+
{
123+
delay_matches = {sva_sequence_matcht::true_match(from_int)};
134124
}
135-
else if(delay.is_unbounded())
125+
else if(delay.is_unbounded()) // f ##[from:$] g
136126
{
137127
throw sva_sequence_match_unsupportedt{sequence}; // can't encode
138128
}
139-
else
129+
else // f ##[from:to] g
140130
{
141131
auto to_int = numeric_cast_v<mp_integer>(delay.to());
142-
std::vector<sva_sequence_matcht> new_matches;
143132

144133
for(mp_integer i = from_int; i <= to_int; ++i)
145-
{
146-
// delay as instructed
147-
auto delay_sequence = sva_sequence_matcht::true_match(i);
134+
delay_matches.push_back(sva_sequence_matcht::true_match(i));
135+
}
136+
137+
// now do RHS
138+
auto rhs_matches = LTL_sequence_matches(delay.rhs());
139+
140+
// cross product lhs x delay x rhs
141+
std::vector<sva_sequence_matcht> result;
148142

149-
for(const auto &match : matches)
143+
for(auto &lhs_match : lhs_matches)
144+
for(auto &delay_match : delay_matches)
145+
for(auto &rhs_match : rhs_matches)
150146
{
151-
new_matches.push_back(concat(delay_sequence, match));
147+
// Sequence concatenation is overlapping
148+
auto new_match =
149+
overlapping_concat(lhs_match, concat(delay_match, rhs_match));
150+
CHECK_RETURN(
151+
new_match.length() ==
152+
lhs_match.length() + delay_match.length() + rhs_match.length() - 1);
153+
result.push_back(std::move(new_match));
152154
}
153-
}
154155

155-
return new_matches;
156-
}
156+
return result;
157157
}
158158
else if(sequence.id() == ID_sva_and)
159159
{

‎src/temporal-logic/temporal_logic.cpp

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -107,7 +107,6 @@ bool is_SVA_sequence_operator(const exprt &expr)
107107
// Note that ID_sva_not does not yield a sequence expression.
108108
return id == ID_sva_and || id == ID_sva_or || id == ID_sva_cycle_delay ||
109109
id == ID_sva_cycle_delay_plus || id == ID_sva_cycle_delay_star ||
110-
id == ID_sva_sequence_concatenation ||
111110
id == ID_sva_sequence_intersect || id == ID_sva_sequence_first_match ||
112111
id == ID_sva_sequence_throughout || id == ID_sva_sequence_within ||
113112
id == ID_sva_sequence_goto_repetition ||

‎src/trans-word-level/sequence.cpp

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -160,6 +160,7 @@ sequence_matchest instantiate_sequence(
160160
return instantiate_sequence(
161161
cycle_delay_plus.lower(), semantics, t, no_timeframes);
162162
}
163+
#if 0
163164
else if(expr.id() == ID_sva_sequence_concatenation)
164165
{
165166
auto &implication = to_binary_expr(expr);
@@ -196,6 +197,7 @@ sequence_matchest instantiate_sequence(
196197

197198
return result;
198199
}
200+
#endif
199201
else if(expr.id() == ID_sva_sequence_intersect)
200202
{
201203
// IEEE 1800-2017 16.9.6

‎src/verilog/expr2verilog.cpp

Lines changed: 0 additions & 56 deletions
Original file line numberDiff line numberDiff line change
@@ -214,47 +214,6 @@ expr2verilogt::resultt expr2verilogt::convert_sva_cycle_delay(
214214

215215
/*******************************************************************\
216216
217-
Function: expr2verilogt::convert_sva_sequence_concatenation
218-
219-
Inputs:
220-
221-
Outputs:
222-
223-
Purpose:
224-
225-
\*******************************************************************/
226-
227-
expr2verilogt::resultt expr2verilogt::convert_sva_sequence_concatenation(
228-
const binary_exprt &src,
229-
verilog_precedencet precedence)
230-
{
231-
if(src.operands().size()!=2)
232-
return convert_norep(src);
233-
234-
std::string dest;
235-
236-
auto op0 = convert_rec(src.op0());
237-
auto op1 = convert_rec(src.op1());
238-
239-
if(precedence > op0.p)
240-
dest += '(';
241-
dest += op0.s;
242-
if(precedence > op0.p)
243-
dest += ')';
244-
245-
dest+=' ';
246-
247-
if(precedence > op0.p)
248-
dest += '(';
249-
dest += op1.s;
250-
if(precedence > op0.p)
251-
dest += ')';
252-
253-
return {precedence, dest};
254-
}
255-
256-
/*******************************************************************\
257-
258217
Function: expr2verilogt::convert_sva_sequence_first_match
259218
260219
Inputs:
@@ -1861,11 +1820,6 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
18611820
return convert_rec(to_sva_boolean_expr(src).op());
18621821
}
18631822

1864-
else if(src.id()==ID_sva_sequence_concatenation)
1865-
return convert_sva_sequence_concatenation(
1866-
to_binary_expr(src), precedence = verilog_precedencet::MIN);
1867-
// not sure about precedence
1868-
18691823
else if(src.id() == ID_sva_sequence_first_match)
18701824
return convert_sva_sequence_first_match(
18711825
to_sva_sequence_first_match_expr(src));
@@ -1885,16 +1839,6 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
18851839
convert_sva_binary("within", to_binary_expr(src));
18861840
// not sure about precedence
18871841

1888-
else if(src.id() == ID_sva_sequence_within)
1889-
return convert_sva_sequence_concatenation(
1890-
to_binary_expr(src), precedence = verilog_precedencet::MIN);
1891-
// not sure about precedence
1892-
1893-
else if(src.id() == ID_sva_sequence_throughout)
1894-
return convert_sva_sequence_concatenation(
1895-
to_binary_expr(src), precedence = verilog_precedencet::MIN);
1896-
// not sure about precedence
1897-
18981842
else if(src.id()==ID_sva_always)
18991843
return precedence = verilog_precedencet::MIN,
19001844
convert_sva_unary("always", to_sva_always_expr(src));

‎src/verilog/expr2verilog_class.h

Lines changed: 0 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -161,9 +161,6 @@ class expr2verilogt
161161

162162
resultt convert_sva_if(const sva_if_exprt &);
163163

164-
resultt
165-
convert_sva_sequence_concatenation(const binary_exprt &, verilog_precedencet);
166-
167164
resultt
168165
convert_sva_sequence_first_match(const sva_sequence_first_match_exprt &);
169166

‎src/verilog/parser.y

Lines changed: 8 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -2538,11 +2538,10 @@ property_expr_proper:
25382538
mto($$, $2); }
25392539
// requires sequence_expr on the LHS
25402540
| property_expr cycle_delay_range sequence_expr %prec "##"
2541-
{ init($$, ID_sva_sequence_concatenation);
2542-
mto($$, $1);
2543-
stack_expr($2).operands().insert(stack_expr($2).operands().begin(), nil_exprt());
2544-
mto($2, $3);
2545-
mto($$, $2); }
2541+
{ $$=$2;
2542+
// preserve the operand ordering as in the source code
2543+
stack_expr($$).operands().insert(stack_expr($1).operands().begin(), stack_expr($1));
2544+
mto($$, $3); }
25462545
// requires sequence_expr on the LHS
25472546
| '(' property_expr_proper ')' sequence_abbrev
25482547
{ $$ = $4;
@@ -2646,11 +2645,10 @@ sequence_expr_proper:
26462645
stack_expr($$).operands().insert(stack_expr($$).operands().begin(), nil_exprt());
26472646
mto($$, $2); }
26482647
| sequence_expr cycle_delay_range sequence_expr %prec "##"
2649-
{ init($$, ID_sva_sequence_concatenation);
2650-
mto($$, $1);
2651-
stack_expr($2).operands().insert(stack_expr($2).operands().begin(), nil_exprt());
2652-
mto($2, $3);
2653-
mto($$, $2); }
2648+
{ $$=$2;
2649+
// preserve the operand ordering as in the source code
2650+
stack_expr($$).operands().insert(stack_expr($1).operands().begin(), stack_expr($1));
2651+
mto($$, $3); }
26542652
| '(' sequence_expr_proper ')'
26552653
{ $$ = $2; }
26562654
| '(' sequence_expr_proper ')' sequence_abbrev

‎src/verilog/sva_expr.cpp

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -92,10 +92,8 @@ exprt sva_sequence_repetition_star_exprt::lower() const
9292

9393
for(; n >= 2; --n)
9494
{
95-
auto cycle_delay =
96-
sva_cycle_delay_exprt{from_integer(1, integer_typet{}), op()};
97-
result = sva_sequence_concatenation_exprt{
98-
std::move(result), std::move(cycle_delay)};
95+
result = sva_cycle_delay_exprt{
96+
std::move(result), from_integer(1, integer_typet{}), nil_exprt{}, op()};
9997
}
10098

10199
return result;

0 commit comments

Comments
 (0)