Skip to content

Commit

Permalink
Verilog: add test for conditional immediate assertion
Browse files Browse the repository at this point in the history
This adds a test for an immediate SystemVerilog assertion that is guarded by
an if statement.
  • Loading branch information
kroening committed Jun 24, 2024
1 parent 921e331 commit 1ca0d63
Show file tree
Hide file tree
Showing 2 changed files with 23 additions and 0 deletions.
9 changes: 9 additions & 0 deletions regression/verilog/SVA/immediate1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,9 @@
CORE
immediate1.sv
--bound 20
^\[main\.assert\.1\] always \(main\.x == 11 \|-> main\.x & 1\): PROVED up to bound 20$
^EXIT=0$
^SIGNAL=0$
--
^warning: ignoring
--
14 changes: 14 additions & 0 deletions regression/verilog/SVA/immediate1.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,14 @@
module main(input clk);

reg [31:0] x;

initial x=0;

always @(posedge clk) begin
if(x == 11)
assert(x & 1); // holds

x<=x+1;
end

endmodule

0 comments on commit 1ca0d63

Please sign in to comment.