Skip to content

Commit

Permalink
SVA: error message non-constant SVA cycle delays
Browse files Browse the repository at this point in the history
Replicates third example in #931.
  • Loading branch information
kroening committed Jan 17, 2025
1 parent f6c38d9 commit 76d3b1c
Show file tree
Hide file tree
Showing 4 changed files with 29 additions and 1 deletion.
9 changes: 9 additions & 0 deletions regression/verilog/SVA/cycle_delay1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
cycle_delay1.sv

^file cycle_delay1\.sv line \d+: expected constant expression, but got `main.from'$
^EXIT=2$
^SIGNAL=0$
--
^warning: ignoring
--
11 changes: 11 additions & 0 deletions regression/verilog/SVA/cycle_delay1.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
module main(input clk, input [31:0] from);

reg [31:0] x;

always_ff @(posedge clk)
x++;

// The cycle delay must be elaboration-time constant
initial assert property (##[from:2] x!=10);

endmodule
2 changes: 1 addition & 1 deletion regression/verilog/SVA/unbounded1.desc
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
CORE
unbounded1.sv
--module main --bound 1
^\[main\.assert\.1\] always \(main\.a ##\[0:main\.upper\] main.b\): REFUTED$
^\[main\.assert\.1\] always \(main\.a ##\[0:\$\] main.b\): REFUTED$
^EXIT=10$
^SIGNAL=0$
--
8 changes: 8 additions & 0 deletions src/verilog/verilog_typecheck_sva.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -193,11 +193,19 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr)
if(expr.id() == ID_sva_cycle_delay) // ##[1:2] something
{
expr.type() = bool_typet();

convert_expr(expr.op0());
expr.op0() = elaborate_constant_expression_check(expr.op0());

if(expr.op1().is_not_nil())
{
convert_expr(expr.op1());
expr.op1() = elaborate_constant_expression_check(expr.op1());
}

convert_sva(expr.op2());
make_boolean(expr.op2());

return std::move(expr);
}
else if(
Expand Down

0 comments on commit 76d3b1c

Please sign in to comment.