From 244e8ce1f42bce47b3426e6679ed0ba5dadd8da6 Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Fri, 7 Feb 2014 20:26:40 +0100
Subject: Added splice command

---
 tests/sat/splice.v  | 14 ++++++++++++++
 tests/sat/splice.ys | 14 ++++++++++++++
 2 files changed, 28 insertions(+)
 create mode 100644 tests/sat/splice.v
 create mode 100644 tests/sat/splice.ys

(limited to 'tests')

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
-- 
cgit v1.2.3