Skip to content

Commit 6e6127d

Browse files
tautschnigtautschnig
authored
Merge pull request #1166 from diffblue/admits_empty
rewrite SVA sequences
2 parents 14416f0 + 11491fc commit 6e6127d

File tree

12 files changed

+418
-58
lines changed

12 files changed

+418
-58
lines changed

‎regression/ebmc-spot/sva-buechi/empty_sequence1.bdd.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
../../verilog/SVA/empty_sequence1.sv
3+
--buechi --bdd
4+
^\[main\.p0\] 1 \[\*0\]: REFUTED$
5+
^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: PROVED$
6+
^\[main\.p2\] main\.x == 0 ##1 \(1 \[\*0\]\): PROVED$
7+
^\[main\.p3\] \(1 \[\*0\]\) ##0 1: REFUTED$
8+
^\[main\.p4\] 1 ##0 \(1 \[\*0\]\): REFUTED$
9+
^EXIT=10$
10+
^SIGNAL=0$
11+
--
12+
^warning: ignoring
13+
--

‎regression/verilog/SVA/empty_sequence1.bdd.desc

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,13 @@
1+
CORE
2+
empty_sequence1.sv
3+
--bdd
4+
^\[main\.p0\] 1 \[\*0\]: REFUTED$
5+
^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: FAILURE: property not supported by BDD engine$
6+
^\[main\.p2\] main\.x == 0 ##1 \(1 \[\*0\]\): FAILURE: property not supported by BDD engine$
7+
^\[main\.p3\] \(1 \[\*0\]\) ##0 1: REFUTED$
8+
^\[main\.p4\] 1 ##0 \(1 \[\*0\]\): REFUTED$
9+
^EXIT=10$
10+
^SIGNAL=0$
11+
--
12+
^warning: ignoring
13+
--

‎regression/verilog/SVA/empty_sequence1.bmc.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ empty_sequence1.sv
55
^\[main\.p1\] \(1 \[\*0\]\) ##1 main\.x == 0: PROVED up to bound 5$
66
^\[main\.p2\] main\.x == 0 ##1 \(1 \[\*0\]\): PROVED up to bound 5$
77
^\[main\.p3\] \(1 \[\*0\]\) ##0 1: REFUTED$
8-
^\[main\.p4\] 1 ##0 \(1 \[\*0\]\): PROVED up to bound 5$
8+
^\[main\.p4\] 1 ##0 \(1 \[\*0\]\): REFUTED$
99
^EXIT=10$
1010
^SIGNAL=0$
1111
--

‎src/temporal-logic/Makefile

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -5,6 +5,7 @@ SRC = ctl.cpp \
55
ltl_sva_to_string.cpp \
66
nnf.cpp \
77
normalize_property.cpp \
8+
rewrite_sva_sequence.cpp \
89
sva_sequence_match.cpp \
910
sva_to_ltl.cpp \
1011
temporal_logic.cpp \

‎src/temporal-logic/ltl_sva_to_string.cpp

Lines changed: 9 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@ Author: Daniel Kroening, [email protected]
1414
#include <verilog/sva_expr.h>
1515

1616
#include "ltl.h"
17+
#include "rewrite_sva_sequence.h"
1718
#include "temporal_expr.h"
1819
#include "temporal_logic.h"
1920

@@ -297,9 +298,13 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
297298
expr.id() == ID_sva_implicit_weak || expr.id() == ID_sva_implicit_strong)
298299
{
299300
PRECONDITION(mode == PROPERTY);
300-
// weak closure
301301
auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
302-
auto op_rec = rec(sequence, SVA_SEQUENCE);
302+
303+
// re-write to get rid of empty matches
304+
auto sequence_rewritten = rewrite_sva_sequence(sequence);
305+
306+
auto op_rec = rec(sequence_rewritten, SVA_SEQUENCE);
307+
// weak closure
303308
return resultt{precedencet::ATOM, '{' + op_rec.s + '}'};
304309
}
305310
else if(expr.id() == ID_sva_or)
@@ -446,7 +451,8 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
446451
}
447452
else if(repetition.is_empty_match())
448453
{
449-
throw ltl_sva_to_string_unsupportedt{expr};
454+
// handled by rewite_sva_sequence
455+
return resultt{precedencet::ATOM, "0"};
450456
}
451457
else if(repetition.is_singleton())
452458
{

‎src/temporal-logic/rewrite_sva_sequence.cpp

Lines changed: 286 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,286 @@
1+
/*******************************************************************\
2+
3+
Module: Rewrite SVA Sequences
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "rewrite_sva_sequence.h"
10+
11+
#include <util/arith_tools.h>
12+
#include <util/mathematical_types.h>
13+
14+
#include <verilog/sva_expr.h>
15+
16+
#include "temporal_logic.h"
17+
18+
/// 1800-2017 F.4.3
19+
/// Returns true iff the given SVA sequence admits an empty match.
20+
bool admits_empty(const exprt &expr)
21+
{
22+
PRECONDITION(expr.type().id() == ID_verilog_sva_sequence);
23+
PRECONDITION(is_SVA_sequence_operator(expr));
24+
25+
if(expr.id() == ID_sva_boolean)
26+
return false; // admits_empty(b) = 0
27+
else if(expr.id() == ID_sva_cycle_delay)
28+
{
29+
auto &cycle_delay = to_sva_cycle_delay_expr(expr);
30+
31+
if(cycle_delay.from().is_zero() && !cycle_delay.is_range())
32+
{
33+
// admits_empty((r1 ##0 r2)) = 0
34+
return false;
35+
}
36+
else
37+
{
38+
// admits_empty((r1 ##1 r2)) = admits_empty(r1) && admits_empty(r2)
39+
return cycle_delay.lhs().is_not_nil() &&
40+
admits_empty(cycle_delay.lhs()) && admits_empty(cycle_delay.rhs());
41+
}
42+
}
43+
else if(expr.id() == ID_sva_cycle_delay_star)
44+
{
45+
auto &cycle_delay = to_sva_cycle_delay_star_expr(expr);
46+
47+
return cycle_delay.lhs().is_not_nil() && admits_empty(cycle_delay.lhs()) &&
48+
admits_empty(cycle_delay.rhs());
49+
}
50+
else if(expr.id() == ID_sva_cycle_delay_plus)
51+
{
52+
auto &cycle_delay = to_sva_cycle_delay_plus_expr(expr);
53+
54+
return cycle_delay.lhs().is_not_nil() && admits_empty(cycle_delay.lhs()) &&
55+
admits_empty(cycle_delay.rhs());
56+
}
57+
else if(expr.id() == ID_sva_or)
58+
{
59+
// admits_empty((r1 or r2)) = admits_empty(r1) || admits_empty(r2)
60+
auto &or_expr = to_sva_or_expr(expr);
61+
return admits_empty(or_expr.lhs()) || admits_empty(or_expr.rhs());
62+
}
63+
else if(expr.id() == ID_sva_sequence_intersect)
64+
{
65+
// admits_empty((r1 intersect r2)) = admits_empty(r1) && admits_empty(r2)
66+
auto &intersect_expr = to_sva_sequence_intersect_expr(expr);
67+
return admits_empty(intersect_expr.lhs()) &&
68+
admits_empty(intersect_expr.rhs());
69+
}
70+
else if(expr.id() == ID_sva_sequence_first_match)
71+
{
72+
// admits_empty(first_match(r)) = admits_empty(r)
73+
auto &first_match_expr = to_sva_sequence_first_match_expr(expr);
74+
return admits_empty(first_match_expr.lhs()) &&
75+
admits_empty(first_match_expr.rhs());
76+
}
77+
else if(expr.id() == ID_sva_sequence_repetition_star)
78+
{
79+
// admits_empty(r[*0]) = 1
80+
// admits_empty(r[*1:$]) = admits_empty(r)
81+
auto &repetition_expr = to_sva_sequence_repetition_star_expr(expr);
82+
if(repetition_expr.is_range())
83+
{
84+
if(repetition_expr.from().is_zero())
85+
return true;
86+
else
87+
return admits_empty(repetition_expr.op());
88+
}
89+
else // singleton
90+
{
91+
if(repetition_expr.repetitions().is_zero())
92+
return true;
93+
else
94+
return admits_empty(repetition_expr.op());
95+
}
96+
}
97+
else if(
98+
expr.id() == ID_sva_sequence_goto_repetition ||
99+
expr.id() == ID_sva_sequence_non_consecutive_repetition)
100+
{
101+
return false;
102+
}
103+
else
104+
{
105+
DATA_INVARIANT(false, "unexpected SVA sequence: " + expr.id_string());
106+
}
107+
}
108+
109+
exprt rewrite_sva_sequence(exprt expr)
110+
{
111+
PRECONDITION(expr.type().id() == ID_verilog_sva_sequence);
112+
PRECONDITION(is_SVA_sequence_operator(expr));
113+
114+
if(expr.id() == ID_sva_cycle_delay)
115+
{
116+
// 1800-2017 16.9.2.1
117+
// - (empty ##0 seq) does not result in a match.
118+
// - (seq ##0 empty) does not result in a match.
119+
// - (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq).
120+
// - (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) `true).
121+
auto &cycle_delay_expr = to_sva_cycle_delay_expr(expr);
122+
123+
bool lhs_admits_empty = cycle_delay_expr.lhs().is_not_nil() &&
124+
admits_empty(cycle_delay_expr.lhs());
125+
126+
bool rhs_admits_empty = admits_empty(cycle_delay_expr.rhs());
127+
128+
// apply recursively to operands
129+
if(cycle_delay_expr.lhs().is_not_nil())
130+
cycle_delay_expr.lhs() = rewrite_sva_sequence(cycle_delay_expr.lhs());
131+
132+
cycle_delay_expr.rhs() = rewrite_sva_sequence(cycle_delay_expr.rhs());
133+
134+
// consider empty match cases
135+
if(!lhs_admits_empty && !rhs_admits_empty)
136+
return cycle_delay_expr;
137+
138+
if(lhs_admits_empty)
139+
{
140+
if(cycle_delay_expr.is_range())
141+
{
142+
mp_integer from_int =
143+
numeric_cast_v<mp_integer>(cycle_delay_expr.from());
144+
DATA_INVARIANT(from_int >= 0, "delay must not be negative");
145+
abort();
146+
}
147+
else // singleton
148+
{
149+
mp_integer delay_int =
150+
numeric_cast_v<mp_integer>(cycle_delay_expr.from());
151+
DATA_INVARIANT(delay_int >= 0, "delay must not be negative");
152+
153+
// lhs ##0 rhs
154+
if(delay_int == 0)
155+
return cycle_delay_expr;
156+
else
157+
{
158+
// (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq).
159+
auto delay =
160+
from_integer(delay_int - 1, cycle_delay_expr.from().type());
161+
auto empty_match_case =
162+
sva_cycle_delay_exprt{delay, cycle_delay_expr.rhs()};
163+
return sva_or_exprt{empty_match_case, cycle_delay_expr, expr.type()};
164+
}
165+
}
166+
}
167+
else if(rhs_admits_empty)
168+
{
169+
if(cycle_delay_expr.is_range())
170+
{
171+
mp_integer from_int =
172+
numeric_cast_v<mp_integer>(cycle_delay_expr.from());
173+
DATA_INVARIANT(from_int >= 0, "delay must not be negative");
174+
abort();
175+
}
176+
else // singleton
177+
{
178+
mp_integer delay_int =
179+
numeric_cast_v<mp_integer>(cycle_delay_expr.from());
180+
DATA_INVARIANT(delay_int >= 0, "delay must not be negative");
181+
182+
// lhs ##0 rhs
183+
if(delay_int == 0)
184+
return cycle_delay_expr;
185+
else
186+
{
187+
// (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) `true).
188+
auto delay =
189+
from_integer(delay_int - 1, cycle_delay_expr.from().type());
190+
auto empty_match_case = sva_cycle_delay_exprt{
191+
cycle_delay_expr.lhs(),
192+
delay,
193+
nil_exprt{},
194+
sva_boolean_exprt{true_exprt{}, expr.type()}};
195+
return sva_or_exprt{empty_match_case, cycle_delay_expr, expr.type()};
196+
}
197+
}
198+
}
199+
else // neither lhs nor rhs admit an empty match
200+
return cycle_delay_expr;
201+
}
202+
else if(expr.id() == ID_sva_sequence_repetition_star)
203+
{
204+
auto &repetition_expr = to_sva_sequence_repetition_star_expr(expr);
205+
repetition_expr.op() = rewrite_sva_sequence(repetition_expr.op());
206+
207+
if(repetition_expr.is_empty_match())
208+
{
209+
// Empty match. Leave as is. Now denotes "no match".
210+
}
211+
else if(!repetition_expr.repetitions_given())
212+
{
213+
// f [*] g ---> f [*1:$] g
214+
repetition_expr = sva_sequence_repetition_star_exprt{
215+
repetition_expr.op(),
216+
from_integer(1, integer_typet{}),
217+
infinity_exprt{integer_typet{}}};
218+
}
219+
else if(repetition_expr.is_range() && repetition_expr.from().is_zero())
220+
{
221+
// f [*0:x] g ---> f [*1:x] g
222+
repetition_expr.from() = from_integer(1, repetition_expr.from().type());
223+
}
224+
225+
return repetition_expr;
226+
}
227+
else if(expr.id() == ID_sva_sequence_repetition_plus)
228+
{
229+
auto &repetition_expr = to_sva_sequence_repetition_plus_expr(expr);
230+
repetition_expr.op() = rewrite_sva_sequence(repetition_expr.op());
231+
return repetition_expr;
232+
}
233+
else if(
234+
expr.id() == ID_sva_or || expr.id() == ID_sva_and ||
235+
expr.id() == ID_sva_sequence_intersect ||
236+
expr.id() == ID_sva_sequence_within)
237+
{
238+
// All operands are sequences
239+
for(auto &op : expr.operands())
240+
op = rewrite_sva_sequence(op);
241+
return expr;
242+
}
243+
else if(expr.id() == ID_sva_sequence_first_match)
244+
{
245+
auto &first_match = to_sva_sequence_first_match_expr(expr);
246+
first_match.sequence() = rewrite_sva_sequence(first_match.sequence());
247+
return first_match;
248+
}
249+
else if(expr.id() == ID_sva_cycle_delay_star)
250+
{
251+
auto &cycle_delay = to_sva_cycle_delay_star_expr(expr);
252+
if(cycle_delay.lhs().is_not_nil())
253+
cycle_delay.lhs() = rewrite_sva_sequence(cycle_delay.lhs());
254+
cycle_delay.rhs() = rewrite_sva_sequence(cycle_delay.rhs());
255+
return expr;
256+
}
257+
else if(expr.id() == ID_sva_cycle_delay_plus)
258+
{
259+
auto &cycle_delay = to_sva_cycle_delay_plus_expr(expr);
260+
if(cycle_delay.lhs().is_not_nil())
261+
cycle_delay.lhs() = rewrite_sva_sequence(cycle_delay.lhs());
262+
cycle_delay.rhs() = rewrite_sva_sequence(cycle_delay.rhs());
263+
return expr;
264+
}
265+
else if(expr.id() == ID_sva_sequence_throughout)
266+
{
267+
auto &throughout = to_sva_sequence_throughout_expr(expr);
268+
throughout.sequence() = rewrite_sva_sequence(throughout.sequence());
269+
return expr;
270+
}
271+
else if(
272+
expr.id() == ID_sva_sequence_goto_repetition ||
273+
expr.id() == ID_sva_sequence_non_consecutive_repetition)
274+
{
275+
// these take a Boolean as argument, not a sequence
276+
return expr;
277+
}
278+
else if(expr.id() == ID_sva_boolean)
279+
{
280+
return expr;
281+
}
282+
else
283+
{
284+
DATA_INVARIANT(false, "unexpected SVA sequence: " + expr.id_string());
285+
}
286+
}

‎src/temporal-logic/rewrite_sva_sequence.h

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
/*******************************************************************\
2+
3+
Module: Rewrite SVA Sequences
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_TEMPORAL_LOGICS_REWRITE_SVA_SEQUENCE_H
10+
#define CPROVER_TEMPORAL_LOGICS_REWRITE_SVA_SEQUENCE_H
11+
12+
#include <util/expr.h>
13+
14+
/// 1800-2017 F.4.3
15+
/// Returns true iff the given SVA sequence admits an empty match.
16+
bool admits_empty(const exprt &);
17+
18+
/// Implements the rewriting rules in 1800-2017 16.9.2.1.
19+
/// The resulting sequence expression do not admit empty matches.
20+
exprt rewrite_sva_sequence(exprt);
21+
22+
#endif // CPROVER_TEMPORAL_LOGICS_REWRITE_SVA_SEQUENCE_H

0 commit comments

Comments
 (0)