From: Jannis Harder <me@jix.one>
Date: Thu, 24 Mar 2022 12:12:25 +0000 (+0100)
Subject: Test signals with nonzero start offsets in aim files with smtbmc
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a434252ca130dc673eb58cc698f8a9e39a273c1b;p=SymbiYosys.git

Test signals with nonzero start offsets in aim files with smtbmc
---

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