Skip to content

Commit c498099

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 8f220ab commit c498099

File tree

7 files changed

+264
-16
lines changed

7 files changed

+264
-16
lines changed

‎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/rewrite_sva_sequence.cpp

Lines changed: 218 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,218 @@
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_or)
43+
{
44+
// admits_empty((r1 or r2)) = admits_empty(r1) || admits_empty(r2)
45+
auto &or_expr = to_sva_or_expr(expr);
46+
return admits_empty(or_expr.lhs()) || admits_empty(or_expr.rhs());
47+
}
48+
else if(expr.id() == ID_sva_sequence_intersect)
49+
{
50+
// admits_empty((r1 intersect r2)) = admits_empty(r1) && admits_empty(r2)
51+
auto &intersect_expr = to_sva_sequence_intersect_expr(expr);
52+
return admits_empty(intersect_expr.lhs()) &&
53+
admits_empty(intersect_expr.rhs());
54+
}
55+
else if(expr.id() == ID_sva_sequence_first_match)
56+
{
57+
// admits_empty(first_match(r)) = admits_empty(r)
58+
auto &first_match_expr = to_sva_sequence_first_match_expr(expr);
59+
return admits_empty(first_match_expr.lhs()) &&
60+
admits_empty(first_match_expr.rhs());
61+
}
62+
else if(expr.id() == ID_sva_sequence_repetition_star)
63+
{
64+
// admits_empty(r[*0]) = 1
65+
// admits_empty(r[*1:$]) = admits_empty(r)
66+
auto &repetition_expr = to_sva_sequence_repetition_star_expr(expr);
67+
if(repetition_expr.is_range())
68+
{
69+
if(repetition_expr.from().is_zero())
70+
return true;
71+
else
72+
return admits_empty(repetition_expr.op());
73+
}
74+
else // singleton
75+
{
76+
if(repetition_expr.repetitions().is_zero())
77+
return true;
78+
else
79+
return admits_empty(repetition_expr.op());
80+
}
81+
}
82+
else if(
83+
expr.id() == ID_sva_sequence_goto_repetition ||
84+
expr.id() == ID_sva_sequence_non_consecutive_repetition)
85+
{
86+
return false;
87+
}
88+
else
89+
{
90+
DATA_INVARIANT(false, "unexpected SVA sequence: " + expr.id_string());
91+
}
92+
}
93+
94+
exprt rewrite_sva_sequence(exprt expr)
95+
{
96+
PRECONDITION(expr.type().id() == ID_verilog_sva_sequence);
97+
PRECONDITION(is_SVA_sequence_operator(expr));
98+
99+
if(expr.id() == ID_sva_cycle_delay)
100+
{
101+
// 1800-2017 16.9.2.1
102+
// - (empty ##0 seq) does not result in a match.
103+
// - (seq ##0 empty) does not result in a match.
104+
// - (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq).
105+
// - (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) `true).
106+
auto &cycle_delay_expr = to_sva_cycle_delay_expr(expr);
107+
108+
bool lhs_admits_empty = cycle_delay_expr.lhs().is_not_nil() &&
109+
admits_empty(cycle_delay_expr.lhs());
110+
111+
bool rhs_admits_empty = admits_empty(cycle_delay_expr.rhs());
112+
113+
// apply recursively to operands
114+
if(cycle_delay_expr.lhs().is_not_nil())
115+
cycle_delay_expr.lhs() = rewrite_sva_sequence(cycle_delay_expr.lhs());
116+
117+
cycle_delay_expr.rhs() = rewrite_sva_sequence(cycle_delay_expr.rhs());
118+
119+
// consider empty match cases
120+
if(!lhs_admits_empty && !rhs_admits_empty)
121+
return cycle_delay_expr;
122+
123+
if(lhs_admits_empty)
124+
{
125+
if(cycle_delay_expr.is_range())
126+
{
127+
mp_integer from_int =
128+
numeric_cast_v<mp_integer>(cycle_delay_expr.from());
129+
DATA_INVARIANT(from_int >= 0, "delay must not be negative");
130+
abort();
131+
}
132+
else // singleton
133+
{
134+
mp_integer delay_int =
135+
numeric_cast_v<mp_integer>(cycle_delay_expr.from());
136+
DATA_INVARIANT(delay_int >= 0, "delay must not be negative");
137+
138+
// lhs ##0 rhs
139+
if(delay_int == 0)
140+
return cycle_delay_expr;
141+
else
142+
{
143+
// (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq).
144+
auto delay =
145+
from_integer(delay_int - 1, cycle_delay_expr.from().type());
146+
auto empty_match_case =
147+
sva_cycle_delay_exprt{delay, cycle_delay_expr.rhs()};
148+
return sva_or_exprt{empty_match_case, cycle_delay_expr, expr.type()};
149+
}
150+
}
151+
}
152+
else if(rhs_admits_empty)
153+
{
154+
if(cycle_delay_expr.is_range())
155+
{
156+
mp_integer from_int =
157+
numeric_cast_v<mp_integer>(cycle_delay_expr.from());
158+
DATA_INVARIANT(from_int >= 0, "delay must not be negative");
159+
abort();
160+
}
161+
else
162+
{
163+
mp_integer delay_int =
164+
numeric_cast_v<mp_integer>(cycle_delay_expr.from());
165+
DATA_INVARIANT(delay_int >= 0, "delay must not be negative");
166+
167+
// lhs ##0 rhs
168+
if(delay_int == 0)
169+
return cycle_delay_expr;
170+
else
171+
{
172+
// (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) `true).
173+
auto delay =
174+
from_integer(delay_int - 1, cycle_delay_expr.from().type());
175+
auto empty_match_case = sva_cycle_delay_exprt{
176+
cycle_delay_expr.lhs(),
177+
delay,
178+
nil_exprt{},
179+
sva_boolean_exprt{true_exprt{}, expr.type()}};
180+
return sva_or_exprt{empty_match_case, cycle_delay_expr, expr.type()};
181+
}
182+
}
183+
}
184+
else // neither lhs nor rhs admit an empty match
185+
return cycle_delay_expr;
186+
}
187+
else if(expr.id() == ID_sva_sequence_repetition_star)
188+
{
189+
auto &repetition_expr = to_sva_sequence_repetition_star_expr(expr);
190+
repetition_expr.op() = rewrite_sva_sequence(repetition_expr.op());
191+
return repetition_expr;
192+
}
193+
else if(
194+
expr.id() == ID_sva_or || expr.id() == ID_sva_and ||
195+
expr.id() == ID_sva_sequence_intersect ||
196+
expr.id() == ID_sva_sequence_first_match ||
197+
expr.id() == ID_sva_sequence_repetition_plus)
198+
{
199+
for(auto &op : expr.operands())
200+
op = rewrite_sva_sequence(op);
201+
return expr;
202+
}
203+
else if(
204+
expr.id() == ID_sva_sequence_goto_repetition ||
205+
expr.id() == ID_sva_sequence_non_consecutive_repetition)
206+
{
207+
// these take a Boolean as argument, not a sequence
208+
return expr;
209+
}
210+
else if(expr.id() == ID_sva_boolean)
211+
{
212+
return expr;
213+
}
214+
else
215+
{
216+
DATA_INVARIANT(false, "unexpected SVA sequence: " + expr.id_string());
217+
}
218+
}

‎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

‎src/temporal-logic/sva_sequence_match.cpp

Lines changed: 17 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -13,6 +13,8 @@ Author: Daniel Kroening, [email protected]
1313

1414
#include <verilog/sva_expr.h>
1515

16+
#include "rewrite_sva_sequence.h"
17+
1618
sva_sequence_matcht sva_sequence_matcht::true_match(const mp_integer &n)
1719
{
1820
sva_sequence_matcht result;
@@ -51,7 +53,7 @@ overlapping_concat(sva_sequence_matcht a, sva_sequence_matcht b)
5153
return concat(std::move(a), b);
5254
}
5355

54-
std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
56+
std::vector<sva_sequence_matcht> sva_sequence_matches_rec(const exprt &sequence)
5557
{
5658
if(sequence.id() == ID_sva_boolean)
5759
{
@@ -61,8 +63,8 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
6163
else if(sequence.id() == ID_sva_sequence_concatenation)
6264
{
6365
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+
auto matches_lhs = sva_sequence_matches_rec(concatenation.lhs());
67+
auto matches_rhs = sva_sequence_matches_rec(concatenation.rhs());
6668

6769
std::vector<sva_sequence_matcht> result;
6870

@@ -81,7 +83,7 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
8183
else if(sequence.id() == ID_sva_sequence_repetition_star) // [*n], [*n:m]
8284
{
8385
auto &repetition = to_sva_sequence_repetition_star_expr(sequence);
84-
auto matches_op = LTL_sequence_matches(repetition.op());
86+
auto matches_op = sva_sequence_matches_rec(repetition.op());
8587

8688
std::vector<sva_sequence_matcht> result;
8789

@@ -119,7 +121,7 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
119121
else if(sequence.id() == ID_sva_cycle_delay)
120122
{
121123
auto &delay = to_sva_cycle_delay_expr(sequence);
122-
auto matches = LTL_sequence_matches(delay.op());
124+
auto matches = sva_sequence_matches_rec(delay.op());
123125
auto from_int = numeric_cast_v<mp_integer>(delay.from());
124126

125127
if(!delay.is_range())
@@ -163,8 +165,8 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
163165
// 3. The end time of the composite sequence is
164166
// the end time of the operand sequence that completes last.
165167
auto &and_expr = to_sva_and_expr(sequence);
166-
auto matches_lhs = LTL_sequence_matches(and_expr.lhs());
167-
auto matches_rhs = LTL_sequence_matches(and_expr.rhs());
168+
auto matches_lhs = sva_sequence_matches_rec(and_expr.lhs());
169+
auto matches_rhs = sva_sequence_matches_rec(and_expr.rhs());
168170

169171
std::vector<sva_sequence_matcht> result;
170172

@@ -200,7 +202,7 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
200202

201203
for(auto &op : to_sva_or_expr(sequence).operands())
202204
{
203-
auto op_matches = LTL_sequence_matches(op);
205+
auto op_matches = sva_sequence_matches_rec(op);
204206
if(op_matches.empty())
205207
throw sva_sequence_match_unsupportedt{sequence}; // not supported
206208
for(auto &match : op_matches)
@@ -214,3 +216,10 @@ std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
214216
throw sva_sequence_match_unsupportedt{sequence}; // not supported
215217
}
216218
}
219+
220+
std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
221+
{
222+
// rewrite, then do recursion
223+
auto rewritten = rewrite_sva_sequence(sequence);
224+
return sva_sequence_matches_rec(rewritten);
225+
}

‎src/temporal-logic/temporal_logic.cpp

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -113,7 +113,7 @@ bool is_SVA_sequence_operator(const exprt &expr)
113113
id == ID_sva_sequence_goto_repetition ||
114114
id == ID_sva_sequence_non_consecutive_repetition ||
115115
id == ID_sva_sequence_repetition_star ||
116-
id == ID_sva_sequence_repetition_plus;
116+
id == ID_sva_sequence_repetition_plus || id == ID_sva_boolean;
117117
}
118118

119119
bool is_SVA_operator(const exprt &expr)

‎src/verilog/sva_expr.cpp

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -120,7 +120,9 @@ exprt sva_sequence_repetition_star_exprt::lower() const
120120
{
121121
auto n_expr = from_integer(n, integer_typet{});
122122
result = sva_or_exprt{
123-
std::move(result), sva_sequence_repetition_star_exprt{op(), n_expr}};
123+
std::move(result),
124+
sva_sequence_repetition_star_exprt{op(), n_expr},
125+
verilog_sva_sequence_typet{}};
124126
}
125127

126128
return result;

‎src/verilog/sva_expr.h

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -838,11 +838,11 @@ static inline sva_not_exprt &to_sva_not_expr(exprt &expr)
838838
return static_cast<sva_not_exprt &>(expr);
839839
}
840840

841-
class sva_and_exprt : public binary_predicate_exprt
841+
class sva_and_exprt : public binary_exprt
842842
{
843843
public:
844-
explicit sva_and_exprt(exprt op0, exprt op1)
845-
: binary_predicate_exprt(std::move(op0), ID_sva_and, std::move(op1))
844+
explicit sva_and_exprt(exprt op0, exprt op1, typet type)
845+
: binary_exprt(std::move(op0), ID_sva_and, std::move(op1), std::move(type))
846846
{
847847
}
848848
};
@@ -936,11 +936,11 @@ static inline sva_implies_exprt &to_sva_implies_expr(exprt &expr)
936936
return static_cast<sva_implies_exprt &>(expr);
937937
}
938938

939-
class sva_or_exprt : public binary_predicate_exprt
939+
class sva_or_exprt : public binary_exprt
940940
{
941941
public:
942-
explicit sva_or_exprt(exprt op0, exprt op1)
943-
: binary_predicate_exprt(std::move(op0), ID_sva_or, std::move(op1))
942+
explicit sva_or_exprt(exprt op0, exprt op1, typet type)
943+
: binary_exprt(std::move(op0), ID_sva_or, std::move(op1), std::move(type))
944944
{
945945
}
946946
};

0 commit comments

Comments
 (0)