Skip to content

Commit 76d3b1c

Browse files
committed
SVA: error message non-constant SVA cycle delays
Replicates third example in #931.
1 parent f6c38d9 commit 76d3b1c

File tree

4 files changed

+29
-1
lines changed

4 files changed

+29
-1
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
CORE
2+
cycle_delay1.sv
3+
4+
^file cycle_delay1\.sv line \d+: expected constant expression, but got `main.from'$
5+
^EXIT=2$
6+
^SIGNAL=0$
7+
--
8+
^warning: ignoring
9+
--
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
module main(input clk, input [31:0] from);
2+
3+
reg [31:0] x;
4+
5+
always_ff @(posedge clk)
6+
x++;
7+
8+
// The cycle delay must be elaboration-time constant
9+
initial assert property (##[from:2] x!=10);
10+
11+
endmodule
Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
CORE
22
unbounded1.sv
33
--module main --bound 1
4-
^\[main\.assert\.1\] always \(main\.a ##\[0:main\.upper\] main.b\): REFUTED$
4+
^\[main\.assert\.1\] always \(main\.a ##\[0:\$\] main.b\): REFUTED$
55
^EXIT=10$
66
^SIGNAL=0$
77
--

src/verilog/verilog_typecheck_sva.cpp

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -193,11 +193,19 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr)
193193
if(expr.id() == ID_sva_cycle_delay) // ##[1:2] something
194194
{
195195
expr.type() = bool_typet();
196+
196197
convert_expr(expr.op0());
198+
expr.op0() = elaborate_constant_expression_check(expr.op0());
199+
197200
if(expr.op1().is_not_nil())
201+
{
198202
convert_expr(expr.op1());
203+
expr.op1() = elaborate_constant_expression_check(expr.op1());
204+
}
205+
199206
convert_sva(expr.op2());
200207
make_boolean(expr.op2());
208+
201209
return std::move(expr);
202210
}
203211
else if(

0 commit comments

Comments
 (0)