diff options
| -rw-r--r-- | passes/techmap/muxcover.cc | 31 | ||||
| -rw-r--r-- | tests/various/muxcover.ys | 320 |
2 files changed, 345 insertions, 6 deletions
diff --git a/passes/techmap/muxcover.cc b/passes/techmap/muxcover.cc index b0722134e..c84cfc39a 100644 --- a/passes/techmap/muxcover.cc +++ b/passes/techmap/muxcover.cc @@ -81,6 +81,23 @@ struct MuxcoverWorker decode_mux_counter = 0; } + bool xcmp(std::initializer_list<SigBit> list) + { + auto cursor = list.begin(), end = list.end(); + log_assert(cursor != end); + SigBit tmp = *(cursor++); + while (cursor != end) { + SigBit bit = *(cursor++); + if (bit == State::Sx) + continue; + if (tmp == State::Sx) + tmp = bit; + if (bit != tmp) + return false; + } + return true; + } + void treeify() { pool<SigBit> roots; @@ -144,6 +161,8 @@ struct MuxcoverWorker if (tree.muxes.count(bit) == 0) { if (first_layer || nopartial) return false; + while (path[0] && path[1]) + path++; if (path[0] == 'S') ret_bit = State::Sx; else @@ -280,7 +299,7 @@ struct MuxcoverWorker ok = ok && follow_muxtree(S2, tree, bit, "BS"); if (nodecode) - ok = ok && S1 == S2; + ok = ok && xcmp({S1, S2}); ok = ok && follow_muxtree(T1, tree, bit, "S"); @@ -330,13 +349,13 @@ struct MuxcoverWorker ok = ok && follow_muxtree(S4, tree, bit, "BBS"); if (nodecode) - ok = ok && S1 == S2 && S2 == S3 && S3 == S4; + ok = ok && xcmp({S1, S2, S3, S4}); ok = ok && follow_muxtree(T1, tree, bit, "AS"); ok = ok && follow_muxtree(T2, tree, bit, "BS"); if (nodecode) - ok = ok && T1 == T2; + ok = ok && xcmp({T1, T2}); ok = ok && follow_muxtree(U1, tree, bit, "S"); @@ -407,7 +426,7 @@ struct MuxcoverWorker ok = ok && follow_muxtree(S8, tree, bit, "BBBS"); if (nodecode) - ok = ok && S1 == S2 && S2 == S3 && S3 == S4 && S4 == S5 && S5 == S6 && S6 == S7 && S7 == S8; + ok = ok && xcmp({S1, S2, S3, S4, S5, S6, S7, S8}); ok = ok && follow_muxtree(T1, tree, bit, "AAS"); ok = ok && follow_muxtree(T2, tree, bit, "ABS"); @@ -415,13 +434,13 @@ struct MuxcoverWorker ok = ok && follow_muxtree(T4, tree, bit, "BBS"); if (nodecode) - ok = ok && T1 == T2 && T2 == T3 && T3 == T4; + ok = ok && xcmp({T1, T2, T3, T4}); ok = ok && follow_muxtree(U1, tree, bit, "AS"); ok = ok && follow_muxtree(U2, tree, bit, "BS"); if (nodecode) - ok = ok && U1 == U2; + ok = ok && xcmp({U1, U2}); ok = ok && follow_muxtree(V1, tree, bit, "S"); diff --git a/tests/various/muxcover.ys b/tests/various/muxcover.ys index 8ef619b46..67e9625e6 100644 --- a/tests/various/muxcover.ys +++ b/tests/various/muxcover.ys @@ -188,3 +188,323 @@ design -import gate -as gate miter -equiv -flatten -make_assert -make_outputs gold gate miter sat -verify -prove-asserts -show-ports miter +## MUX2 in MUX4 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux2in4(input [1:0] i, input s, output o); + assign o = s ? i[1] : i[0]; +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux4=99 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 1 t:$_MUX4_ +select -assert-count 0 t:$_MUX8_ +select -assert-count 0 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX4_ +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 + +## MUX2 in MUX8 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux2in8(input [1:0] i, input s, output o); + assign o = s ? i[1] : i[0]; +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux8=99 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 1 t:$_MUX8_ +select -assert-count 0 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX8_ +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 + +## MUX4 in MUX8 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux4in8(input [3:0] i, input [1:0] s, output o); + assign o = s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0]); +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux8=299 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 1 t:$_MUX8_ +select -assert-count 0 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX8_ +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 + +## MUX2 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux2in16(input [1:0] i, input s, output o); + assign o = s ? i[1] : i[0]; +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux16=99 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 0 t:$_MUX8_ +select -assert-count 1 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX16_ +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 + +## MUX4 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux4in16(input [3:0] i, input [1:0] s, output o); + assign o = s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0]); +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux16=299 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 0 t:$_MUX8_ +select -assert-count 1 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX16_ +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 + +## MUX8 in MUX16 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux4in16(input [7:0] i, input [2:0] s, output o); + assign o = s[2] ? s[1] ? (s[0] ? i[3] : i[2]) : (s[0] ? i[1] : i[0]) + : s[1] ? (s[0] ? i[7] : i[6]) : (s[0] ? i[5] : i[4]); +endmodule +EOT +prep +design -save gold + +techmap +muxcover -mux16=699 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 0 t:$_MUX8_ +select -assert-count 1 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX16_ +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 + +## mux_if_bal_5_1 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux_if_bal_5_1 #(parameter N=5, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* begin + o <= {{W{{1'bx}}}}; + if (s[0] == 1'b0) + if (s[1] == 1'b0) + if (s[2] == 1'b0) + o <= i[0*W+:W]; + else + o <= i[1*W+:W]; + else + if (s[2] == 1'b0) + o <= i[2*W+:W]; + else + o <= i[3*W+:W]; + else + if (s[1] == 1'b0) + if (s[2] == 1'b0) + o <= i[4*W+:W]; +end +endmodule +EOT +prep +design -save gold + +wreduce +opt -full +techmap +muxcover -mux8=350 +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 1 t:$_MUX8_ +select -assert-count 0 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX8_ +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter +sat -verify -prove-asserts -show-ports miter + +## mux_if_bal_5_1 (nodecode) :: https://github.com/YosysHQ/yosys/issues/1132 +design -load gold + +wreduce +opt -full +techmap +muxcover -mux8=350 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 1 t:$_MUX8_ +select -assert-count 0 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX8_ +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter +sat -verify -prove-asserts -show-ports miter + +## mux_if_bal_9_1 :: https://github.com/YosysHQ/yosys/issues/1132 + +design -reset +read_verilog -formal <<EOT +module mux_if_bal_9_1 #(parameter N=9, parameter W=1) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output reg [W-1:0] o); +always @* begin + o <= {{W{{1'bx}}}}; + if (s[3] == 1'b0) + if (s[2] == 1'b0) + if (s[1] == 1'b0) + if (s[0] == 1'b0) + o <= i[0*W+:W]; + else + o <= i[1*W+:W]; + else + if (s[0] == 1'b0) + o <= i[2*W+:W]; + else + o <= i[3*W+:W]; + else + if (s[1] == 1'b0) + if (s[0] == 1'b0) + o <= i[4*W+:W]; + else + o <= i[5*W+:W]; + else + if (s[0] == 1'b0) + o <= i[6*W+:W]; + else + o <= i[7*W+:W]; + else + if (s[2] == 1'b0) + if (s[1] == 1'b0) + if (s[0] == 1'b0) + o <= i[8*W+:W]; +end +endmodule +EOT +prep +design -save gold + +wreduce +opt -full +techmap +muxcover -mux16=750 +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 0 t:$_MUX8_ +select -assert-count 1 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX16_ +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter +sat -verify -prove-asserts -show-ports miter + +## mux_if_bal_9_1 (nodecode) :: https://github.com/YosysHQ/yosys/issues/1132 + +design -load gold + +wreduce +opt -full +techmap +muxcover -mux16=750 -nodecode +clean +opt_expr -mux_bool +select -assert-count 0 t:$_MUX_ +select -assert-count 0 t:$_MUX4_ +select -assert-count 0 t:$_MUX8_ +select -assert-count 1 t:$_MUX16_ +techmap -map +/simcells.v t:$_MUX16_ +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs -ignore_gold_x gold gate miter +sat -verify -prove-asserts -show-ports miter |