Added splice command

2 files changed, 28 insertions, 0 deletions

diff --git a/tests/sat/splice.v b/tests/sat/splice.v
new file mode 100644
index 000000000..8d1dcd22f
--- /dev/null
+++ b/tests/sat/splice.v
@@ -0,0 +1,14 @@
+module test(a, b, y);
+
+input [15:0] a, b;
+output [15:0] y;
+
+wire [7:0] ah = a[15:8], al = a[7:0];
+wire [7:0] bh = b[15:8], bl = b[7:0];
+
+wire [7:0] th = ah + bh, tl = al + bl;
+wire [15:0] t = {th, tl}, k = t ^ 16'hcd;
+
+assign y = { k[7:0], k[15:8] };
+
+endmodule
diff --git a/tests/sat/splice.ys b/tests/sat/splice.ys
new file mode 100644
index 000000000..365a4e2fd
--- /dev/null
+++ b/tests/sat/splice.ys
@@ -0,0 +1,14 @@
+read_verilog splice.v
+hierarchy -check; opt
+copy test gold
+
+cd test
+splice
+# show
+
+cd ..
+rename test gate
+miter -equiv -make_assert -make_outputs gold gate miter
+
+flatten miter
+sat -verify -prove-asserts -show-inputs -show-outputs miter