Skip to content

Commit 7aad14c

Browse files
kroeningkroening
committed
rewrite SVA sequences
This adds two new SVA sequence expressions, X and Y. This adds a facility to rewrite SVA sequences using the new expressions such that they do not admit empty matches.
1 parent 8f220ab commit 7aad14c

File tree

7 files changed

+235
-8
lines changed

7 files changed

+235
-8
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: 200 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,200 @@
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
83+
{
84+
DATA_INVARIANT(false, "unexpected SVA sequence: " + expr.id_string());
85+
}
86+
}
87+
88+
exprt rewrite_sva_sequence(exprt expr)
89+
{
90+
PRECONDITION(expr.type().id() == ID_verilog_sva_sequence);
91+
PRECONDITION(is_SVA_sequence_operator(expr));
92+
93+
if(expr.id() == ID_sva_cycle_delay)
94+
{
95+
// 1800-2017 16.9.2.1
96+
// - (empty ##0 seq) does not result in a match.
97+
// - (seq ##0 empty) does not result in a match.
98+
// - (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq).
99+
// - (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) `true).
100+
auto &cycle_delay_expr = to_sva_cycle_delay_expr(expr);
101+
102+
bool lhs_admits_empty = cycle_delay_expr.lhs().is_not_nil() &&
103+
admits_empty(cycle_delay_expr.lhs());
104+
105+
bool rhs_admits_empty = admits_empty(cycle_delay_expr.rhs());
106+
107+
// apply recursively to operands
108+
if(cycle_delay_expr.lhs().is_not_nil())
109+
cycle_delay_expr.lhs() = rewrite_sva_sequence(cycle_delay_expr.lhs());
110+
111+
cycle_delay_expr.rhs() = rewrite_sva_sequence(cycle_delay_expr.rhs());
112+
113+
// consider empty match cases
114+
if(!lhs_admits_empty && !rhs_admits_empty)
115+
return cycle_delay_expr;
116+
117+
if(lhs_admits_empty)
118+
{
119+
if(cycle_delay_expr.is_range())
120+
{
121+
mp_integer from_int =
122+
numeric_cast_v<mp_integer>(cycle_delay_expr.from());
123+
DATA_INVARIANT(from_int >= 0, "delay must not be negative");
124+
abort();
125+
}
126+
else // singleton
127+
{
128+
mp_integer delay_int =
129+
numeric_cast_v<mp_integer>(cycle_delay_expr.from());
130+
DATA_INVARIANT(delay_int >= 0, "delay must not be negative");
131+
132+
// lhs ##0 rhs
133+
if(delay_int == 0)
134+
return cycle_delay_expr;
135+
else
136+
{
137+
// (empty ##n seq), where n is greater than 0, is equivalent to (##(n-1) seq).
138+
auto delay =
139+
from_integer(delay_int - 1, cycle_delay_expr.from().type());
140+
auto empty_match_case =
141+
sva_cycle_delay_exprt{delay, cycle_delay_expr.rhs()};
142+
return sva_or_exprt{empty_match_case, cycle_delay_expr, expr.type()};
143+
}
144+
}
145+
}
146+
else if(rhs_admits_empty)
147+
{
148+
if(cycle_delay_expr.is_range())
149+
{
150+
mp_integer from_int =
151+
numeric_cast_v<mp_integer>(cycle_delay_expr.from());
152+
DATA_INVARIANT(from_int >= 0, "delay must not be negative");
153+
abort();
154+
}
155+
else
156+
{
157+
mp_integer delay_int =
158+
numeric_cast_v<mp_integer>(cycle_delay_expr.from());
159+
DATA_INVARIANT(delay_int >= 0, "delay must not be negative");
160+
161+
// lhs ##0 rhs
162+
if(delay_int == 0)
163+
return cycle_delay_expr;
164+
else
165+
{
166+
// (seq ##n empty), where n is greater than 0, is equivalent to (seq ##(n-1) `true).
167+
auto delay =
168+
from_integer(delay_int - 1, cycle_delay_expr.from().type());
169+
auto empty_match_case = sva_cycle_delay_exprt{
170+
cycle_delay_expr.lhs(),
171+
delay,
172+
nil_exprt{},
173+
sva_boolean_exprt{true_exprt{}, expr.type()}};
174+
return sva_or_exprt{empty_match_case, cycle_delay_expr, expr.type()};
175+
}
176+
}
177+
}
178+
else // neither lhs nor rhs admit an empty match
179+
return cycle_delay_expr;
180+
}
181+
else if(
182+
expr.id() == ID_sva_or || expr.id() == ID_sva_and ||
183+
expr.id() == ID_sva_sequence_intersect ||
184+
expr.id() == ID_sva_sequence_first_match ||
185+
expr.id() == ID_sva_sequence_repetition_plus ||
186+
expr.id() == ID_sva_sequence_repetition_star)
187+
{
188+
for(auto &op : expr.operands())
189+
op = rewrite_sva_sequence(op);
190+
return expr;
191+
}
192+
else if(expr.id() == ID_sva_boolean)
193+
{
194+
return expr;
195+
}
196+
else
197+
{
198+
DATA_INVARIANT(false, "unexpected SVA sequence: " + expr.id_string());
199+
}
200+
}

‎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: 2 additions & 0 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 "temporal_logic.h"
17+
1618
sva_sequence_matcht sva_sequence_matcht::true_match(const mp_integer &n)
1719
{
1820
sva_sequence_matcht result;

‎src/temporal-logic/sva_sequence_match.h

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -9,8 +9,8 @@ Author: Daniel Kroening, [email protected]
99
#ifndef CPROVER_TEMPORAL_LOGICS_SVA_SEQUENCE_MATCH_H
1010
#define CPROVER_TEMPORAL_LOGICS_SVA_SEQUENCE_MATCH_H
1111

12-
#include <util/expr.h>
1312
#include <util/mp_arith.h>
13+
#include <util/std_expr.h>
1414

1515
// A sequence of match conditions for potential matches of SVA
1616
// sequence expressions.
@@ -68,4 +68,8 @@ class sva_sequence_match_unsupportedt
6868
/// Throws sva_sequence_match_unsupportedt when given sequence that cannot be translated.
6969
std::vector<sva_sequence_matcht> LTL_sequence_matches(const exprt &);
7070

71+
/// Implements the rewriting rules in 1800-2017 16.9.2.1.
72+
/// The resulting sequence expression do not admit empty matches.
73+
exprt rewrite_sva_empty_match(const exprt &);
74+
7175
#endif // CPROVER_TEMPORAL_LOGICS_SVA_SEQUENCE_MATCH_H

‎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)