Merge pull request #577 from diffblue/immediate1-1

Verilog: add test for conditional immediate assertion
diffblue · Jun 25, 2024 · f48e9b2 · f48e9b2
2 parents 756dfeb + 1ca0d63
commit f48e9b2
Show file tree

Hide file tree

Showing 2 changed files with 23 additions and 0 deletions.
diff --git a/regression/verilog/SVA/immediate1.desc 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
@@ -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