Skip to content

Commit f20c412

Browse files
kroeningkroening
authored
Merge pull request #1090 from diffblue/sva_sequence_repetition
use `sva_sequence_repetition_exprt` for `[*]` and `[+]`
2 parents 86f6cd1 + 1f6926e commit f20c412

File tree

9 files changed

+215
-95
lines changed

9 files changed

+215
-95
lines changed

‎regression/verilog/SVA/sequence_repetition2.desc‎

Lines changed: 9 additions & 9 deletions
Original file line numberDiff line numberDiff line change
@@ -1,15 +1,15 @@
11
CORE
22
sequence_repetition2.sv
33
--bound 10
4-
^\[main\.p0\] main\.x == 0\[\*\]: PROVED up to bound 10$
5-
^\[main\.p1\] main\.x == 1\[\*\]: PROVED up to bound 10$
6-
^\[main\.p2\] \(main\.x == 0\[\+\]\) #=# main\.x == 1: PROVED up to bound 10$
7-
^\[main\.p3\] main\.x == 0\[\+\]: PROVED up to bound 10$
8-
^\[main\.p4\] main\.half_x == 0\[\*\]: PROVED up to bound 10$
9-
^\[main\.p5\] 0\[\*\]: PROVED up to bound 10$
10-
^\[main\.p6\] main\.x == 1\[\+\]: REFUTED$
11-
^\[main\.p7\] \(main\.x == 0\[\+\]\) #-# main\.x == 1: REFUTED$
12-
^\[main\.p8\] 0\[\+\]: REFUTED$
4+
^\[main\.p0\] main\.x == 0 \[\*\]: PROVED up to bound 10$
5+
^\[main\.p1\] main\.x == 1 \[\*\]: PROVED up to bound 10$
6+
^\[main\.p2\] \(main\.x == 0 \[\+\]\) #=# main\.x == 1: PROVED up to bound 10$
7+
^\[main\.p3\] main\.x == 0 \[\+\]: PROVED up to bound 10$
8+
^\[main\.p4\] main\.half_x == 0 \[\*\]: PROVED up to bound 10$
9+
^\[main\.p5\] 0 \[\*\]: PROVED up to bound 10$
10+
^\[main\.p6\] main\.x == 1 \[\+\]: REFUTED$
11+
^\[main\.p7\] \(main\.x == 0 \[\+\]\) #-# main\.x == 1: REFUTED$
12+
^\[main\.p8\] 0 \[\+\]: REFUTED$
1313
^EXIT=10$
1414
^SIGNAL=0$
1515
--

‎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_star)
6060
IREP_ID_ONE(sva_cycle_delay_plus)
6161
IREP_ID_ONE(sva_disable_iff)
6262
IREP_ID_ONE(sva_sequence_concatenation)
63-
IREP_ID_ONE(sva_sequence_consecutive_repetition)
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/temporal_logic.cpp‎

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -111,7 +111,6 @@ bool is_SVA_sequence_operator(const exprt &expr)
111111
id == ID_sva_sequence_intersect || id == ID_sva_sequence_first_match ||
112112
id == ID_sva_sequence_throughout || id == ID_sva_sequence_within ||
113113
id == ID_sva_sequence_goto_repetition ||
114-
id == ID_sva_sequence_consecutive_repetition ||
115114
id == ID_sva_sequence_non_consecutive_repetition ||
116115
id == ID_sva_sequence_repetition_star ||
117116
id == ID_sva_sequence_repetition_plus;

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

Lines changed: 39 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -364,42 +364,52 @@ sequence_matchest instantiate_sequence(
364364

365365
return result;
366366
}
367-
else if(expr.id() == ID_sva_sequence_consecutive_repetition) // [*...]
367+
else if(expr.id() == ID_sva_sequence_repetition_star) // [*...]
368368
{
369-
// x[*n] is syntactic sugar for x ##1 ... ##1 x, with n repetitions
370-
auto &repetition = to_sva_sequence_consecutive_repetition_expr(expr);
371-
return instantiate_sequence(
372-
repetition.lower(), semantics, t, no_timeframes);
373-
}
374-
else if(
375-
expr.id() == ID_sva_sequence_repetition_plus ||
376-
expr.id() == ID_sva_sequence_repetition_star)
377-
{
378-
// x[+] and x[*]
379-
auto &op = to_unary_expr(expr).op();
369+
auto &repetition = to_sva_sequence_repetition_star_expr(expr);
370+
if(repetition.is_unbounded() && repetition.repetitions_given())
371+
{
372+
// [*x:$]
373+
auto from = numeric_cast_v<mp_integer>(repetition.from());
374+
auto &op = repetition.op();
380375

381-
// Is x a sequence or a state predicate?
382-
if(is_SVA_sequence_operator(op))
383-
PRECONDITION(false); // no support
376+
// Is op a sequence or a state predicate?
377+
if(is_SVA_sequence_operator(op))
378+
PRECONDITION(false); // no support
384379

385-
sequence_matchest result;
380+
sequence_matchest result;
386381

387-
// we incrementally add conjuncts to the condition
388-
exprt::operandst conjuncts;
382+
// we incrementally add conjuncts to the condition
383+
exprt::operandst conjuncts;
389384

390-
for(mp_integer u = t; u < no_timeframes; ++u)
391-
{
392-
// does x hold in state u?
393-
auto cond_u = instantiate(op, u, no_timeframes);
394-
conjuncts.push_back(cond_u);
395-
result.push_back({u, conjunction(conjuncts)});
396-
}
385+
for(mp_integer u = t; u < no_timeframes; ++u)
386+
{
387+
// does op hold in timeframe u?
388+
auto cond_u = instantiate(op, u, no_timeframes);
389+
conjuncts.push_back(cond_u);
397390

398-
// In addition to the above, x[*] allows an empty match.
399-
if(expr.id() == ID_sva_sequence_repetition_star)
400-
result.push_back({t, true_exprt{}});
391+
if(conjuncts.size() >= from)
392+
result.push_back({u, conjunction(conjuncts)});
393+
}
401394

402-
return result;
395+
// Empty match allowed?
396+
if(from == 0)
397+
result.push_back({t, true_exprt{}});
398+
399+
return result;
400+
}
401+
else
402+
{
403+
// [*], [*n], [*x:y]
404+
return instantiate_sequence(
405+
repetition.lower(), semantics, t, no_timeframes);
406+
}
407+
}
408+
else if(expr.id() == ID_sva_sequence_repetition_plus) // [+]
409+
{
410+
auto &repetition = to_sva_sequence_repetition_plus_expr(expr);
411+
return instantiate_sequence(
412+
repetition.lower(), semantics, t, no_timeframes);
403413
}
404414
else if(expr.id() == ID_sva_sequence_goto_repetition) // [->...]
405415
{

‎src/verilog/expr2verilog.cpp‎

Lines changed: 15 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -629,18 +629,21 @@ expr2verilogt::resultt expr2verilogt::convert_sva_sequence_repetition(
629629

630630
std::string dest = op_rec.s + " [" + name;
631631

632-
if(expr.is_range())
632+
if(expr.repetitions_given())
633633
{
634-
dest += convert_rec(expr.from()).s;
635-
dest += ':';
634+
if(expr.is_range())
635+
{
636+
dest += convert_rec(expr.from()).s;
637+
dest += ':';
636638

637-
if(expr.is_unbounded())
638-
dest += '$';
639+
if(expr.is_unbounded())
640+
dest += "$";
641+
else
642+
dest += convert_rec(expr.to()).s;
643+
}
639644
else
640-
dest += convert_rec(expr.to()).s;
645+
dest += convert_rec(expr.repetitions()).s;
641646
}
642-
else
643-
dest += convert_rec(expr.repetitions()).s;
644647

645648
dest += ']';
646649

@@ -1850,23 +1853,17 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
18501853
return precedence = verilog_precedencet::MIN,
18511854
convert_sva_unary("always", to_sva_always_expr(src));
18521855

1853-
else if(src.id() == ID_sva_sequence_repetition_star)
1854-
return precedence = verilog_precedencet::MIN,
1855-
convert_sva_unary(to_unary_expr(src), "[*]");
1856-
// not sure about precedence
1857-
18581856
else if(src.id() == ID_sva_sequence_repetition_plus)
1859-
return precedence = verilog_precedencet::MIN,
1860-
convert_sva_unary(to_unary_expr(src), "[+]");
1861-
// not sure about precedence
1857+
return convert_sva_sequence_repetition(
1858+
"+", to_sva_sequence_repetition_plus_expr(src));
18621859

18631860
else if(src.id() == ID_sva_sequence_non_consecutive_repetition)
18641861
return convert_sva_sequence_repetition(
18651862
"=", to_sva_sequence_non_consecutive_repetition_expr(src));
18661863

1867-
else if(src.id() == ID_sva_sequence_consecutive_repetition)
1864+
else if(src.id() == ID_sva_sequence_repetition_star)
18681865
return convert_sva_sequence_repetition(
1869-
"*", to_sva_sequence_consecutive_repetition_expr(src));
1866+
"*", to_sva_sequence_repetition_star_expr(src));
18701867

18711868
else if(src.id() == ID_sva_sequence_goto_repetition)
18721869
return convert_sva_sequence_repetition(

‎src/verilog/parser.y‎

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2690,7 +2690,7 @@ sequence_abbrev:
26902690

26912691
consecutive_repetition:
26922692
"[*" const_or_range_expression ']'
2693-
{ init($$, ID_sva_sequence_consecutive_repetition);
2693+
{ init($$, ID_sva_sequence_repetition_star);
26942694
if(stack_expr($2).id() == ID_sva_cycle_delay)
26952695
swapop($$, $2);
26962696
else
@@ -2700,9 +2700,13 @@ consecutive_repetition:
27002700
}
27012701
}
27022702
| "[*" ']'
2703-
{ init($$, ID_sva_sequence_repetition_star); }
2703+
{ init($$, ID_sva_sequence_repetition_star);
2704+
stack_expr($$).add_to_operands(nil_exprt{}, nil_exprt{});
2705+
}
27042706
| "[+" ']'
2705-
{ init($$, ID_sva_sequence_repetition_plus); }
2707+
{ init($$, ID_sva_sequence_repetition_plus);
2708+
stack_expr($$).add_to_operands(nil_exprt{}, nil_exprt{});
2709+
}
27062710
;
27072711

27082712
non_consecutive_repetition:

‎src/verilog/sva_expr.cpp‎

Lines changed: 17 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -57,12 +57,25 @@ exprt sva_case_exprt::lowering() const
5757
disjunction(disjuncts), case_items.front().result(), reduced_rec};
5858
}
5959

60-
exprt sva_sequence_consecutive_repetition_exprt::lower() const
60+
exprt sva_sequence_repetition_plus_exprt::lower() const
61+
{
62+
// [+] is the same as [*1:$]
63+
return sva_sequence_repetition_star_exprt{
64+
op(), from_integer(1, integer_typet{}), infinity_exprt{integer_typet{}}};
65+
}
66+
67+
exprt sva_sequence_repetition_star_exprt::lower() const
6168
{
6269
PRECONDITION(
6370
op().type().id() == ID_bool || op().type().id() == ID_verilog_sva_sequence);
6471

65-
if(!is_range())
72+
if(!repetitions_given())
73+
{
74+
// op[*] is the same as op[*0:$]
75+
return sva_sequence_repetition_star_exprt{
76+
op(), from_integer(0, integer_typet{}), infinity_exprt{integer_typet{}}};
77+
}
78+
else if(!is_range())
6679
{
6780
// expand x[*n] into x ##1 x ##1 ...
6881
auto n = numeric_cast_v<mp_integer>(repetitions());
@@ -94,14 +107,13 @@ exprt sva_sequence_consecutive_repetition_exprt::lower() const
94107
DATA_INVARIANT(
95108
to_int >= from_int, "number of repetitions must be interval");
96109

97-
exprt result = sva_sequence_consecutive_repetition_exprt{op(), from()};
110+
exprt result = sva_sequence_repetition_star_exprt{op(), from()};
98111

99112
for(mp_integer n = from_int + 1; n <= to_int; ++n)
100113
{
101114
auto n_expr = from_integer(n, integer_typet{});
102115
result = sva_or_exprt{
103-
std::move(result),
104-
sva_sequence_consecutive_repetition_exprt{op(), n_expr}};
116+
std::move(result), sva_sequence_repetition_star_exprt{op(), n_expr}};
105117
}
106118

107119
return result;

0 commit comments

Comments
 (0)