From c28d4b804720c2cf0086e921748219150e9631b5 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 2 Oct 2019 14:52:40 -0700
Subject: Add test that is expecting to fail

---
 tests/sat/initval.ys | 20 ++++++++++++++++++++
 1 file changed, 20 insertions(+)

(limited to 'tests')

diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys
index 2079d2f34..1627a37e3 100644
--- a/tests/sat/initval.ys
+++ b/tests/sat/initval.ys
@@ -2,3 +2,23 @@ read_verilog -sv initval.v
 proc;;
 
 sat -seq 10 -prove-asserts
+
+read_verilog <<EOT
+module gold(input clk, input i, output reg [1:0] o);
+initial o = 2'b10;
+always @(posedge clk)
+   o[0] <= {i,i};
+endmodule
+
+module gate(input clk, input i, output reg [1:0] o);
+initial o = 2'b10;
+always @(posedge clk)
+   o[0] <= i;
+always @*
+   o[1] <= o[0];
+endmodule
+EOT
+
+proc
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 1 -falsify -prove-asserts -show-ports miter
-- 
cgit v1.2.3


From e730a595eeee1d9936a892c2477c99593d64bcfe Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 2 Oct 2019 17:48:55 -0700
Subject: Add test

---
 tests/various/peepopt.ys | 31 +++++++++++++++++++++++++++++++
 1 file changed, 31 insertions(+)

(limited to 'tests')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index 6bca62e2b..dc0acf3ca 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -173,3 +173,34 @@ select -assert-count 1 t:$dff r:WIDTH=2 %i
 select -assert-count 2 t:$mux
 select -assert-count 2 t:$mux r:WIDTH=2 %i
 select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D
+
+####################
+
+design -reset
+read_verilog <<EOT
+module peepopt_dffmuxext_signed_rst_init(input clk, ce, rstn, input signed [1:0] i, output reg signed [3:0] o);
+    initial o <= 4'b0010;
+    always @(posedge clk) begin
+        if (ce) o <= i;
+        if (!rstn) o <= 4'b1111;
+    end
+endmodule
+EOT
+
+proc
+#equiv_opt -assert peepopt
+
+design -save gold
+peepopt
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 1 -verify -prove-asserts -show-ports miter
+
+design -load postopt
+wreduce
+select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 2 t:$mux
+select -assert-count 2 t:$mux r:WIDTH=2 %i
+select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D
-- 
cgit v1.2.3


From f6fabc8fda1eb00b0227f1a91d85b837a0609728 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 2 Oct 2019 18:03:45 -0700
Subject: Update test

---
 tests/various/peepopt.ys | 16 +++-------------
 1 file changed, 3 insertions(+), 13 deletions(-)

(limited to 'tests')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index dc0acf3ca..734a22408 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -188,19 +188,9 @@ endmodule
 EOT
 
 proc
-#equiv_opt -assert peepopt
-
-design -save gold
-peepopt
-design -stash gate
-design -import gold -as gold
-design -import gate -as gate
-miter -equiv -flatten -make_assert -make_outputs gold gate miter
-sat -seq 1 -verify -prove-asserts -show-ports miter
-
+equiv_opt -assert peepopt
 design -load postopt
-wreduce
-select -assert-count 1 t:$dff r:WIDTH=2 %i
+select -assert-count 1 t:$dff r:WIDTH=4 %i
 select -assert-count 2 t:$mux
-select -assert-count 2 t:$mux r:WIDTH=2 %i
+select -assert-count 2 t:$mux r:WIDTH=4 %i
 select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D
-- 
cgit v1.2.3


From e4bd5aaebf7e329236b10c93eac9ad113231f00e Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 2 Oct 2019 18:12:25 -0700
Subject: Fix test

---
 tests/various/peepopt.ys | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

(limited to 'tests')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index 734a22408..1f18f1c74 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -188,8 +188,18 @@ endmodule
 EOT
 
 proc
-equiv_opt -assert peepopt
-design -load postopt
+#equiv_opt -assert peepopt
+
+design -save gold
+peepopt
+wreduce
+design -stash gate
+design -import gold -as gold
+design -import gate -as gate
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -seq 1 -verify -prove-asserts -show-ports miter
+
+design -load gate
 select -assert-count 1 t:$dff r:WIDTH=4 %i
 select -assert-count 2 t:$mux
 select -assert-count 2 t:$mux r:WIDTH=4 %i
-- 
cgit v1.2.3


From e9645c7fa7fc349afad103ff8736699bb4dc0412 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Wed, 2 Oct 2019 21:26:26 -0700
Subject: Fix broken CI, check reset even for constants, trim rstmux

---
 tests/various/peepopt.ys | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'tests')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index 1f18f1c74..4b130578b 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -131,8 +131,8 @@ EOT
 proc
 equiv_opt -assert peepopt
 design -load postopt
-select -assert-count 1 t:$dff r:WIDTH=5 %i
-select -assert-count 1 t:$mux r:WIDTH=5 %i
+select -assert-count 1 t:$dff r:WIDTH=4 %i
+select -assert-count 1 t:$mux r:WIDTH=4 %i
 select -assert-count 0 t:$dff t:$mux %% t:* %D
 
 ####################
-- 
cgit v1.2.3


From 045f34403889b69f3ac3ac08d96e5cf1fae787d1 Mon Sep 17 00:00:00 2001
From: Eddie Hung <eddie@fpgeh.com>
Date: Thu, 3 Oct 2019 11:11:50 -0700
Subject: Use `sat -tempinduct` and comments for why equiv_opt not sufficient

---
 tests/various/peepopt.ys | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'tests')

diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys
index 4b130578b..ee5ad8a1a 100644
--- a/tests/various/peepopt.ys
+++ b/tests/various/peepopt.ys
@@ -188,6 +188,13 @@ endmodule
 EOT
 
 proc
+# NB: equiv_opt uses equiv_induct which covers
+#     only the induction half of temporal induction
+#     --- missing the base-case half
+#     This makes it akin to `sat -tempinduct-inductonly`
+#     instead of `sat -tempinduct-baseonly` or
+#     `sat -tempinduct` which is necessary for this
+#     testcase
 #equiv_opt -assert peepopt
 
 design -save gold
@@ -197,7 +204,7 @@ design -stash gate
 design -import gold -as gold
 design -import gate -as gate
 miter -equiv -flatten -make_assert -make_outputs gold gate miter
-sat -seq 1 -verify -prove-asserts -show-ports miter
+sat -tempinduct -verify -prove-asserts -show-ports miter
 
 design -load gate
 select -assert-count 1 t:$dff r:WIDTH=4 %i
-- 
cgit v1.2.3