Skip to content

Commit 087a57a

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 f77b914 commit 087a57a

File tree

9 files changed

+186
-9
lines changed

9 files changed

+186
-9
lines changed

‎regression/verilog/SVA/always_with_range1.desc‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
always_with_range1.sv
3+
--bound 20
4+
^\[main\.property\.1\] always \[0:9\] main\.x < 10: $
5+
^EXIT=0$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--

‎regression/verilog/SVA/always_with_range1.sv‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
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+
// strong variant
15+
initial p0: assert property (s_always [0:9] x<10);
16+
17+
endmodule

‎src/hw_cbmc_irep_ids.h‎

Lines changed: 2 additions & 0 deletions
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‎

Lines changed: 6 additions & 5 deletions
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‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -54,6 +54,8 @@ bool bmc_supports_property(const exprt &expr)
5454
return true;
5555
else if(expr.id() == ID_sva_always)
5656
return true;
57+
else if(expr.id() == ID_sva_ranged_always)
58+
return true;
5759
else
5860
return false;
5961
}

‎src/verilog/expr2verilog.cpp‎

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1088,6 +1088,22 @@ std::string expr2verilogt::convert(
10881088
else if(src.id()==ID_sva_always)
10891089
return precedence = 0, convert_sva("always", to_sva_always_expr(src).op());
10901090

1091+
else if(src.id() == ID_sva_ranged_always)
1092+
{
1093+
return precedence = 0, convert_sva(
1094+
"always",
1095+
to_sva_ranged_always_expr(src).range(),
1096+
to_sva_ranged_always_expr(src).op());
1097+
}
1098+
1099+
else if(src.id() == ID_sva_s_always)
1100+
{
1101+
return precedence = 0, convert_sva(
1102+
"s_always",
1103+
to_sva_s_always_expr(src).range(),
1104+
to_sva_s_always_expr(src).op());
1105+
}
1106+
10911107
else if(src.id() == ID_sva_cover)
10921108
return precedence = 0, convert_sva("cover", to_sva_cover_expr(src).op());
10931109

‎src/verilog/parser.y‎

Lines changed: 8 additions & 3 deletions
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
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‎

Lines changed: 123 additions & 0 deletions
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:

‎src/verilog/verilog_typecheck_expr.cpp‎

Lines changed: 3 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2236,7 +2236,9 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
22362236

22372237
return std::move(expr);
22382238
}
2239-
else if(expr.id() == ID_sva_eventually)
2239+
else if(
2240+
expr.id() == ID_sva_eventually || expr.id() == ID_sva_ranged_always ||
2241+
expr.id() == ID_sva_s_always)
22402242
{
22412243
auto &range = to_binary_expr(expr.op0());
22422244
auto lower = convert_integer_constant_expression(range.op0());

0 commit comments

Comments
 (0)