Skip to content

Commit 8f220ab

Browse files
kroeningkroening
authored
Merge pull request #1160 from diffblue/sva-cycle-delay-expr
add (optional) lhs to SVA cycle delay operator
2 parents ddeb32d + 749da3b commit 8f220ab

File tree

9 files changed

+213
-92
lines changed

9 files changed

+213
-92
lines changed

‎src/temporal-logic/ltl_sva_to_string.cpp‎

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -422,12 +422,16 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
422422
else if(expr.id() == ID_sva_cycle_delay_star) // ##[*] something
423423
{
424424
PRECONDITION(mode == SVA_SEQUENCE);
425-
return suffix("[*]", to_sva_cycle_delay_star_expr(expr), mode);
425+
auto new_expr = unary_exprt{
426+
ID_sva_cycle_delay_star, to_sva_cycle_delay_star_expr(expr).rhs()};
427+
return suffix("[*]", new_expr, mode);
426428
}
427429
else if(expr.id() == ID_sva_cycle_delay_plus) // ##[+] something
428430
{
429431
PRECONDITION(mode == SVA_SEQUENCE);
430-
return suffix("[+]", to_sva_cycle_delay_plus_expr(expr), mode);
432+
auto new_expr = unary_exprt{
433+
ID_sva_cycle_delay_star, to_sva_cycle_delay_plus_expr(expr).rhs()};
434+
return suffix("[+]", new_expr, mode);
431435
}
432436
else if(expr.id() == ID_if)
433437
{

‎src/verilog/expr2verilog.cpp‎

Lines changed: 58 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -142,38 +142,78 @@ Function: expr2verilogt::convert_sva_cycle_delay
142142
\*******************************************************************/
143143

144144
expr2verilogt::resultt expr2verilogt::convert_sva_cycle_delay(
145-
const ternary_exprt &src,
145+
const sva_cycle_delay_exprt &src,
146146
verilog_precedencet precedence)
147147
{
148-
if(src.operands().size()!=3)
149-
return convert_norep(src);
150-
151148
std::string dest="##";
152149

153-
auto op0 = convert_rec(src.op0());
154-
auto op1 = convert_rec(src.op1());
155-
auto op2 = convert_rec(src.op2());
150+
auto from = convert_rec(src.from());
156151

157-
if(src.op1().is_nil())
158-
dest += op0.s;
159-
else if(src.op1().id()==ID_infinity)
160-
dest += '[' + op0.s + ':' + '$' + ']';
152+
if(!src.is_range())
153+
dest += from.s;
154+
else if(src.is_unbounded())
155+
dest += '[' + from.s + ':' + '$' + ']';
161156
else
162-
dest += '[' + op0.s + ':' + op1.s + ']';
157+
{
158+
auto to = convert_rec(src.to());
159+
dest += '[' + from.s + ':' + to.s + ']';
160+
}
163161

164162
dest+=' ';
165163

166-
if(precedence > op2.p)
164+
auto rhs = convert_rec(src.rhs());
165+
166+
if(precedence > rhs.p)
167167
dest += '(';
168-
dest += op2.s;
169-
if(precedence > op2.p)
168+
dest += rhs.s;
169+
if(precedence > rhs.p)
170170
dest += ')';
171171

172172
return {precedence, dest};
173173
}
174174

175175
/*******************************************************************\
176176
177+
Function: expr2verilogt::convert_sva_cycle_delay
178+
179+
Inputs:
180+
181+
Outputs:
182+
183+
Purpose:
184+
185+
\*******************************************************************/
186+
187+
expr2verilogt::resultt expr2verilogt::convert_sva_cycle_delay(
188+
const std::string &name,
189+
const binary_exprt &expr)
190+
{
191+
std::string dest;
192+
193+
if(expr.lhs().is_not_nil())
194+
{
195+
auto lhs = convert_rec(expr.lhs());
196+
if(lhs.p == verilog_precedencet::MIN)
197+
dest += "(" + lhs.s + ")";
198+
else
199+
dest += lhs.s;
200+
dest += ' ';
201+
}
202+
203+
dest += name;
204+
dest += ' ';
205+
206+
auto rhs = convert_rec(expr.rhs());
207+
if(rhs.p == verilog_precedencet::MIN)
208+
dest += "(" + rhs.s + ")";
209+
else
210+
dest += rhs.s;
211+
212+
return {verilog_precedencet::MIN, std::move(dest)};
213+
}
214+
215+
/*******************************************************************\
216+
177217
Function: expr2verilogt::convert_sva_sequence_concatenation
178218
179219
Inputs:
@@ -1784,10 +1824,10 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
17841824
convert_sva_binary("|=>", to_binary_expr(src));
17851825

17861826
else if(src.id() == ID_sva_cycle_delay_star)
1787-
return convert_sva_unary("##[*]", to_unary_expr(src));
1827+
return convert_sva_cycle_delay("##[*]", to_sva_cycle_delay_star_expr(src));
17881828

17891829
else if(src.id() == ID_sva_cycle_delay_plus)
1790-
return convert_sva_unary("##[+]", to_unary_expr(src));
1830+
return convert_sva_cycle_delay("##[+]", to_sva_cycle_delay_plus_expr(src));
17911831

17921832
else if(src.id() == ID_sva_overlapped_followed_by)
17931833
return precedence = verilog_precedencet::MIN,
@@ -1799,7 +1839,7 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
17991839

18001840
else if(src.id()==ID_sva_cycle_delay)
18011841
return convert_sva_cycle_delay(
1802-
to_ternary_expr(src), precedence = verilog_precedencet::MIN);
1842+
to_sva_cycle_delay_expr(src), precedence = verilog_precedencet::MIN);
18031843
// not sure about precedence
18041844

18051845
else if(src.id() == ID_sva_strong)

‎src/verilog/expr2verilog_class.h‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,7 @@ class sva_abort_exprt;
1616
class sva_case_exprt;
1717
class sva_if_exprt;
1818
class sva_ranged_predicate_exprt;
19+
class sva_cycle_delay_exprt;
1920
class sva_sequence_first_match_exprt;
2021
class sva_sequence_repetition_exprt;
2122

@@ -137,6 +138,9 @@ class expr2verilogt
137138

138139
resultt convert_sva_binary(const std::string &name, const binary_exprt &);
139140

141+
resultt
142+
convert_sva_cycle_delay(const std::string &symbol, const binary_exprt &);
143+
140144
resultt convert_sva_sequence_repetition(
141145
const std::string &name,
142146
const sva_sequence_repetition_exprt &);
@@ -152,7 +156,8 @@ class expr2verilogt
152156

153157
resultt convert_with(const with_exprt &, verilog_precedencet);
154158

155-
resultt convert_sva_cycle_delay(const ternary_exprt &, verilog_precedencet);
159+
resultt
160+
convert_sva_cycle_delay(const sva_cycle_delay_exprt &, verilog_precedencet);
156161

157162
resultt convert_sva_if(const sva_if_exprt &);
158163

‎src/verilog/parser.y‎

Lines changed: 16 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2533,10 +2533,16 @@ property_expr_proper:
25332533
// copy of sequence_expr, to allow and/or to be both sequence_expr and property_expr
25342534
//
25352535
| cycle_delay_range sequence_expr %prec "##"
2536-
{ $$=$1; mto($$, $2); }
2536+
{ $$=$1;
2537+
stack_expr($$).operands().insert(stack_expr($$).operands().begin(), nil_exprt());
2538+
mto($$, $2); }
25372539
// requires sequence_expr on the LHS
25382540
| property_expr cycle_delay_range sequence_expr %prec "##"
2539-
{ init($$, ID_sva_sequence_concatenation); mto($$, $1); mto($2, $3); mto($$, $2); }
2541+
{ init($$, ID_sva_sequence_concatenation);
2542+
mto($$, $1);
2543+
stack_expr($2).operands().insert(stack_expr($2).operands().begin(), nil_exprt());
2544+
mto($2, $3);
2545+
mto($$, $2); }
25402546
// requires sequence_expr on the LHS
25412547
| '(' property_expr_proper ')' sequence_abbrev
25422548
{ $$ = $4;
@@ -2636,9 +2642,15 @@ sequence_expr:
26362642

26372643
sequence_expr_proper:
26382644
cycle_delay_range sequence_expr %prec "##"
2639-
{ $$=$1; mto($$, $2); }
2645+
{ $$=$1;
2646+
stack_expr($$).operands().insert(stack_expr($$).operands().begin(), nil_exprt());
2647+
mto($$, $2); }
26402648
| sequence_expr cycle_delay_range sequence_expr %prec "##"
2641-
{ init($$, ID_sva_sequence_concatenation); mto($$, $1); mto($2, $3); mto($$, $2); }
2649+
{ init($$, ID_sva_sequence_concatenation);
2650+
mto($$, $1);
2651+
stack_expr($2).operands().insert(stack_expr($2).operands().begin(), nil_exprt());
2652+
mto($2, $3);
2653+
mto($$, $2); }
26422654
| '(' sequence_expr_proper ')'
26432655
{ $$ = $2; }
26442656
| '(' sequence_expr_proper ')' sequence_abbrev

‎src/verilog/sva_expr.cpp‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -15,18 +15,20 @@ exprt sva_cycle_delay_plus_exprt::lower() const
1515
{
1616
// same as ##[1:$]
1717
return sva_cycle_delay_exprt{
18+
lhs(),
1819
from_integer(1, integer_typet{}),
1920
exprt{ID_infinity, integer_typet{}},
20-
op()};
21+
rhs()};
2122
}
2223

2324
exprt sva_cycle_delay_star_exprt::lower() const
2425
{
2526
// same as ##[0:$]
2627
return sva_cycle_delay_exprt{
28+
lhs(),
2729
from_integer(0, integer_typet{}),
2830
exprt{ID_infinity, integer_typet{}},
29-
op()};
31+
rhs()};
3032
}
3133

3234
exprt sva_case_exprt::lower() const

‎src/verilog/sva_expr.h‎

Lines changed: 60 additions & 33 deletions
Original file line numberDiff line numberDiff line change
@@ -994,38 +994,48 @@ static inline sva_followed_by_exprt &to_sva_followed_by_expr(exprt &expr)
994994
return static_cast<sva_followed_by_exprt &>(expr);
995995
}
996996

997-
class sva_cycle_delay_exprt : public ternary_exprt
997+
/// lhs ##n rhs
998+
/// lhs ##[from:to] rhs
999+
/// lhs ##[from:$] rhs
1000+
/// The lhs is optional, indicated by 'nil'
1001+
class sva_cycle_delay_exprt : public exprt
9981002
{
9991003
public:
10001004
/// The upper bound may be $
1001-
sva_cycle_delay_exprt(constant_exprt from, exprt to, exprt op)
1002-
: ternary_exprt(
1005+
sva_cycle_delay_exprt(exprt lhs, constant_exprt from, exprt to, exprt rhs)
1006+
: exprt{
10031007
ID_sva_cycle_delay,
1004-
std::move(from),
1005-
std::move(to),
1006-
std::move(op),
1007-
verilog_sva_sequence_typet{})
1008+
verilog_sva_sequence_typet{},
1009+
{std::move(lhs), std::move(from), std::move(to), std::move(rhs)}}
10081010
{
10091011
}
10101012

1011-
sva_cycle_delay_exprt(constant_exprt cycles, exprt op)
1012-
: ternary_exprt(
1013+
sva_cycle_delay_exprt(constant_exprt cycles, exprt rhs)
1014+
: exprt{
10131015
ID_sva_cycle_delay,
1014-
std::move(cycles),
1015-
nil_exprt{},
1016-
std::move(op),
1017-
verilog_sva_sequence_typet{})
1016+
verilog_sva_sequence_typet{},
1017+
{nil_exprt{}, std::move(cycles), nil_exprt{}, std::move(rhs)}}
1018+
{
1019+
}
1020+
1021+
const exprt &lhs() const
1022+
{
1023+
return operands()[0];
1024+
}
1025+
1026+
exprt &lhs()
10181027
{
1028+
return operands()[0];
10191029
}
10201030

10211031
const constant_exprt &from() const
10221032
{
1023-
return static_cast<const constant_exprt &>(op0());
1033+
return static_cast<const constant_exprt &>(operands()[1]);
10241034
}
10251035

10261036
constant_exprt &from()
10271037
{
1028-
return static_cast<constant_exprt &>(op0());
1038+
return static_cast<constant_exprt &>(operands()[1]);
10291039
}
10301040

10311041
// May be just the singleton 'from' or
@@ -1034,39 +1044,54 @@ class sva_cycle_delay_exprt : public ternary_exprt
10341044
const constant_exprt &to() const
10351045
{
10361046
PRECONDITION(is_range() && !is_unbounded());
1037-
return static_cast<const constant_exprt &>(op1());
1047+
return static_cast<const constant_exprt &>(operands()[2]);
10381048
}
10391049

10401050
constant_exprt &to()
10411051
{
10421052
PRECONDITION(is_range() && !is_unbounded());
1043-
return static_cast<constant_exprt &>(op1());
1053+
return static_cast<constant_exprt &>(operands()[2]);
10441054
}
10451055

10461056
bool is_range() const
10471057
{
1048-
return op1().is_not_nil();
1058+
return operands()[2].is_not_nil();
10491059
}
10501060

10511061
bool is_unbounded() const
10521062
{
1053-
return op1().id() == ID_infinity;
1063+
return operands()[2].id() == ID_infinity;
10541064
}
10551065

10561066
const exprt &op() const
10571067
{
1058-
return op2();
1068+
return operands()[3];
10591069
}
10601070

10611071
exprt &op()
10621072
{
1063-
return op2();
1073+
return operands()[3];
10641074
}
10651075

1066-
protected:
1067-
using ternary_exprt::op0;
1068-
using ternary_exprt::op1;
1069-
using ternary_exprt::op2;
1076+
const exprt &rhs() const
1077+
{
1078+
return operands()[3];
1079+
}
1080+
1081+
exprt &rhs()
1082+
{
1083+
return operands()[3];
1084+
}
1085+
1086+
static void check(
1087+
const exprt &expr,
1088+
const validation_modet vm = validation_modet::INVARIANT)
1089+
{
1090+
DATA_CHECK(
1091+
vm,
1092+
expr.operands().size() == 4,
1093+
"sva_cycle_delay expression must have four operands");
1094+
}
10701095
};
10711096

10721097
static inline const sva_cycle_delay_exprt &
@@ -1084,13 +1109,14 @@ static inline sva_cycle_delay_exprt &to_sva_cycle_delay_expr(exprt &expr)
10841109
return static_cast<sva_cycle_delay_exprt &>(expr);
10851110
}
10861111

1087-
class sva_cycle_delay_plus_exprt : public unary_exprt
1112+
class sva_cycle_delay_plus_exprt : public binary_exprt
10881113
{
10891114
public:
1090-
explicit sva_cycle_delay_plus_exprt(exprt op)
1091-
: unary_exprt(
1115+
explicit sva_cycle_delay_plus_exprt(exprt __lhs, exprt __rhs)
1116+
: binary_exprt(
1117+
std::move(__lhs),
10921118
ID_sva_cycle_delay_plus,
1093-
std::move(op),
1119+
std::move(__rhs),
10941120
verilog_sva_sequence_typet{})
10951121
{
10961122
}
@@ -1115,13 +1141,14 @@ to_sva_cycle_delay_plus_expr(exprt &expr)
11151141
return static_cast<sva_cycle_delay_plus_exprt &>(expr);
11161142
}
11171143

1118-
class sva_cycle_delay_star_exprt : public unary_exprt
1144+
class sva_cycle_delay_star_exprt : public binary_exprt
11191145
{
11201146
public:
1121-
explicit sva_cycle_delay_star_exprt(exprt op)
1122-
: unary_exprt(
1147+
explicit sva_cycle_delay_star_exprt(exprt __lhs, exprt __rhs)
1148+
: binary_exprt(
1149+
std::move(__lhs),
11231150
ID_sva_cycle_delay_star,
1124-
std::move(op),
1151+
std::move(__rhs),
11251152
verilog_sva_sequence_typet{})
11261153
{
11271154
}

‎src/verilog/verilog_typecheck_expr.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -207,6 +207,7 @@ class verilog_typecheck_exprt:public verilog_typecheck_baset
207207
[[nodiscard]] exprt convert_unary_sva(unary_exprt);
208208
[[nodiscard]] exprt convert_binary_sva(binary_exprt);
209209
[[nodiscard]] exprt convert_ternary_sva(ternary_exprt);
210+
[[nodiscard]] exprt convert_other_sva(exprt);
210211

211212
static void set_default_sequence_semantics(exprt &, sva_sequence_semanticst);
212213

0 commit comments

Comments
 (0)