Merge remote-tracking branch 'origin/master' into xaig

4 files changed, 110 insertions, 0 deletions

diff --git a/tests/sat/counters-repeat.v b/tests/sat/counters-repeat.v
new file mode 100644
index 000000000..2ea45499a
--- /dev/null
+++ b/tests/sat/counters-repeat.v
@@ -0,0 +1,38 @@
+// coverage for repeat loops outside of constant functions
+
+module counter1(clk, rst, ping);
+	input clk, rst;
+	output ping;
+	reg [31:0] count;
+
+	always @(posedge clk) begin
+		if (rst)
+			count <= 0;
+		else
+			count <= count + 1;
+	end
+
+	assign ping = &count;
+endmodule
+
+module counter2(clk, rst, ping);
+	input clk, rst;
+	output ping;
+	reg [31:0] count;
+
+	integer i;
+	reg carry;
+
+	always @(posedge clk) begin
+		carry = 1;
+		i = 0;
+		repeat (32) begin
+			count[i] <= !rst & (count[i] ^ carry);
+			carry = count[i] & carry;
+			i = i+1;
+		end
+	end
+
+	assign ping = &count;
+endmodule
+
diff --git a/tests/sat/counters-repeat.ys b/tests/sat/counters-repeat.ys
new file mode 100644
index 000000000..b3dcfe08a
--- /dev/null
+++ b/tests/sat/counters-repeat.ys
@@ -0,0 +1,10 @@
+
+read_verilog counters-repeat.v
+proc; opt
+
+expose -shared counter1 counter2
+miter -equiv -make_assert -make_outputs counter1 counter2 miter
+
+cd miter; flatten; opt
+sat -verify -prove-asserts -tempinduct -set-at 1 in_rst 1 -seq 1 -show-inputs -show-outputs
+
diff --git a/tests/various/pmux2shiftx.v b/tests/various/pmux2shiftx.v
new file mode 100644
index 000000000..fec84187b
--- /dev/null
+++ b/tests/various/pmux2shiftx.v
@@ -0,0 +1,34 @@
+module pmux2shiftx_test (
+	input [2:0] S1,
+	input [5:0] S2,
+	input [1:0] S3,
+	input [9:0] A, B, C, D, D, E, F, G, H,
+	input [9:0] I, J, K, L, M, N, O, P, Q,
+	output reg [9:0] X
+);
+	always @* begin
+		case (S1)
+			3'd 0: X = A;
+			3'd 1: X = B;
+			3'd 2: X = C;
+			3'd 3: X = D;
+			3'd 4: X = E;
+			3'd 5: X = F;
+			3'd 6: X = G;
+			3'd 7: X = H;
+		endcase
+		case (S2)
+			6'd 45: X = I;
+			6'd 47: X = J;
+			6'd 49: X = K;
+			6'd 55: X = L;
+			6'd 57: X = M;
+			6'd 59: X = N;
+		endcase
+		case (S3)
+			2'd 1: X = O;
+			2'd 2: X = P;
+			2'd 3: X = Q;
+		endcase
+	end
+endmodule
diff --git a/tests/various/pmux2shiftx.ys b/tests/various/pmux2shiftx.ys
new file mode 100644
index 000000000..deb134083
--- /dev/null
+++ b/tests/various/pmux2shiftx.ys
@@ -0,0 +1,28 @@
+read_verilog pmux2shiftx.v
+prep
+design -save gold
+
+pmux2shiftx -min_density 70
+
+opt
+
+stat
+# show -width
+select -assert-count 1 t:$sub
+select -assert-count 1 t:$mux
+select -assert-count 1 t:$shift
+select -assert-count 3 t:$shiftx
+
+design -stash gate
+
+design -import gold -as gold
+design -import gate -as gate
+
+miter -equiv -flatten -make_assert -make_outputs gold gate miter
+sat -verify -prove-asserts -show-ports miter
+
+design -load gold
+stat
+
+design -load gate
+stat