Skip to content

Commit b7c57d3

Browse files
kroeningkroening
committed
rewrite SVA sequences
This adds a facility to rewrite SVA sequences using SVA or such that they do not admit empty matches. This can be used to remove the burden of handling the four cases of possible empty matches in the ##[...] operator from engines that reason about SVA sequences.
1 parent bf112c1 commit b7c57d3

File tree

10 files changed

+374
-59
lines changed

10 files changed

+374
-59
lines changed

‎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
@@ -15,6 +15,7 @@ Author: Daniel Kroening, [email protected]
1515
#include <verilog/sva_expr.h>
1616

1717
#include "ltl.h"
18+
#include "rewrite_sva_sequence.h"
1819
#include "temporal_expr.h"
1920
#include "temporal_logic.h"
2021

@@ -298,9 +299,13 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
298299
expr.id() == ID_sva_implicit_weak || expr.id() == ID_sva_implicit_strong)
299300
{
300301
PRECONDITION(mode == PROPERTY);
301-
// weak closure
302302
auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
303-
auto op_rec = rec(sequence, SVA_SEQUENCE);
303+
304+
// re-write to get rid of empty matches
305+
auto sequence_rewritten = rewrite_sva_sequence(sequence);
306+
307+
auto op_rec = rec(sequence_rewritten, SVA_SEQUENCE);
308+
// weak closure
304309
return resultt{precedencet::ATOM, '{' + op_rec.s + '}'};
305310
}
306311
else if(expr.id() == ID_sva_or)
@@ -448,7 +453,8 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
448453
}
449454
else if(repetition.is_empty_match())
450455
{
451-
throw ebmc_errort{} << "cannot convert [*0] to Buechi";
456+
// handled by rewite_sva_sequence
457+
PRECONDITION(false);
452458
}
453459
else if(repetition.is_singleton())
454460
{

‎src/temporal-logic/rewrite_sva_sequence.cpp

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

‎src/temporal-logic/rewrite_sva_sequence.h

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
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+
/// Implements the rewriting rules in 1800-2017 16.9.2.1.
15+
/// The resulting sequence expression do not admit empty matches.
16+
exprt rewrite_sva_sequence(exprt);
17+
18+
#endif // CPROVER_TEMPORAL_LOGICS_REWRITE_SVA_SEQUENCE_H

0 commit comments

Comments
 (0)