Skip to content

Commit cb93af5

Browse files
tautschnigtautschnig
authored
Merge pull request #1116 from diffblue/extract-sva-sequence-match
extract `sva_sequence_matcht`
2 parents 0ef4d02 + eab9810 commit cb93af5

File tree

4 files changed

+184
-147
lines changed

4 files changed

+184
-147
lines changed

‎src/temporal-logic/Makefile‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2,6 +2,7 @@ SRC = ctl.cpp \
22
ltl.cpp \
33
nnf.cpp \
44
normalize_property.cpp \
5+
sva_sequence_match.cpp \
56
sva_to_ltl.cpp \
67
temporal_logic.cpp \
78
trivial_sva.cpp \

‎src/temporal-logic/sva_sequence_match.cpp‎

Lines changed: 122 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,122 @@
1+
/*******************************************************************\
2+
3+
Module: SVA Sequence Matches
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#include "sva_sequence_match.h"
10+
11+
#include <util/arith_tools.h>
12+
#include <util/std_expr.h>
13+
14+
#include <verilog/sva_expr.h>
15+
16+
sva_sequence_matcht sva_sequence_matcht::true_match(const mp_integer &n)
17+
{
18+
sva_sequence_matcht result;
19+
for(mp_integer i; i < n; ++i)
20+
result.cond_vector.push_back(true_exprt{});
21+
return result;
22+
}
23+
24+
// nonoverlapping concatenation
25+
sva_sequence_matcht concat(sva_sequence_matcht a, const sva_sequence_matcht &b)
26+
{
27+
a.cond_vector.insert(
28+
a.cond_vector.end(), b.cond_vector.begin(), b.cond_vector.end());
29+
return a;
30+
}
31+
32+
// overlapping concatenation
33+
sva_sequence_matcht
34+
overlapping_concat(sva_sequence_matcht a, sva_sequence_matcht b)
35+
{
36+
PRECONDITION(!a.empty_match());
37+
PRECONDITION(!b.empty_match());
38+
auto a_last = a.cond_vector.back();
39+
a.cond_vector.pop_back();
40+
b.cond_vector.front() = conjunction({a_last, b.cond_vector.front()});
41+
return concat(std::move(a), b);
42+
}
43+
44+
std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
45+
{
46+
if(sequence.id() == ID_sva_boolean)
47+
{
48+
// atomic proposition
49+
return {sva_sequence_matcht{to_sva_boolean_expr(sequence).op()}};
50+
}
51+
else if(sequence.id() == ID_sva_sequence_concatenation)
52+
{
53+
auto &concatenation = to_sva_sequence_concatenation_expr(sequence);
54+
auto matches_lhs = LTL_sequence_matches(concatenation.lhs());
55+
auto matches_rhs = LTL_sequence_matches(concatenation.rhs());
56+
57+
if(matches_lhs.empty() || matches_rhs.empty())
58+
return {};
59+
60+
std::vector<sva_sequence_matcht> result;
61+
62+
// cross product
63+
for(auto &match_lhs : matches_lhs)
64+
for(auto &match_rhs : matches_rhs)
65+
{
66+
// Sequence concatenation is overlapping
67+
auto new_match = overlapping_concat(match_lhs, match_rhs);
68+
CHECK_RETURN(
69+
new_match.length() == match_lhs.length() + match_rhs.length() - 1);
70+
result.push_back(std::move(new_match));
71+
}
72+
return result;
73+
}
74+
else if(sequence.id() == ID_sva_cycle_delay)
75+
{
76+
auto &delay = to_sva_cycle_delay_expr(sequence);
77+
auto matches = LTL_sequence_matches(delay.op());
78+
auto from_int = numeric_cast_v<mp_integer>(delay.from());
79+
80+
if(matches.empty())
81+
return {};
82+
83+
if(delay.to().is_nil())
84+
{
85+
// delay as instructed
86+
auto delay_sequence = sva_sequence_matcht::true_match(from_int);
87+
88+
for(auto &match : matches)
89+
match = concat(delay_sequence, match);
90+
91+
return matches;
92+
}
93+
else if(delay.to().id() == ID_infinity)
94+
{
95+
return {}; // can't encode
96+
}
97+
else if(delay.to().is_constant())
98+
{
99+
auto to_int = numeric_cast_v<mp_integer>(to_constant_expr(delay.to()));
100+
std::vector<sva_sequence_matcht> new_matches;
101+
102+
for(mp_integer i = from_int; i <= to_int; ++i)
103+
{
104+
// delay as instructed
105+
auto delay_sequence = sva_sequence_matcht::true_match(i);
106+
107+
for(const auto &match : matches)
108+
{
109+
new_matches.push_back(concat(delay_sequence, match));
110+
}
111+
}
112+
113+
return new_matches;
114+
}
115+
else
116+
return {};
117+
}
118+
else
119+
{
120+
return {}; // unsupported
121+
}
122+
}

‎src/temporal-logic/sva_sequence_match.h‎

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
/*******************************************************************\
2+
3+
Module: SVA Sequence Matches
4+
5+
Author: Daniel Kroening, [email protected]
6+
7+
\*******************************************************************/
8+
9+
#ifndef CPROVER_TEMPORAL_LOGICS_SVA_SEQUENCE_MATCH_H
10+
#define CPROVER_TEMPORAL_LOGICS_SVA_SEQUENCE_MATCH_H
11+
12+
#include <util/expr.h>
13+
#include <util/mp_arith.h>
14+
15+
// A sequence of match conditions for potential matches of SVA
16+
// sequence expressions.
17+
struct sva_sequence_matcht
18+
{
19+
// the empty match
20+
sva_sequence_matcht()
21+
{
22+
}
23+
24+
// a match of length 1
25+
explicit sva_sequence_matcht(exprt __cond) : cond_vector{1, std::move(__cond)}
26+
{
27+
}
28+
29+
std::vector<exprt> cond_vector;
30+
31+
std::size_t length()
32+
{
33+
return cond_vector.size();
34+
}
35+
36+
bool empty_match() const
37+
{
38+
return cond_vector.empty();
39+
}
40+
41+
// generate true ##1 ... ##1 true with length n
42+
static sva_sequence_matcht true_match(const mp_integer &n);
43+
};
44+
45+
// the set of potential matches for the given sequence expression
46+
std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &);
47+
48+
#endif // CPROVER_TEMPORAL_LOGICS_SVA_SEQUENCE_MATCH_H

‎src/temporal-logic/sva_to_ltl.cpp‎

Lines changed: 13 additions & 147 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
1111
#include <verilog/sva_expr.h>
1212

1313
#include "ltl.h"
14+
#include "sva_sequence_match.h"
1415
#include "temporal_logic.h"
1516

1617
static exprt n_Xes(mp_integer n, exprt op)
@@ -22,153 +23,18 @@ static exprt n_Xes(mp_integer n, exprt op)
2223
return n_Xes(n - 1, X_exprt{std::move(op)});
2324
}
2425

25-
// Returns a set of match conditions (given as LTL formula)
26-
struct ltl_sequence_matcht
26+
// c0 ∧ X c1 ∧ XX c2 ....
27+
static exprt ltl(const sva_sequence_matcht &match)
2728
{
28-
// the empty match
29-
ltl_sequence_matcht()
29+
exprt::operandst conjuncts;
30+
conjuncts.reserve(match.cond_vector.size());
31+
for(std::size_t i = 0; i < match.cond_vector.size(); i++)
3032
{
33+
auto &c = match.cond_vector[i];
34+
if(!c.is_true())
35+
conjuncts.push_back(n_Xes(i, c));
3136
}
32-
33-
// a match of length 1
34-
explicit ltl_sequence_matcht(exprt __cond) : cond_vector{1, std::move(__cond)}
35-
{
36-
}
37-
38-
std::vector<exprt> cond_vector;
39-
40-
std::size_t length()
41-
{
42-
return cond_vector.size();
43-
}
44-
45-
bool empty_match() const
46-
{
47-
return cond_vector.empty();
48-
}
49-
50-
// c0 ∧ X c1 ∧ XX c2 ....
51-
exprt cond_expr() const
52-
{
53-
exprt::operandst conjuncts;
54-
conjuncts.reserve(cond_vector.size());
55-
for(std::size_t i = 0; i < cond_vector.size(); i++)
56-
{
57-
auto &c = cond_vector[i];
58-
if(!c.is_true())
59-
conjuncts.push_back(n_Xes(i, c));
60-
}
61-
return conjunction(conjuncts);
62-
}
63-
64-
// generate true ##1 ... ##1 true with length n
65-
static ltl_sequence_matcht true_match(const mp_integer &n)
66-
{
67-
ltl_sequence_matcht result;
68-
for(mp_integer i; i < n; ++i)
69-
result.cond_vector.push_back(true_exprt{});
70-
return result;
71-
}
72-
};
73-
74-
// nonoverlapping concatenation
75-
ltl_sequence_matcht concat(ltl_sequence_matcht a, const ltl_sequence_matcht &b)
76-
{
77-
a.cond_vector.insert(
78-
a.cond_vector.end(), b.cond_vector.begin(), b.cond_vector.end());
79-
return a;
80-
}
81-
82-
// overlapping concatenation
83-
ltl_sequence_matcht
84-
overlapping_concat(ltl_sequence_matcht a, ltl_sequence_matcht b)
85-
{
86-
PRECONDITION(!a.empty_match());
87-
PRECONDITION(!b.empty_match());
88-
auto a_last = a.cond_vector.back();
89-
a.cond_vector.pop_back();
90-
b.cond_vector.front() = conjunction({a_last, b.cond_vector.front()});
91-
return concat(std::move(a), b);
92-
}
93-
94-
std::vector<ltl_sequence_matcht> LTL_sequence_matches(const exprt &sequence)
95-
{
96-
if(sequence.id() == ID_sva_boolean)
97-
{
98-
// atomic proposition
99-
return {ltl_sequence_matcht{to_sva_boolean_expr(sequence).op()}};
100-
}
101-
else if(sequence.id() == ID_sva_sequence_concatenation)
102-
{
103-
auto &concatenation = to_sva_sequence_concatenation_expr(sequence);
104-
auto matches_lhs = LTL_sequence_matches(concatenation.lhs());
105-
auto matches_rhs = LTL_sequence_matches(concatenation.rhs());
106-
107-
if(matches_lhs.empty() || matches_rhs.empty())
108-
return {};
109-
110-
std::vector<ltl_sequence_matcht> result;
111-
112-
// cross product
113-
for(auto &match_lhs : matches_lhs)
114-
for(auto &match_rhs : matches_rhs)
115-
{
116-
// Sequence concatenation is overlapping
117-
auto new_match = overlapping_concat(match_lhs, match_rhs);
118-
CHECK_RETURN(
119-
new_match.length() == match_lhs.length() + match_rhs.length() - 1);
120-
result.push_back(std::move(new_match));
121-
}
122-
return result;
123-
}
124-
else if(sequence.id() == ID_sva_cycle_delay)
125-
{
126-
auto &delay = to_sva_cycle_delay_expr(sequence);
127-
auto matches = LTL_sequence_matches(delay.op());
128-
auto from_int = numeric_cast_v<mp_integer>(delay.from());
129-
130-
if(matches.empty())
131-
return {};
132-
133-
if(delay.to().is_nil())
134-
{
135-
// delay as instructed
136-
auto delay_sequence = ltl_sequence_matcht::true_match(from_int);
137-
138-
for(auto &match : matches)
139-
match = concat(delay_sequence, match);
140-
141-
return matches;
142-
}
143-
else if(delay.to().id() == ID_infinity)
144-
{
145-
return {}; // can't encode
146-
}
147-
else if(delay.to().is_constant())
148-
{
149-
auto to_int = numeric_cast_v<mp_integer>(to_constant_expr(delay.to()));
150-
std::vector<ltl_sequence_matcht> new_matches;
151-
152-
for(mp_integer i = from_int; i <= to_int; ++i)
153-
{
154-
// delay as instructed
155-
auto delay_sequence = ltl_sequence_matcht::true_match(i);
156-
157-
for(const auto &match : matches)
158-
{
159-
new_matches.push_back(concat(delay_sequence, match));
160-
}
161-
}
162-
163-
return new_matches;
164-
}
165-
else
166-
return {};
167-
}
168-
else
169-
{
170-
return {}; // unsupported
171-
}
37+
return conjunction(conjuncts);
17238
}
17339

17440
/// takes an SVA property as input, and returns an equivalent LTL property,
@@ -296,7 +162,7 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
296162
{
297163
auto delay = match.length() + (overlapped ? 0 : 1) - 1;
298164
auto delayed_property = n_Xes(delay, property_rec.value());
299-
conjuncts.push_back(implies_exprt{match.cond_expr(), delayed_property});
165+
conjuncts.push_back(implies_exprt{ltl(match), delayed_property});
300166
}
301167
}
302168

@@ -332,7 +198,7 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
332198
{
333199
auto delay = match.length() + (overlapped ? 0 : 1) - 1;
334200
auto delayed_property = n_Xes(delay, property_rec.value());
335-
disjuncts.push_back(and_exprt{match.cond_expr(), delayed_property});
201+
disjuncts.push_back(and_exprt{ltl(match), delayed_property});
336202
}
337203
}
338204

@@ -360,7 +226,7 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
360226
for(auto &match : matches)
361227
{
362228
if(!match.empty_match())
363-
disjuncts.push_back(match.cond_expr());
229+
disjuncts.push_back(ltl(match));
364230
}
365231

366232
return disjunction(disjuncts);

0 commit comments

Comments
 (0)