From 4c831d72ef2d3a9f9b91d6fa27e09800ae09e869 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 19 Apr 2019 20:23:09 +0200 Subject: [PATCH] Add test for pmux2shiftx Signed-off-by: Clifford Wolf --- tests/various/pmux2shiftx.v | 28 ++++++++++++++++++++++++++++ tests/various/pmux2shiftx.ys | 24 ++++++++++++++++++++++++ 2 files changed, 52 insertions(+) create mode 100644 tests/various/pmux2shiftx.v create mode 100644 tests/various/pmux2shiftx.ys diff --git a/tests/various/pmux2shiftx.v b/tests/various/pmux2shiftx.v new file mode 100644 index 000000000..ac61c5c0e --- /dev/null +++ b/tests/various/pmux2shiftx.v @@ -0,0 +1,28 @@ +module pmux2shiftx_test ( + input [2:0] S1, + input [5:0] S2, + input [9:0] A, B, C, D, D, E, F, + input [9:0] G, H, I, J, K, L, M, N, + output reg [9:0] X +); + always @* begin + case (S1) + 3'd0: X = A; + 3'd1: X = B; + 3'd2: X = C; + 3'd3: X = D; + 3'd4: X = E; + 3'd5: X = F; + 3'd6: X = G; + 3'd7: X = H; + endcase + case (S2) + 6'd46: X = I; + 6'd47: X = J; + 6'd48: X = K; + 6'd52: X = L; + 6'd53: X = M; + 6'd54: X = N; + endcase + end +endmodule diff --git a/tests/various/pmux2shiftx.ys b/tests/various/pmux2shiftx.ys new file mode 100644 index 000000000..16618ac0a --- /dev/null +++ b/tests/various/pmux2shiftx.ys @@ -0,0 +1,24 @@ +read_verilog pmux2shiftx.v +prep +design -save gold + +pmux2shiftx +opt +# show -width +select -assert-count 1 t:$mux +select -assert-count 1 t:$shift +select -assert-count 2 t:$shiftx +select -assert-count 1 t:$sub +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports miter + +design -load gold +stat + +design -load gate +stat -- 2.30.2