From a434252ca130dc673eb58cc698f8a9e39a273c1b Mon Sep 17 00:00:00 2001
From: Jannis Harder <me@jix.one>
Date: Thu, 24 Mar 2022 13:12:25 +0100
Subject: [PATCH] Test signals with nonzero start offsets in aim files with
 smtbmc

---
 tests/.gitignore                           |  1 +
 tests/aim_vs_smt2_nonzero_start_offset.sby | 33 ++++++++++++++++++++++
 2 files changed, 34 insertions(+)
 create mode 100644 tests/aim_vs_smt2_nonzero_start_offset.sby

diff --git a/tests/.gitignore b/tests/.gitignore
index 212f4dd..120675b 100644
--- 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
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
-- 
2.30.2