Skip to content

Commit 46f69a6

Browse files
kroeningkroening
committed
Verilog: ranged always and s_always properties
This adds support for always property expressions with a given range and for s_always properties.
1 parent 3e4ea73 commit 46f69a6

File tree

9 files changed

+278
-29
lines changed

9 files changed

+278
-29
lines changed

‎regression/verilog/SVA/always_with_range1.desc

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
CORE
2+
always_with_range1.sv
3+
--bound 20
4+
^\[main\.property\.1\] always \[0:9\] main\.x < 10: PROVED up to bound 20$
5+
^\[main\.property\.2\] always \[0:\$\] main\.x < 10: REFUTED$
6+
^\[main\.property\.3\] s_always \[0:9\] main\.x < 10: PROVED up to bound 20$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
^warning: ignoring
11+
--

‎regression/verilog/SVA/always_with_range1.sv

+20
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
module main;
2+
3+
reg [31:0] x;
4+
wire clk;
5+
6+
initial x=0;
7+
8+
always @(posedge clk)
9+
x<=x+1;
10+
11+
// holds owing to the range
12+
initial p0: assert property (always [0:9] x<10);
13+
14+
// unbounded, fails
15+
initial p1: assert property (always [0:$] x<10);
16+
17+
// strong variant
18+
initial p2: assert property (s_always [0:9] x<10);
19+
20+
endmodule

‎src/hw_cbmc_irep_ids.h

+2
Original file line numberDiff line numberDiff line change
@@ -16,6 +16,8 @@ IREP_ID_ONE(sva_sequence_throughout)
1616
IREP_ID_ONE(sva_sequence_concatenation)
1717
IREP_ID_ONE(sva_sequence_first_match)
1818
IREP_ID_ONE(sva_always)
19+
IREP_ID_ONE(sva_ranged_always)
20+
IREP_ID_ONE(sva_s_always)
1921
IREP_ID_ONE(sva_cover)
2022
IREP_ID_ONE(sva_nexttime)
2123
IREP_ID_ONE(sva_s_nexttime)

‎src/temporal-logic/temporal_logic.cpp

+6-5
Original file line numberDiff line numberDiff line change
@@ -17,11 +17,12 @@ bool is_temporal_operator(const exprt &expr)
1717
expr.id() == ID_A || expr.id() == ID_E || expr.id() == ID_U ||
1818
expr.id() == ID_R || expr.id() == ID_G || expr.id() == ID_F ||
1919
expr.id() == ID_X || expr.id() == ID_sva_always ||
20-
expr.id() == ID_sva_always || expr.id() == ID_sva_nexttime ||
21-
expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_until ||
22-
expr.id() == ID_sva_s_until || expr.id() == ID_sva_until_with ||
23-
expr.id() == ID_sva_s_until_with || expr.id() == ID_sva_eventually ||
24-
expr.id() == ID_sva_s_eventually || expr.id() == ID_sva_cycle_delay;
20+
expr.id() == ID_sva_always || expr.id() == ID_sva_ranged_always ||
21+
expr.id() == ID_sva_nexttime || expr.id() == ID_sva_s_nexttime ||
22+
expr.id() == ID_sva_until || expr.id() == ID_sva_s_until ||
23+
expr.id() == ID_sva_until_with || expr.id() == ID_sva_s_until_with ||
24+
expr.id() == ID_sva_eventually || expr.id() == ID_sva_s_eventually ||
25+
expr.id() == ID_sva_cycle_delay;
2526
}
2627

2728
bool has_temporal_operator(const exprt &expr)

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

+56-10
Original file line numberDiff line numberDiff line change
@@ -8,11 +8,13 @@ Author: Daniel Kroening, [email protected]
88

99
#include "property.h"
1010

11+
#include <util/arith_tools.h>
1112
#include <util/expr_iterator.h>
1213
#include <util/namespace.h>
1314
#include <util/std_expr.h>
1415
#include <util/symbol_table.h>
1516

17+
#include <ebmc/ebmc_error.h>
1618
#include <temporal-logic/temporal_expr.h>
1719
#include <temporal-logic/temporal_logic.h>
1820
#include <verilog/sva_expr.h>
@@ -56,6 +58,8 @@ bool bmc_supports_property(const exprt &expr)
5658
return bmc_supports_property(to_X_expr(expr).op());
5759
else if(expr.id() == ID_sva_always)
5860
return true;
61+
else if(expr.id() == ID_sva_ranged_always)
62+
return true;
5963
else
6064
return false;
6165
}
@@ -75,12 +79,12 @@ Function: property_obligations_rec
7579
static void property_obligations_rec(
7680
const exprt &property_expr,
7781
decision_proceduret &solver,
78-
std::size_t current,
79-
std::size_t no_timeframes,
82+
mp_integer current,
83+
mp_integer no_timeframes,
8084
const namespacet &ns,
81-
std::map<std::size_t, exprt::operandst> &obligations)
85+
std::map<mp_integer, exprt::operandst> &obligations)
8286
{
83-
PRECONDITION(current < no_timeframes);
87+
PRECONDITION(current >= 0 && current < no_timeframes);
8488

8589
if(property_expr.id() == ID_X)
8690
{
@@ -108,11 +112,51 @@ static void property_obligations_rec(
108112
PRECONDITION(false);
109113
}(property_expr);
110114

111-
for(std::size_t c = current; c < no_timeframes; c++)
115+
for(mp_integer c = current; c < no_timeframes; ++c)
112116
{
113117
property_obligations_rec(phi, solver, c, no_timeframes, ns, obligations);
114118
}
115119
}
120+
else if(
121+
property_expr.id() == ID_sva_ranged_always ||
122+
property_expr.id() == ID_sva_s_always)
123+
{
124+
auto &phi = property_expr.id() == ID_sva_ranged_always
125+
? to_sva_ranged_always_expr(property_expr).op()
126+
: to_sva_s_always_expr(property_expr).op();
127+
auto &range = property_expr.id() == ID_sva_ranged_always
128+
? to_sva_ranged_always_expr(property_expr).range()
129+
: to_sva_s_always_expr(property_expr).range();
130+
131+
mp_integer from, to;
132+
133+
auto from_opt = numeric_cast<mp_integer>(range.op0());
134+
if(!from_opt.has_value())
135+
throw ebmc_errort() << "failed to convert SVA always from index";
136+
137+
from = *from_opt;
138+
139+
if(range.op1().id() == ID_infinity)
140+
{
141+
to = no_timeframes - 1;
142+
}
143+
else
144+
{
145+
auto to_opt = numeric_cast<mp_integer>(range.op1());
146+
if(!to_opt.has_value())
147+
throw ebmc_errort() << "failed to convert SVA always to index";
148+
to = *to_opt;
149+
}
150+
151+
for(mp_integer c = from; c <= to; ++c)
152+
{
153+
if(c >= 0 && c < no_timeframes)
154+
{
155+
property_obligations_rec(
156+
phi, solver, c, no_timeframes, ns, obligations);
157+
}
158+
}
159+
}
116160
else
117161
{
118162
// current state property
@@ -133,13 +177,13 @@ Function: property_obligations
133177
134178
\*******************************************************************/
135179

136-
static std::map<std::size_t, exprt::operandst> property_obligations(
180+
static std::map<mp_integer, exprt::operandst> property_obligations(
137181
const exprt &property_expr,
138182
decision_proceduret &solver,
139-
std::size_t no_timeframes,
183+
mp_integer no_timeframes,
140184
const namespacet &ns)
141185
{
142-
std::map<std::size_t, exprt::operandst> obligations;
186+
std::map<mp_integer, exprt::operandst> obligations;
143187

144188
property_obligations_rec(
145189
property_expr, solver, 0, no_timeframes, ns, obligations);
@@ -178,8 +222,10 @@ void property(
178222
for(auto &obligation_it : obligations)
179223
{
180224
auto t = obligation_it.first;
181-
DATA_INVARIANT(t < no_timeframes, "obligation must have valid timeframe");
182-
prop_handles[t] = conjunction(obligation_it.second);
225+
DATA_INVARIANT(
226+
t >= 0 && t < no_timeframes, "obligation must have valid timeframe");
227+
auto t_int = numeric_cast_v<std::size_t>(t);
228+
prop_handles[t_int] = conjunction(obligation_it.second);
183229
}
184230
}
185231

‎src/verilog/expr2verilog.cpp

+22-2
Original file line numberDiff line numberDiff line change
@@ -394,8 +394,12 @@ std::string expr2verilogt::convert_sva(
394394
if(range.has_value())
395395
{
396396
auto &range_binary = to_binary_expr(range.value());
397-
range_str = "[" + convert(range_binary.lhs()) + ':' +
398-
convert(range_binary.rhs()) + "] ";
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 += "] ";
399403
}
400404

401405
unsigned p;
@@ -1088,6 +1092,22 @@ std::string expr2verilogt::convert(
10881092
else if(src.id()==ID_sva_always)
10891093
return precedence = 0, convert_sva("always", to_sva_always_expr(src).op());
10901094

1095+
else if(src.id() == ID_sva_ranged_always)
1096+
{
1097+
return precedence = 0, convert_sva(
1098+
"always",
1099+
to_sva_ranged_always_expr(src).range(),
1100+
to_sva_ranged_always_expr(src).op());
1101+
}
1102+
1103+
else if(src.id() == ID_sva_s_always)
1104+
{
1105+
return precedence = 0, convert_sva(
1106+
"s_always",
1107+
to_sva_s_always_expr(src).range(),
1108+
to_sva_s_always_expr(src).op());
1109+
}
1110+
10911111
else if(src.id() == ID_sva_cover)
10921112
return precedence = 0, convert_sva("cover", to_sva_cover_expr(src).op());
10931113

‎src/verilog/parser.y

+8-3
Original file line numberDiff line numberDiff line change
@@ -1965,8 +1965,11 @@ property_expr_proper:
19651965
| property_expr "|=>" property_expr { init($$, ID_sva_non_overlapped_implication); mto($$, $1); mto($$, $3); }
19661966
| "nexttime" property_expr { init($$, "sva_nexttime"); mto($$, $2); }
19671967
| "s_nexttime" property_expr { init($$, "sva_s_nexttime"); mto($$, $2); }
1968+
| "always" '[' cycle_delay_const_range_expression ']' property_expr %prec "always"
1969+
{ init($$, ID_sva_ranged_always); mto($$, $3); mto($$, $5); }
19681970
| "always" property_expr { init($$, "sva_always"); mto($$, $2); }
1969-
| "s_always" property_expr { init($$, "sva_s_always"); mto($$, $2); }
1971+
| "s_always" '[' constant_range ']' property_expr %prec "s_always"
1972+
{ init($$, ID_sva_s_always); mto($$, $3); mto($$, $5); }
19701973
| "s_eventually" property_expr
19711974
{ init($$, "sva_s_eventually"); mto($$, $2); }
19721975
| "eventually" '[' constant_range ']' property_expr %prec "eventually"
@@ -2008,8 +2011,10 @@ cycle_delay_range:
20082011
;
20092012

20102013
cycle_delay_const_range_expression:
2011-
constant_expression ':' constant_expression
2012-
| constant_expression ':' '$'
2014+
constant_expression TOK_COLON constant_expression
2015+
{ init($$, ID_sva_cycle_delay); mto($$, $1); mto($$, $3); }
2016+
| constant_expression TOK_COLON '$'
2017+
{ init($$, ID_sva_cycle_delay); mto($$, $1); stack_expr($$).add_to_operands(exprt(ID_infinity)); }
20132018
;
20142019

20152020
expression_or_dist:

‎src/verilog/sva_expr.h

+123
Original file line numberDiff line numberDiff line change
@@ -170,6 +170,129 @@ static inline sva_always_exprt &to_sva_always_expr(exprt &expr)
170170
return static_cast<sva_always_exprt &>(expr);
171171
}
172172

173+
class sva_ranged_always_exprt : public binary_predicate_exprt
174+
{
175+
public:
176+
explicit sva_ranged_always_exprt(binary_exprt range, exprt op)
177+
: binary_predicate_exprt(std::move(range), ID_sva_always, std::move(op))
178+
{
179+
}
180+
181+
// These come with a range, which is binary
182+
const binary_exprt &range() const
183+
{
184+
return static_cast<const binary_exprt &>(op0());
185+
}
186+
187+
binary_exprt &range()
188+
{
189+
return static_cast<binary_exprt &>(op0());
190+
}
191+
192+
const exprt &op() const
193+
{
194+
return op1();
195+
}
196+
197+
exprt &op()
198+
{
199+
return op1();
200+
}
201+
202+
const exprt &lhs() const = delete;
203+
exprt &lhs() = delete;
204+
const exprt &rhs() const = delete;
205+
exprt &rhs() = delete;
206+
207+
static void check(
208+
const exprt &expr,
209+
const validation_modet vm = validation_modet::INVARIANT)
210+
{
211+
binary_exprt::check(expr, vm);
212+
binary_exprt::check(to_binary_expr(expr).op0(), vm);
213+
}
214+
215+
protected:
216+
using binary_predicate_exprt::op0;
217+
using binary_predicate_exprt::op1;
218+
};
219+
220+
static inline const sva_ranged_always_exprt &
221+
to_sva_ranged_always_expr(const exprt &expr)
222+
{
223+
PRECONDITION(expr.id() == ID_sva_ranged_always);
224+
sva_ranged_always_exprt::check(expr, validation_modet::INVARIANT);
225+
return static_cast<const sva_ranged_always_exprt &>(expr);
226+
}
227+
228+
static inline sva_ranged_always_exprt &to_sva_ranged_always_expr(exprt &expr)
229+
{
230+
PRECONDITION(expr.id() == ID_sva_ranged_always);
231+
sva_ranged_always_exprt::check(expr, validation_modet::INVARIANT);
232+
return static_cast<sva_ranged_always_exprt &>(expr);
233+
}
234+
235+
class sva_s_always_exprt : public binary_predicate_exprt
236+
{
237+
public:
238+
explicit sva_s_always_exprt(binary_exprt range, exprt op)
239+
: binary_predicate_exprt(std::move(range), ID_sva_s_always, std::move(op))
240+
{
241+
}
242+
243+
// These come with a range, which is binary
244+
const binary_exprt &range() const
245+
{
246+
return static_cast<const binary_exprt &>(op0());
247+
}
248+
249+
binary_exprt &range()
250+
{
251+
return static_cast<binary_exprt &>(op0());
252+
}
253+
254+
const exprt &op() const
255+
{
256+
return op1();
257+
}
258+
259+
exprt &op()
260+
{
261+
return op1();
262+
}
263+
264+
const exprt &lhs() const = delete;
265+
exprt &lhs() = delete;
266+
const exprt &rhs() const = delete;
267+
exprt &rhs() = delete;
268+
269+
static void check(
270+
const exprt &expr,
271+
const validation_modet vm = validation_modet::INVARIANT)
272+
{
273+
binary_exprt::check(expr, vm);
274+
binary_exprt::check(to_binary_expr(expr).op0(), vm);
275+
}
276+
277+
protected:
278+
using binary_predicate_exprt::op0;
279+
using binary_predicate_exprt::op1;
280+
};
281+
282+
static inline const sva_s_always_exprt &to_sva_s_always_expr(const exprt &expr)
283+
{
284+
PRECONDITION(expr.id() == ID_sva_s_always);
285+
sva_s_always_exprt::check(expr, validation_modet::INVARIANT);
286+
return static_cast<const sva_s_always_exprt &>(expr);
287+
}
288+
289+
static inline sva_s_always_exprt &to_sva_s_always_expr(exprt &expr)
290+
{
291+
PRECONDITION(expr.id() == ID_sva_s_always);
292+
sva_s_always_exprt::check(expr, validation_modet::INVARIANT);
293+
return static_cast<sva_s_always_exprt &>(expr);
294+
}
295+
173296
class sva_cover_exprt : public unary_predicate_exprt
174297
{
175298
public:

0 commit comments

Comments
 (0)