From 68eae996fb3c768204a6690409182c97fd015fa4 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Wed, 15 Jan 2025 11:34:14 -0800
Subject: [PATCH] KNOWNBUG tests for checkers

---
 regression/verilog/checker/checker5.desc |  9 +++++++++
 regression/verilog/checker/checker5.sv   |  9 +++++++++
 regression/verilog/checker/checker6.desc |  9 +++++++++
 regression/verilog/checker/checker6.sv   | 11 +++++++++++
 4 files changed, 38 insertions(+)
 create mode 100644 regression/verilog/checker/checker5.desc
 create mode 100644 regression/verilog/checker/checker5.sv
 create mode 100644 regression/verilog/checker/checker6.desc
 create mode 100644 regression/verilog/checker/checker6.sv

diff --git a/regression/verilog/checker/checker5.desc b/regression/verilog/checker/checker5.desc
new file mode 100644
index 00000000..3424d867
--- /dev/null
+++ b/regression/verilog/checker/checker5.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+checker5.sv
+--bound 20
+^\[main\.c\.assert\.1\] always myChecker\.data != 10: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Support for checkers inside modules is missing.
diff --git a/regression/verilog/checker/checker5.sv b/regression/verilog/checker/checker5.sv
new file mode 100644
index 00000000..c863a3be
--- /dev/null
+++ b/regression/verilog/checker/checker5.sv
@@ -0,0 +1,9 @@
+module main(input clk);
+  checker myChecker(input logic [31:0] data);
+    assert property (data != 10);
+  endchecker
+
+  reg [31:0] counter = 0;
+  always_ff @(posedge clk) counter++;
+  myChecker c(counter);
+endmodule
diff --git a/regression/verilog/checker/checker6.desc b/regression/verilog/checker/checker6.desc
new file mode 100644
index 00000000..f844bd16
--- /dev/null
+++ b/regression/verilog/checker/checker6.desc
@@ -0,0 +1,9 @@
+KNOWNBUG
+checker6.sv
+--bound 20
+^\[main\.c\.assert\.1\] always myChecker\.data != 10: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+Support for checkers inside packages is missing.
diff --git a/regression/verilog/checker/checker6.sv b/regression/verilog/checker/checker6.sv
new file mode 100644
index 00000000..8616c018
--- /dev/null
+++ b/regression/verilog/checker/checker6.sv
@@ -0,0 +1,11 @@
+package my_package;
+  checker myChecker(input logic [31:0] data);
+    assert property (data != 10);
+  endchecker
+endpackage
+
+module main(input clk);
+  reg [31:0] counter = 0;
+  always_ff @(posedge clk) counter++;
+  my_package::myChecker c(counter);
+endmodule