6 files changed, 70 insertions, 2 deletions
diff --git a/tests/sat/asserts.ys b/tests/sat/asserts.ys
index de5e7c9aa..d8f994925 100644
--- a/tests/sat/asserts.ys
+++ b/tests/sat/asserts.ys
@@ -1,3 +1,3 @@
-read_verilog asserts.v
+read_verilog -sv asserts.v
 hierarchy; proc; opt
 sat -verify -seq 1 -set-at 1 rst 1 -tempinduct -prove-asserts
diff --git a/tests/sat/asserts_seq.ys b/tests/sat/asserts_seq.ys
index c622ef610..e97686644 100644
--- a/tests/sat/asserts_seq.ys
+++ b/tests/sat/asserts_seq.ys
@@ -1,4 +1,4 @@
-read_verilog asserts_seq.v
+read_verilog -sv asserts_seq.v
 hierarchy; proc; opt
 
 sat -verify  -prove-asserts -tempinduct -seq 1 test_001
diff --git a/tests/sat/initval.v b/tests/sat/initval.v
new file mode 100644
index 000000000..5b661f8d6
--- /dev/null
+++ b/tests/sat/initval.v
@@ -0,0 +1,15 @@
+module test(input clk, input [3:0] bar, output [3:0] foo);
+  reg [3:0] foo = 0;
+  reg [3:0] last_bar = 0;
+
+  always @*
+    foo[1:0] <= bar[1:0];
+
+  always @(posedge clk)
+    foo[3:2] <= bar[3:2];
+
+  always @(posedge clk)
+    last_bar <= bar;
+
+  assert property (foo == {last_bar[3:2], bar[1:0]});
+endmodule
diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys
new file mode 100644
index 000000000..2079d2f34
--- /dev/null
+++ b/tests/sat/initval.ys
@@ -0,0 +1,4 @@
+read_verilog -sv initval.v
+proc;;
+
+sat -seq 10 -prove-asserts
diff --git a/tests/sat/share.v b/tests/sat/share.v
new file mode 100644
index 000000000..e06fc8f1e
--- /dev/null
+++ b/tests/sat/share.v
@@ -0,0 +1,32 @@
+module test_1(
+	input [7:0] a, b, c,
+	input s, x,
+	output [7:0] y1, y2
+);
+	wire [7:0] t1, t2;
+	assign t1 = s ? a*b : 0, t2 = !s ? b*c : 0;
+	assign y1 = x ? t2 : t1, y2 = x ? t1 : t2;
+endmodule
+
+
+module test_2(
+	input s,
+	input [7:0] a, b, c,
+	output reg [7:0] y
+);
+	always @* begin
+		y <= 'bx;
+		if (s) begin
+			if (a * b > 8)
+				y <= b / c;
+			else
+				y <= c / b;
+		end else begin
+			if (b * c > 8)
+				y <= a / b;
+			else
+				y <= b / a;
+		end
+	end
+endmodule
+
diff --git a/tests/sat/share.ys b/tests/sat/share.ys
new file mode 100644
index 000000000..f2f5d649d
--- /dev/null
+++ b/tests/sat/share.ys
@@ -0,0 +1,17 @@
+read_verilog share.v
+proc;;
+
+copy test_1 gold_1
+copy test_2 gold_2
+share test_1 test_2;;
+
+select -assert-count 1 test_1/t:$mul
+select -assert-count 1 test_2/t:$mul
+select -assert-count 1 test_2/t:$div
+
+miter -equiv -flatten -make_outputs -make_outcmp gold_1 test_1 miter_1
+sat -verify -prove trigger 0 -show-inputs -show-outputs miter_1
+
+miter -equiv -flatten -make_outputs -make_outcmp gold_2 test_2 miter_2
+sat -verify -prove trigger 0 -show-inputs -show-outputs miter_2
+