Skip to content

Commit

Permalink
ebmc: add two basic tests for CEGAR
Browse files Browse the repository at this point in the history
  • Loading branch information
kroening committed Dec 24, 2024
1 parent ddf9f0a commit 302cacf
Show file tree
Hide file tree
Showing 4 changed files with 37 additions and 0 deletions.
6 changes: 6 additions & 0 deletions regression/ebmc/cegar/basic1.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
KNOWNBUG
basic1.sv
--cegar
SUCCESS$
^EXIT=0$
^SIGNAL=0$
12 changes: 12 additions & 0 deletions regression/ebmc/cegar/basic1.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,12 @@
module top(input clk);

reg important;
reg not_important;

initial important = 1;
always @(posedge clk)
important = important;

assert property (important == 1);

endmodule
6 changes: 6 additions & 0 deletions regression/ebmc/cegar/basic2.desc
Original file line number Diff line number Diff line change
@@ -0,0 +1,6 @@
CORE
basic2.sv
--cegar
^VERIFICATION FAILED -- PROPERTY REFUTED$
^EXIT=0$
^SIGNAL=0$
13 changes: 13 additions & 0 deletions regression/ebmc/cegar/basic2.sv
Original file line number Diff line number Diff line change
@@ -0,0 +1,13 @@
module top(input clk);

reg important;
reg not_important;

initial important = 1;
always @(posedge clk)
important = 0;

// should fail after one transition
assert property (important == 1);

endmodule

0 comments on commit 302cacf

Please sign in to comment.