Merge pull request #146 from jix/aim_vs_smt2_nonzero_start_offset

Test and fix signals with nonzero start offsets in aim files with smtbmc

diff --git a/sbysrc/sby_core.py b/sbysrc/sby_core.py
index e1ee51c363f38b37175bfd4e71243745feea8faf..b78ef8531d24547d0c022319fa6f8ec6d784dbe4 100644 (file)
--- a/sbysrc/sby_core.py
+++ b/sbysrc/sby_core.py
@@ -503,7 +503,7 @@ class SbyTask:
                 print("abc -g AND -fast", file=f)
                 print("opt_clean", file=f)
                 print("stat", file=f)
-                print("write_aiger -I -B -zinit -map design_aiger.aim design_aiger.aig", file=f)
+                print("write_aiger -I -B -zinit -no-startoffset -map design_aiger.aim design_aiger.aig", file=f)
 
             proc = SbyProc(
                 self,

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