Skip to content

Commit

Permalink
SVA: add test with 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 34da31d
Show file tree
Hide file tree
Showing 2 changed files with 21 additions and 0 deletions.
10 changes: 10 additions & 0 deletions regression/verilog/SVA/cycle_delay1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,10 @@
CORE
cycle_delay1.sv

^C string exception : failed to convert sva_cycle_delay offsets$
^EXIT=2$
^SIGNAL=0$
--
^warning: ignoring
--
The error message could be better.
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

0 comments on commit 34da31d

Please sign in to comment.