summaryrefslogtreecommitdiff
path: root/tests
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-02-07 20:26:40 +0100
committerClifford Wolf <clifford@clifford.at>2014-02-07 20:30:56 +0100
commit244e8ce1f42bce47b3426e6679ed0ba5dadd8da6 (patch)
treeb374e5f99803bc2e991c965e4ac3b69280c265b6 /tests
parent08aa1062b4fbaa507091b9015811104d93da3315 (diff)
Added splice command
Diffstat (limited to 'tests')
-rw-r--r--tests/sat/splice.v14
-rw-r--r--tests/sat/splice.ys14
2 files changed, 28 insertions, 0 deletions
diff --git a/tests/sat/splice.v b/tests/sat/splice.v
new file mode 100644
index 00000000..8d1dcd22
--- /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 00000000..365a4e2f
--- /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