Skip to content

Commit 8563787

Browse files
kroeningkroening
committed
SVA: consecutive repetition
This implements SVA's [*n] sequence operator.
1 parent c12e5ff commit 8563787

File tree

12 files changed

+177
-17
lines changed

12 files changed

+177
-17
lines changed

‎regression/verilog/SVA/sequence_repetition1.desc‎

Lines changed: 6 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -1,12 +1,12 @@
11
CORE
22
sequence_repetition1.sv
33
--bound 10
4-
^\[.*\] 1 \[\*\] main\.half_x == 0: FAILURE: property not supported by BMC engine$
5-
^\[.*\] 1 \[->\] main\.half_x == 0: FAILURE: property not supported by BMC engine$
6-
^\[.*\] 1 \[=\] main\.half_x == 0: FAILURE: property not supported by BMC engine$
7-
^\[.*\] 1 \[\*\] main\.x == 0: FAILURE: property not supported by BMC engine$
8-
^\[.*\] 1 \[->\] main\.x == 0: FAILURE: property not supported by BMC engine$
9-
^\[.*\] 1 \[=\] main\.x == 0: FAILURE: property not supported by BMC engine$
4+
^\[.*\] main\.half_x == 0 \[\*2\]: PROVED up to bound 10$
5+
^\[.*\] main\.half_x == 0 \[->2\]: FAILURE: property not supported by BMC engine$
6+
^\[.*\] main\.half_x == 0 \[=2\]: FAILURE: property not supported by BMC engine$
7+
^\[.*\] main\.x == 0 \[\*2\]: REFUTED$
8+
^\[.*\] main\.x == 0 \[->2\]: FAILURE: property not supported by BMC engine$
9+
^\[.*\] main\.x == 0 \[=2\]: FAILURE: property not supported by BMC engine$
1010
^EXIT=10$
1111
^SIGNAL=0$
1212
--

‎regression/verilog/SVA/sequence_repetition3.desc‎

Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
sequence_repetition3.sv
3+
--bound 10
4+
^\[main\.p0\] \(main\.x == 0 \[\*1\]\) #=# \(main\.x == 1 \[\*1\]\): PROVED up to bound 10$
5+
^\[main\.p1\] \(main\.half_x == 0 \[\*2\]\) #=# \(main\.half_x == 1 \[\*2\]\): PROVED up to bound 10$
6+
^\[main\.p2\] main\.half_x == 0 \[\*3\]: REFUTED$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
^warning: ignoring
11+
--

‎regression/verilog/SVA/sequence_repetition3.sv‎

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module main(input clk);
2+
3+
reg [31:0] x = 0;
4+
5+
// 0 1 2 3 4 ...
6+
always_ff @(posedge clk)
7+
x<=x+1;
8+
9+
// 0 0 1 1 2 2 3 3 ...
10+
wire [31:0] half_x = x/2;
11+
12+
// should pass
13+
initial p0: assert property (x==0[*1] #=# x==1[*1]);
14+
initial p1: assert property (half_x==0[*2] #=# half_x==1[*2]);
15+
16+
// should fail
17+
initial p2: assert property (half_x==0[*3]);
18+
19+
endmodule

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

Lines changed: 0 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -138,10 +138,6 @@ bool bmc_supports_SVA_property(const exprt &expr)
138138
if(has_subexpr(expr, ID_sva_sequence_non_consecutive_repetition))
139139
return false;
140140

141-
// sva_sequence_consecutive_repetition is not supported yet
142-
if(has_subexpr(expr, ID_sva_sequence_consecutive_repetition))
143-
return false;
144-
145141
// sva_sequence_goto_repetition is not supported yet
146142
if(has_subexpr(expr, ID_sva_sequence_goto_repetition))
147143
return false;

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

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -176,6 +176,12 @@ std::vector<std::pair<mp_integer, exprt>> instantiate_sequence(
176176

177177
return result;
178178
}
179+
else if(expr.id() == ID_sva_sequence_consecutive_repetition)
180+
{
181+
// x[*n] is syntactic sugar for x ##1 ... ##1 x, with n repetitions
182+
auto &repetition = to_sva_sequence_consecutive_repetition_expr(expr);
183+
return instantiate_sequence(repetition.lower(), t, no_timeframes);
184+
}
179185
else
180186
{
181187
// not a sequence, evaluate as state predicate

‎src/verilog/expr2verilog.cpp‎

Lines changed: 28 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -502,6 +502,31 @@ expr2verilogt::resultt expr2verilogt::convert_sva_binary(
502502

503503
/*******************************************************************\
504504
505+
Function: expr2verilogt::convert_sva_binary_repetition
506+
507+
Inputs:
508+
509+
Outputs:
510+
511+
Purpose:
512+
513+
\*******************************************************************/
514+
515+
expr2verilogt::resultt expr2verilogt::convert_sva_binary_repetition(
516+
const std::string &name,
517+
const binary_exprt &expr)
518+
{
519+
auto op0 = convert_rec(expr.lhs());
520+
if(op0.p == verilog_precedencet::MIN)
521+
op0.s = "(" + op0.s + ")";
522+
523+
auto op1 = convert_rec(expr.rhs());
524+
525+
return {verilog_precedencet::MIN, op0.s + " " + name + op1.s + "]"};
526+
}
527+
528+
/*******************************************************************\
529+
505530
Function: expr2verilogt::convert_sva_abort
506531
507532
Inputs:
@@ -1504,17 +1529,17 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
15041529

15051530
else if(src.id() == ID_sva_sequence_non_consecutive_repetition)
15061531
return precedence = verilog_precedencet::MIN,
1507-
convert_sva_binary("[=]", to_binary_expr(src));
1532+
convert_sva_binary_repetition("[=", to_binary_expr(src));
15081533
// not sure about precedence
15091534

15101535
else if(src.id() == ID_sva_sequence_consecutive_repetition)
15111536
return precedence = verilog_precedencet::MIN,
1512-
convert_sva_binary("[*]", to_binary_expr(src));
1537+
convert_sva_binary_repetition("[*", to_binary_expr(src));
15131538
// not sure about precedence
15141539

15151540
else if(src.id() == ID_sva_sequence_goto_repetition)
15161541
return precedence = verilog_precedencet::MIN,
1517-
convert_sva_binary("[->]", to_binary_expr(src));
1542+
convert_sva_binary_repetition("[->", to_binary_expr(src));
15181543
// not sure about precedence
15191544

15201545
else if(src.id() == ID_sva_ranged_always)

‎src/verilog/expr2verilog_class.h‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -124,6 +124,9 @@ class expr2verilogt
124124

125125
resultt convert_sva_binary(const std::string &name, const binary_exprt &);
126126

127+
resultt
128+
convert_sva_binary_repetition(const std::string &name, const binary_exprt &);
129+
127130
resultt convert_sva_abort(const std::string &name, const sva_abort_exprt &);
128131

129132
resultt

‎src/verilog/parser.y‎

Lines changed: 4 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2262,7 +2262,10 @@ expression_or_dist_brace:
22622262
sequence_expr:
22632263
expression_or_dist
22642264
| expression_or_dist boolean_abbrev
2265-
{ $$ = $2; mto($$, $1); }
2265+
{ $$ = $2;
2266+
// preserve the operand ordering as in the source code
2267+
stack_expr($$).operands().insert(stack_expr($$).operands().begin(), stack_expr($1));
2268+
}
22662269
| cycle_delay_range sequence_expr
22672270
{ $$=$1; mto($$, $2); }
22682271
| expression cycle_delay_range sequence_expr

‎src/verilog/sva_expr.cpp‎

Lines changed: 21 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -8,6 +8,9 @@ Author: Daniel Kroening, kroening@kroening.com
88

99
#include "sva_expr.h"
1010

11+
#include <util/arith_tools.h>
12+
#include <util/mathematical_types.h>
13+
1114
exprt sva_case_exprt::lowering() const
1215
{
1316
auto &case_items = this->case_items();
@@ -35,3 +38,21 @@ exprt sva_case_exprt::lowering() const
3538
return if_exprt{
3639
disjunction(disjuncts), case_items.front().result(), reduced_rec};
3740
}
41+
42+
exprt sva_sequence_consecutive_repetition_exprt::lower() const
43+
{
44+
auto n = numeric_cast_v<mp_integer>(to_constant_expr(rhs()));
45+
DATA_INVARIANT(n >= 1, "number of repetitions must be at least one");
46+
47+
exprt result = lhs();
48+
49+
for(; n >= 2; --n)
50+
{
51+
auto cycle_delay =
52+
sva_cycle_delay_exprt{from_integer(1, integer_typet{}), lhs()};
53+
result = sva_sequence_concatenation_exprt{
54+
std::move(cycle_delay), std::move(result)};
55+
}
56+
57+
return result;
58+
}

‎src/verilog/sva_expr.h‎

Lines changed: 26 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1155,4 +1155,30 @@ inline sva_case_exprt &to_sva_case_expr(exprt &expr)
11551155
return static_cast<sva_case_exprt &>(expr);
11561156
}
11571157

1158+
class sva_sequence_consecutive_repetition_exprt : public binary_predicate_exprt
1159+
{
1160+
public:
1161+
exprt lower() const;
1162+
1163+
protected:
1164+
using binary_predicate_exprt::op0;
1165+
using binary_predicate_exprt::op1;
1166+
};
1167+
1168+
inline const sva_sequence_consecutive_repetition_exprt &
1169+
to_sva_sequence_consecutive_repetition_expr(const exprt &expr)
1170+
{
1171+
PRECONDITION(expr.id() == ID_sva_sequence_consecutive_repetition);
1172+
sva_sequence_consecutive_repetition_exprt::check(expr);
1173+
return static_cast<const sva_sequence_consecutive_repetition_exprt &>(expr);
1174+
}
1175+
1176+
inline sva_sequence_consecutive_repetition_exprt &
1177+
to_sva_sequence_consecutive_repetition_expr(exprt &expr)
1178+
{
1179+
PRECONDITION(expr.id() == ID_sva_sequence_consecutive_repetition);
1180+
sva_sequence_consecutive_repetition_exprt::check(expr);
1181+
return static_cast<sva_sequence_consecutive_repetition_exprt &>(expr);
1182+
}
1183+
11581184
#endif

0 commit comments

Comments
 (0)