Test signals with nonzero start offsets in aim files with smtbmc

diff --git a/tests/.gitignore b/tests/.gitignore
index 212f4ddbe1f3e25fcc3abb967ed421e5905ef440..120675bec4354855a2ba9fe51cff81368d3f05b8 100644 (file)
--- a/tests/.gitignore
+++ b/tests/.gitignore
@@ -10,3 +10,4 @@
 /junit_*/
 /submod_props*/
 /multi_assert*/
+/aim_vs_smt2_nonzero_start_offset*/

diff --git a/tests/aim_vs_smt2_nonzero_start_offset.sby b/tests/aim_vs_smt2_nonzero_start_offset.sby
new file mode 100644 (file)
index 0000000..4309551
--- /dev/null
+++ b/tests/aim_vs_smt2_nonzero_start_offset.sby
@@ -0,0 +1,33 @@
+[tasks]
+bmc
+prove
+
+[options]
+bmc: mode bmc
+prove: mode prove
+expect fail
+wait on
+
+[engines]
+bmc: abc bmc3
+bmc: abc sim3
+prove: aiger avy
+prove: aiger suprove
+prove: abc pdr
+
+[script]
+read -sv test.sv
+prep -top test
+
+[file test.sv]
+module test (
+    input clk,
+    input [8:1] nonzero_offset
+);
+    reg [7:0] counter = 0;
+
+    always @(posedge clk) begin
+        if (counter == 3) assert(nonzero_offset[1]);
+        counter <= counter + 1;
+    end
+endmodule