Skip to content

Commit 263aafa

Browse files
tautschnigtautschnig
authored
Merge pull request #507 from diffblue/sva_ranged_predicate_exprt
Verilog: introduce `sva_ranged_predicate_exprt`
2 parents 75aed06 + 6f69042 commit 263aafa

File tree

7 files changed

+153
-192
lines changed

7 files changed

+153
-192
lines changed

‎src/trans-word-level/instantiate_word_level.cpp

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -225,15 +225,14 @@ exprt wl_instantiatet::instantiate_rec(exprt expr, const mp_integer &t) const
225225
else if(expr.id() == ID_sva_eventually)
226226
{
227227
const auto &eventually_expr = to_sva_eventually_expr(expr);
228-
const auto &range = eventually_expr.range();
229228
const auto &op = eventually_expr.op();
230229

231230
mp_integer lower;
232-
if(to_integer_non_constant(range.op0(), lower))
231+
if(to_integer_non_constant(eventually_expr.lower(), lower))
233232
throw "failed to convert sva_eventually index";
234233

235234
mp_integer upper;
236-
if(to_integer_non_constant(range.op1(), upper))
235+
if(to_integer_non_constant(eventually_expr.upper(), upper))
237236
throw "failed to convert sva_eventually index";
238237

239238
// This is weak, and passes if any of the timeframes

‎src/trans-word-level/property.cpp

Lines changed: 10 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -215,25 +215,28 @@ static void property_obligations_rec(
215215
auto &phi = property_expr.id() == ID_sva_ranged_always
216216
? to_sva_ranged_always_expr(property_expr).op()
217217
: to_sva_s_always_expr(property_expr).op();
218-
auto &range = property_expr.id() == ID_sva_ranged_always
219-
? to_sva_ranged_always_expr(property_expr).range()
220-
: to_sva_s_always_expr(property_expr).range();
221-
222-
auto from_opt = numeric_cast<mp_integer>(range.op0());
218+
auto &lower = property_expr.id() == ID_sva_ranged_always
219+
? to_sva_ranged_always_expr(property_expr).lower()
220+
: to_sva_s_always_expr(property_expr).lower();
221+
auto &upper = property_expr.id() == ID_sva_ranged_always
222+
? to_sva_ranged_always_expr(property_expr).upper()
223+
: to_sva_s_always_expr(property_expr).upper();
224+
225+
auto from_opt = numeric_cast<mp_integer>(lower);
223226
if(!from_opt.has_value())
224227
throw ebmc_errort() << "failed to convert SVA always from index";
225228

226229
auto from = std::max(mp_integer{0}, *from_opt);
227230

228231
mp_integer to;
229232

230-
if(range.op1().id() == ID_infinity)
233+
if(upper.id() == ID_infinity)
231234
{
232235
to = no_timeframes - 1;
233236
}
234237
else
235238
{
236-
auto to_opt = numeric_cast<mp_integer>(range.op1());
239+
auto to_opt = numeric_cast<mp_integer>(upper);
237240
if(!to_opt.has_value())
238241
throw ebmc_errort() << "failed to convert SVA always to index";
239242
to = std::min(*to_opt, no_timeframes - 1);

‎src/verilog/expr2verilog.cpp

Lines changed: 46 additions & 31 deletions
Original file line numberDiff line numberDiff line change
@@ -384,25 +384,21 @@ Function: expr2verilogt::convert_sva
384384
385385
\*******************************************************************/
386386

387-
std::string expr2verilogt::convert_sva(
387+
std::string expr2verilogt::convert_sva_ranged_predicate(
388388
const std::string &name,
389-
const std::optional<exprt> &range,
390-
const exprt &op)
389+
const sva_ranged_predicate_exprt &src)
391390
{
392391
std::string range_str;
393392

394-
if(range.has_value())
395-
{
396-
auto &range_binary = to_binary_expr(range.value());
397-
range_str = "[" + convert(range_binary.lhs()) + ':';
398-
if(range_binary.rhs().id() == ID_infinity)
399-
range_str += "$";
400-
else
401-
range_str += convert(range_binary.rhs());
402-
range_str += "] ";
403-
}
393+
range_str = "[" + convert(src.lower()) + ':';
394+
if(src.upper().id() == ID_infinity)
395+
range_str += "$";
396+
else
397+
range_str += convert(src.upper());
398+
range_str += "] ";
404399

405400
unsigned p;
401+
auto &op = src.op();
406402
auto s = convert(op, p);
407403
if(p == 0 && op.operands().size() >= 2)
408404
s = "(" + s + ")";
@@ -411,6 +407,29 @@ std::string expr2verilogt::convert_sva(
411407

412408
/*******************************************************************\
413409
410+
Function: expr2verilogt::convert_sva_unary
411+
412+
Inputs:
413+
414+
Outputs:
415+
416+
Purpose:
417+
418+
\*******************************************************************/
419+
420+
std::string expr2verilogt::convert_sva_unary(
421+
const std::string &name,
422+
const unary_exprt &src)
423+
{
424+
unsigned p;
425+
auto s = convert(src.op(), p);
426+
if(p == 0 && src.op().operands().size() >= 2)
427+
s = "(" + s + ")";
428+
return name + " " + s;
429+
}
430+
431+
/*******************************************************************\
432+
414433
Function: expr2verilogt::convert_sva
415434
416435
Inputs:
@@ -1093,47 +1112,43 @@ std::string expr2verilogt::convert(
10931112
// not sure about precedence
10941113

10951114
else if(src.id()==ID_sva_always)
1096-
return precedence = 0, convert_sva("always", to_sva_always_expr(src).op());
1115+
return precedence = 0, convert_sva_unary("always", to_sva_always_expr(src));
10971116

10981117
else if(src.id() == ID_sva_ranged_always)
10991118
{
1100-
return precedence = 0, convert_sva(
1101-
"always",
1102-
to_sva_ranged_always_expr(src).range(),
1103-
to_sva_ranged_always_expr(src).op());
1119+
return precedence = 0, convert_sva_ranged_predicate(
1120+
"always", to_sva_ranged_always_expr(src));
11041121
}
11051122

11061123
else if(src.id() == ID_sva_s_always)
11071124
{
1108-
return precedence = 0, convert_sva(
1109-
"s_always",
1110-
to_sva_s_always_expr(src).range(),
1111-
to_sva_s_always_expr(src).op());
1125+
return precedence = 0,
1126+
convert_sva_ranged_predicate("s_always", to_sva_s_always_expr(src));
11121127
}
11131128

11141129
else if(src.id() == ID_sva_cover)
1115-
return precedence = 0, convert_sva("cover", to_sva_cover_expr(src).op());
1130+
return precedence = 0, convert_sva_unary("cover", to_sva_cover_expr(src));
11161131

11171132
else if(src.id() == ID_sva_assume)
1118-
return precedence = 0, convert_sva("assume", to_sva_assume_expr(src).op());
1133+
return precedence = 0, convert_sva_unary("assume", to_sva_assume_expr(src));
11191134

11201135
else if(src.id()==ID_sva_nexttime)
11211136
return precedence = 0,
1122-
convert_sva("nexttime", to_sva_nexttime_expr(src).op());
1137+
convert_sva_unary("nexttime", to_sva_nexttime_expr(src));
11231138

11241139
else if(src.id()==ID_sva_s_nexttime)
11251140
return precedence = 0,
1126-
convert_sva("s_nexttime", to_sva_s_nexttime_expr(src).op());
1141+
convert_sva_unary("s_nexttime", to_sva_s_nexttime_expr(src));
11271142

11281143
else if(src.id()==ID_sva_eventually)
1129-
return precedence = 0, convert_sva(
1130-
"eventually",
1131-
to_sva_eventually_expr(src).range(),
1132-
to_sva_eventually_expr(src).op());
1144+
{
1145+
return precedence = 0, convert_sva_ranged_predicate(
1146+
"eventually", to_sva_eventually_expr(src));
1147+
}
11331148

11341149
else if(src.id()==ID_sva_s_eventually)
11351150
return precedence = 0,
1136-
convert_sva("s_eventually", to_sva_s_eventually_expr(src).op());
1151+
convert_sva_unary("s_eventually", to_sva_s_eventually_expr(src));
11371152

11381153
else if(src.id()==ID_sva_until)
11391154
return precedence = 0, convert_sva(

‎src/verilog/expr2verilog_class.h

Lines changed: 5 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -12,6 +12,8 @@ Author: Daniel Kroening, [email protected]
1212
#include <util/bitvector_expr.h>
1313
#include <util/std_expr.h>
1414

15+
class sva_ranged_predicate_exprt;
16+
1517
class expr2verilogt
1618
{
1719
public:
@@ -82,15 +84,11 @@ class expr2verilogt
8284
const std::string &name,
8385
const exprt &src);
8486

85-
std::string convert_sva(
87+
std::string convert_sva_ranged_predicate(
8688
const std::string &name,
87-
const std::optional<exprt> &range,
88-
const exprt &op);
89+
const sva_ranged_predicate_exprt &);
8990

90-
std::string convert_sva(const std::string &name, const exprt &op)
91-
{
92-
return convert_sva(name, {}, op);
93-
}
91+
std::string convert_sva_unary(const std::string &name, const unary_exprt &);
9492

9593
std::string
9694
convert_sva(const exprt &lhs, const std::string &name, const exprt &rhs);

‎src/verilog/parser.y

Lines changed: 5 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -2062,16 +2062,16 @@ property_expr_proper:
20622062
| "nexttime" property_expr { init($$, "sva_nexttime"); mto($$, $2); }
20632063
| "s_nexttime" property_expr { init($$, "sva_s_nexttime"); mto($$, $2); }
20642064
| "always" '[' cycle_delay_const_range_expression ']' property_expr %prec "always"
2065-
{ init($$, ID_sva_ranged_always); mto($$, $3); mto($$, $5); }
2065+
{ init($$, ID_sva_ranged_always); swapop($$, $3); mto($$, $5); }
20662066
| "always" property_expr { init($$, "sva_always"); mto($$, $2); }
20672067
| "s_always" '[' constant_range ']' property_expr %prec "s_always"
2068-
{ init($$, ID_sva_s_always); mto($$, $3); mto($$, $5); }
2068+
{ init($$, ID_sva_s_always); swapop($$, $3); mto($$, $5); }
20692069
| "s_eventually" property_expr
2070-
{ init($$, "sva_s_eventually"); mto($$, $2); }
2070+
{ init($$, ID_sva_s_eventually); mto($$, $2); }
20712071
| "eventually" '[' constant_range ']' property_expr %prec "eventually"
2072-
{ init($$, "sva_eventually"); mto($$, $3); mto($$, $5); }
2072+
{ init($$, ID_sva_eventually); swapop($$, $3); mto($$, $5); }
20732073
| "s_eventually" '[' cycle_delay_const_range_expression ']' property_expr %prec "s_eventually"
2074-
{ init($$, "sva_s_eventually"); mto($$, $5); }
2074+
{ init($$, ID_sva_s_eventually); swapop($$, $3); mto($$, $5); }
20752075
| property_expr "until" property_expr { init($$, "sva_until"); mto($$, $1); mto($$, $3); }
20762076
| property_expr "until_with" property_expr { init($$, "sva_until_with"); mto($$, $1); mto($$, $3); }
20772077
| property_expr "s_until" property_expr { init($$, "sva_s_until"); mto($$, $1); mto($$, $3); }

0 commit comments

Comments
 (0)