Skip to content

Commit 1d075d4

Browse files
tautschnigtautschnig
authored
Merge pull request #533 from diffblue/indexed_nexttime
Verilog SVA: indexed `nexttime` and `s_nexttime`
2 parents 7e07de2 + 39f96a6 commit 1d075d4

File tree

9 files changed

+179
-16
lines changed

9 files changed

+179
-16
lines changed

‎regression/verilog/SVA/nexttime1.desc‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
KNOWNBUG
2+
nexttime1.sv
3+
--module main --bound 10
4+
^\[main\.property\.1\] s_nexttime\[0\] main\.counter == 0: PROVED up to bound 10$
5+
^\[main\.property\.2\] s_nexttime\[1\] main\.counter == 1: PROVED up to bound 10$
6+
^\[main\.property\.3\] nexttime\[8\] main\.counter == 8: PROVED up to bound 10$
7+
^EXIT=10$
8+
^SIGNAL=0$
9+
--
10+
^warning: ignoring
11+
--
12+
Backend support missing.

‎regression/verilog/SVA/nexttime1.sv‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
module main(input clk);
2+
3+
// count up from 0 to 10
4+
reg [7:0] counter;
5+
6+
initial counter = 0;
7+
8+
always @(posedge clk)
9+
if(counter == 10)
10+
counter = 0;
11+
else
12+
counter = counter + 1;
13+
14+
// expected to pass
15+
initial p1: assert property (s_nexttime[0] counter == 0);
16+
17+
// expected to pass
18+
initial p2: assert property (s_nexttime[1] counter == 1);
19+
20+
// expected to pass
21+
initial p3: assert property (nexttime[8] counter == 8);
22+
23+
endmodule

‎src/temporal-logic/negate_property.cpp‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -93,7 +93,7 @@ exprt negate_property(const exprt &expr)
9393
}
9494
else if(expr.id() == ID_sva_nexttime)
9595
{
96-
unary_exprt result = to_sva_nexttime_expr(expr);
96+
auto result = to_sva_nexttime_expr(expr);
9797
result.op() = negate_property(result.op());
9898
return std::move(result);
9999
}

‎src/temporal-logic/normalize_property.cpp‎

Lines changed: 8 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -112,9 +112,15 @@ exprt normalize_property(exprt expr)
112112
expr = normalize_pre_sva_non_overlapped_implication(
113113
to_sva_non_overlapped_implication_expr(expr));
114114
else if(expr.id() == ID_sva_nexttime)
115-
expr = X_exprt{to_sva_nexttime_expr(expr).op()};
115+
{
116+
if(!to_sva_nexttime_expr(expr).is_indexed())
117+
expr = X_exprt{to_sva_nexttime_expr(expr).op()};
118+
}
116119
else if(expr.id() == ID_sva_s_nexttime)
117-
expr = X_exprt{to_sva_s_nexttime_expr(expr).op()};
120+
{
121+
if(!to_sva_s_nexttime_expr(expr).is_indexed())
122+
expr = X_exprt{to_sva_s_nexttime_expr(expr).op()};
123+
}
118124
else if(expr.id() == ID_sva_cycle_delay)
119125
expr = normalize_pre_sva_cycle_delay(to_sva_cycle_delay_expr(expr));
120126
else if(expr.id() == ID_sva_cycle_delay_plus)

‎src/verilog/expr2verilog.cpp‎

Lines changed: 33 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -430,7 +430,7 @@ std::string expr2verilogt::convert_sva_unary(
430430

431431
/*******************************************************************\
432432
433-
Function: expr2verilogt::convert_sva
433+
Function: expr2verilogt::convert_sva_binary
434434
435435
Inputs:
436436
@@ -459,6 +459,35 @@ std::string expr2verilogt::convert_sva_binary(
459459

460460
/*******************************************************************\
461461
462+
Function: expr2verilogt::convert_sva_indexed_binary
463+
464+
Inputs:
465+
466+
Outputs:
467+
468+
Purpose:
469+
470+
\*******************************************************************/
471+
472+
std::string expr2verilogt::convert_sva_indexed_binary(
473+
const std::string &name,
474+
const binary_exprt &expr)
475+
{
476+
std::string s0;
477+
478+
if(expr.op0().is_not_nil())
479+
s0 = '[' + convert(expr.lhs()) + ']';
480+
481+
unsigned p1;
482+
auto s1 = convert(expr.rhs(), p1);
483+
if(p1 == 0)
484+
s1 = "(" + s1 + ")";
485+
486+
return name + s0 + ' ' + s1;
487+
}
488+
489+
/*******************************************************************\
490+
462491
Function: expr2verilogt::convert_replication
463492
464493
Inputs:
@@ -1161,11 +1190,11 @@ std::string expr2verilogt::convert(
11611190

11621191
else if(src.id()==ID_sva_nexttime)
11631192
return precedence = 0,
1164-
convert_sva_unary("nexttime", to_sva_nexttime_expr(src));
1193+
convert_sva_indexed_binary("nexttime", to_sva_nexttime_expr(src));
11651194

11661195
else if(src.id()==ID_sva_s_nexttime)
1167-
return precedence = 0,
1168-
convert_sva_unary("s_nexttime", to_sva_s_nexttime_expr(src));
1196+
return precedence = 0, convert_sva_indexed_binary(
1197+
"s_nexttime", to_sva_s_nexttime_expr(src));
11691198

11701199
else if(src.id()==ID_sva_eventually)
11711200
{

‎src/verilog/expr2verilog_class.h‎

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

9393
std::string convert_sva_binary(const std::string &name, const binary_exprt &);
9494

95+
std::string
96+
convert_sva_indexed_binary(const std::string &name, const binary_exprt &);
97+
9598
virtual std::string
9699
convert_replication(const replication_exprt &, unsigned precedence);
97100

‎src/verilog/parser.y‎

Lines changed: 10 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -2059,11 +2059,18 @@ property_expr_proper:
20592059
| property_expr "and" property_expr { init($$, ID_and); mto($$, $1); mto($$, $3); }
20602060
| property_expr "|->" property_expr { init($$, ID_sva_overlapped_implication); mto($$, $1); mto($$, $3); }
20612061
| property_expr "|=>" property_expr { init($$, ID_sva_non_overlapped_implication); mto($$, $1); mto($$, $3); }
2062-
| "nexttime" property_expr { init($$, "sva_nexttime"); mto($$, $2); }
2063-
| "s_nexttime" property_expr { init($$, "sva_s_nexttime"); mto($$, $2); }
2062+
| "nexttime" property_expr
2063+
{ init($$, "sva_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); }
2064+
| "nexttime" '[' constant_expression ']' property_expr %prec "nexttime"
2065+
{ init($$, "sva_nexttime"); mto($$, $3); mto($$, $5); }
2066+
| "s_nexttime" property_expr
2067+
{ init($$, "sva_s_nexttime"); stack_expr($$).add_to_operands(nil_exprt()); mto($$, $2); }
2068+
| "s_nexttime" '[' constant_expression ']' property_expr %prec "s_nexttime"
2069+
{ init($$, "sva_s_nexttime"); mto($$, $3); mto($$, $5); }
20642070
| "always" '[' cycle_delay_const_range_expression ']' property_expr %prec "always"
20652071
{ init($$, ID_sva_ranged_always); swapop($$, $3); mto($$, $5); }
2066-
| "always" property_expr { init($$, "sva_always"); mto($$, $2); }
2072+
| "always" property_expr
2073+
{ init($$, "sva_always"); mto($$, $2); }
20672074
| "s_always" '[' constant_range ']' property_expr %prec "s_always"
20682075
{ init($$, ID_sva_s_always); swapop($$, $3); mto($$, $5); }
20692076
| "s_eventually" property_expr

‎src/verilog/sva_expr.h‎

Lines changed: 64 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -11,13 +11,43 @@ Author: Daniel Kroening, kroening@kroening.com
1111

1212
#include <util/std_expr.h>
1313

14-
class sva_nexttime_exprt : public unary_predicate_exprt
14+
class sva_nexttime_exprt : public binary_predicate_exprt
1515
{
1616
public:
17+
// nonindexed variant
1718
explicit sva_nexttime_exprt(exprt op)
18-
: unary_predicate_exprt(ID_sva_nexttime, std::move(op))
19+
: binary_predicate_exprt(nil_exprt(), ID_sva_nexttime, std::move(op))
1920
{
2021
}
22+
23+
bool is_indexed() const
24+
{
25+
return index().is_not_nil();
26+
}
27+
28+
const exprt &index() const
29+
{
30+
return op0();
31+
}
32+
33+
exprt &index()
34+
{
35+
return op0();
36+
}
37+
38+
const exprt &op() const
39+
{
40+
return op1();
41+
}
42+
43+
exprt &op()
44+
{
45+
return op1();
46+
}
47+
48+
protected:
49+
using binary_predicate_exprt::op0;
50+
using binary_predicate_exprt::op1;
2151
};
2252

2353
static inline const sva_nexttime_exprt &to_sva_nexttime_expr(const exprt &expr)
@@ -34,13 +64,43 @@ static inline sva_nexttime_exprt &to_sva_nexttime_expr(exprt &expr)
3464
return static_cast<sva_nexttime_exprt &>(expr);
3565
}
3666

37-
class sva_s_nexttime_exprt : public unary_predicate_exprt
67+
class sva_s_nexttime_exprt : public binary_predicate_exprt
3868
{
3969
public:
70+
// nonindexed variant
4071
explicit sva_s_nexttime_exprt(exprt op)
41-
: unary_predicate_exprt(ID_sva_s_nexttime, std::move(op))
72+
: binary_predicate_exprt(nil_exprt(), ID_sva_s_nexttime, std::move(op))
4273
{
4374
}
75+
76+
bool is_indexed() const
77+
{
78+
return index().is_not_nil();
79+
}
80+
81+
const exprt &index() const
82+
{
83+
return op0();
84+
}
85+
86+
exprt &index()
87+
{
88+
return op0();
89+
}
90+
91+
const exprt &op() const
92+
{
93+
return op1();
94+
}
95+
96+
exprt &op()
97+
{
98+
return op1();
99+
}
100+
101+
protected:
102+
using binary_predicate_exprt::op0;
103+
using binary_predicate_exprt::op1;
44104
};
45105

46106
static inline const sva_s_nexttime_exprt &

‎src/verilog/verilog_typecheck_expr.cpp‎

Lines changed: 25 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1905,8 +1905,7 @@ exprt verilog_typecheck_exprt::convert_unary_expr(unary_exprt expr)
19051905
expr.type() = expr.op().type();
19061906
}
19071907
else if(
1908-
expr.id() == ID_sva_always || expr.id() == ID_sva_nexttime ||
1909-
expr.id() == ID_sva_s_nexttime || expr.id() == ID_sva_s_eventually ||
1908+
expr.id() == ID_sva_always || expr.id() == ID_sva_s_eventually ||
19101909
expr.id() == ID_sva_cycle_delay_plus ||
19111910
expr.id() == ID_sva_cycle_delay_star)
19121911
{
@@ -2237,6 +2236,30 @@ exprt verilog_typecheck_exprt::convert_binary_expr(binary_exprt expr)
22372236

22382237
return std::move(expr);
22392238
}
2239+
else if(expr.id() == ID_sva_nexttime)
2240+
{
2241+
if(to_sva_nexttime_expr(expr).is_indexed())
2242+
convert_expr(to_sva_nexttime_expr(expr).index());
2243+
2244+
auto &op = to_sva_nexttime_expr(expr).op();
2245+
convert_expr(op);
2246+
make_boolean(op);
2247+
expr.type() = bool_typet();
2248+
2249+
return std::move(expr);
2250+
}
2251+
else if(expr.id() == ID_sva_s_nexttime)
2252+
{
2253+
if(to_sva_s_nexttime_expr(expr).is_indexed())
2254+
convert_expr(to_sva_s_nexttime_expr(expr).index());
2255+
2256+
auto &op = to_sva_s_nexttime_expr(expr).op();
2257+
convert_expr(op);
2258+
make_boolean(op);
2259+
expr.type() = bool_typet();
2260+
2261+
return std::move(expr);
2262+
}
22402263
else if(expr.id()==ID_sva_overlapped_implication ||
22412264
expr.id()==ID_sva_non_overlapped_implication ||
22422265
expr.id()==ID_sva_until ||

0 commit comments

Comments
 (0)