Skip to content

Commit b14d69d

Browse files
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 b14d69d

File tree

5 files changed

+228
-7
lines changed

5 files changed

+228
-7
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 \
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+
}
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/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)