From 1ca0d63b8710d13f1d9c82565b27ab4c5b765728 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Mon, 24 Jun 2024 08:45:07 -0700
Subject: [PATCH] Verilog: add test for conditional immediate assertion

This adds a test for an immediate SystemVerilog assertion that is guarded by
an if statement.
---
 regression/verilog/SVA/immediate1.desc |  9 +++++++++
 regression/verilog/SVA/immediate1.sv   | 14 ++++++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 regression/verilog/SVA/immediate1.desc
 create mode 100644 regression/verilog/SVA/immediate1.sv

diff --git a/regression/verilog/SVA/immediate1.desc b/regression/verilog/SVA/immediate1.desc
new file mode 100644
index 000000000..5c8543978
--- /dev/null
+++ b/regression/verilog/SVA/immediate1.desc
@@ -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
+--
diff --git a/regression/verilog/SVA/immediate1.sv b/regression/verilog/SVA/immediate1.sv
new file mode 100644
index 000000000..41ce8a91c
--- /dev/null
+++ b/regression/verilog/SVA/immediate1.sv
@@ -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