Skip to content

Commit 095ae90

Browse files
authored
Merge pull request #928 from diffblue/checker5
KNOWNBUG tests for checkers
2 parents c93d1e8 + 68eae99 commit 095ae90

File tree

4 files changed

+38
-0
lines changed

4 files changed

+38
-0
lines changed
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
checker5.sv
3+
--bound 20
4+
^\[main\.c\.assert\.1\] always myChecker\.data != 10: REFUTED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
--
9+
Support for checkers inside modules is missing.
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
module main(input clk);
2+
checker myChecker(input logic [31:0] data);
3+
assert property (data != 10);
4+
endchecker
5+
6+
reg [31:0] counter = 0;
7+
always_ff @(posedge clk) counter++;
8+
myChecker c(counter);
9+
endmodule
Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
KNOWNBUG
2+
checker6.sv
3+
--bound 20
4+
^\[main\.c\.assert\.1\] always myChecker\.data != 10: REFUTED$
5+
^EXIT=10$
6+
^SIGNAL=0$
7+
--
8+
--
9+
Support for checkers inside packages is missing.
Lines changed: 11 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
package my_package;
2+
checker myChecker(input logic [31:0] data);
3+
assert property (data != 10);
4+
endchecker
5+
endpackage
6+
7+
module main(input clk);
8+
reg [31:0] counter = 0;
9+
always_ff @(posedge clk) counter++;
10+
my_package::myChecker c(counter);
11+
endmodule

0 commit comments

Comments
 (0)