summaryrefslogtreecommitdiff
path: root/tests/sat
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-07-20 20:45:01 +0200
committerClifford Wolf <clifford@clifford.at>2014-07-20 21:15:01 +0200
commit8836943693dcd6fc6e6b74141ca8c89e9b8c1f0e (patch)
tree03acce68a697965c56f9e59ce72c4778a2d14c72 /tests/sat
parent04fcb07213291f469d208ceca2a32fb8c2fe3215 (diff)
Added yet another resource sharing test case
Diffstat (limited to 'tests/sat')
-rw-r--r--tests/sat/share.v32
-rw-r--r--tests/sat/share.ys17
2 files changed, 49 insertions, 0 deletions
diff --git a/tests/sat/share.v b/tests/sat/share.v
new file mode 100644
index 00000000..e06fc8f1
--- /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 00000000..f2f5d649
--- /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
+