Added yet another resource sharing test case

This commit is contained in:
Clifford Wolf 2014-07-20 20:45:01 +02:00
parent 04fcb07213
commit 8836943693
2 changed files with 49 additions and 0 deletions

32
tests/sat/share.v Normal file
View File

@ -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

17
tests/sat/share.ys Normal file
View File

@ -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