mirror of https://github.com/YosysHQ/yosys.git
Merge remote-tracking branch 'origin/eddie/fix1132' into xc7mux
This commit is contained in:
commit
90750e43ef
|
@ -151,7 +151,7 @@ struct MuxcoverWorker
|
|||
return true;
|
||||
}
|
||||
char port_name[3] = {'\\', *path, 0};
|
||||
return follow_muxtree(ret_bit, tree, sigmap(tree.muxes.at(bit)->getPort(port_name)), path+1, false);
|
||||
return follow_muxtree(ret_bit, tree, tree.muxes.at(bit)->getPort(port_name), path+1, false);
|
||||
} else {
|
||||
ret_bit = bit;
|
||||
return true;
|
||||
|
@ -160,7 +160,7 @@ struct MuxcoverWorker
|
|||
|
||||
int prepare_decode_mux(SigBit &A, SigBit B, SigBit sel, SigBit bit)
|
||||
{
|
||||
if (A == B || sel == State::Sx)
|
||||
if (A == B || sel == State::Sx || A == State::Sx || B == State::Sx)
|
||||
return 0;
|
||||
|
||||
tuple<SigBit, SigBit, SigBit> key(A, B, sel);
|
||||
|
@ -324,22 +324,23 @@ struct MuxcoverWorker
|
|||
ok = ok && follow_muxtree(G, tree, bit, "BBA");
|
||||
ok = ok && follow_muxtree(H, tree, bit, "BBB");
|
||||
|
||||
ok = ok && follow_muxtree(U1, tree, bit, "S");
|
||||
|
||||
ok = ok && follow_muxtree(T1, tree, bit, "AS");
|
||||
ok = ok && follow_muxtree(T2, tree, bit, "BS");
|
||||
|
||||
if (nodecode)
|
||||
ok = ok && T1 == T2;
|
||||
|
||||
ok = ok && follow_muxtree(S1, tree, bit, "AAS");
|
||||
ok = ok && follow_muxtree(S2, tree, bit, "ABS");
|
||||
ok = ok && follow_muxtree(S3, tree, bit, "BAS");
|
||||
ok = ok && follow_muxtree(S4, tree, bit, "BBS");
|
||||
|
||||
if (nodecode)
|
||||
ok = ok && S1 == S2 && /*S2 == S3 &&*/ S3 == S4;
|
||||
// ^^ Should already be checked by T1 == T2 above
|
||||
ok = ok && (S1 == S2 || S1 == State::Sx || S2 == State::Sx) &&
|
||||
/*S2 == S3 && */
|
||||
(S3 == S4 || S3 == State::Sx || S4 == State::Sx);
|
||||
|
||||
ok = ok && follow_muxtree(T1, tree, bit, "AS");
|
||||
ok = ok && follow_muxtree(T2, tree, bit, "BS");
|
||||
|
||||
if (nodecode)
|
||||
ok = ok && (T1 == T2 || T1 == State::Sx || T2 == State::Sx);
|
||||
|
||||
ok = ok && follow_muxtree(U1, tree, bit, "S");
|
||||
|
||||
if (ok)
|
||||
{
|
||||
|
@ -356,13 +357,10 @@ struct MuxcoverWorker
|
|||
|
||||
mux.cost += prepare_decode_mux(T1, T2, U1, bit);
|
||||
|
||||
if (T1 != RTLIL::Sx) {
|
||||
mux.cost += prepare_decode_mux(S1, S2, T1, bit);
|
||||
mux.cost += prepare_decode_mux(S3, S4, T2, bit);
|
||||
mux.cost += prepare_decode_mux(S1, S2, T1, bit);
|
||||
mux.cost += prepare_decode_mux(S3, S4, T2, bit);
|
||||
if (T1 != T2 && T1 != State::Sx && T2 != State::Sx)
|
||||
mux.cost += prepare_decode_mux(S1, S3, U1, bit);
|
||||
}
|
||||
else
|
||||
S1 = RTLIL::Sx;
|
||||
|
||||
mux.selects.push_back(S1);
|
||||
mux.selects.push_back(T1);
|
||||
|
@ -402,23 +400,6 @@ struct MuxcoverWorker
|
|||
ok = ok && follow_muxtree(O, tree, bit, "BBBA");
|
||||
ok = ok && follow_muxtree(P, tree, bit, "BBBB");
|
||||
|
||||
ok = ok && follow_muxtree(V1, tree, bit, "S");
|
||||
|
||||
ok = ok && follow_muxtree(U1, tree, bit, "AS");
|
||||
ok = ok && follow_muxtree(U2, tree, bit, "BS");
|
||||
|
||||
if (nodecode)
|
||||
ok = ok && U1 == U2;
|
||||
|
||||
ok = ok && follow_muxtree(T1, tree, bit, "AAS");
|
||||
ok = ok && follow_muxtree(T2, tree, bit, "ABS");
|
||||
ok = ok && follow_muxtree(T3, tree, bit, "BAS");
|
||||
ok = ok && follow_muxtree(T4, tree, bit, "BBS");
|
||||
|
||||
if (nodecode)
|
||||
ok = ok && T1 == T2 && /*T2 == T3 &&*/ T3 == T4;
|
||||
// ^^ Should already be checked by U1 == U2 above
|
||||
|
||||
ok = ok && follow_muxtree(S1, tree, bit, "AAAS");
|
||||
ok = ok && follow_muxtree(S2, tree, bit, "AABS");
|
||||
ok = ok && follow_muxtree(S3, tree, bit, "ABAS");
|
||||
|
@ -429,7 +410,31 @@ 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 && (S1 == S2 || S1 == State::Sx || S2 == State::Sx) &&
|
||||
/*S2 == S3 &&*/
|
||||
(S3 == S4 || S3 == State::Sx || S4 == State::Sx) &&
|
||||
/*S4 == S5 &&*/
|
||||
(S5 == S6 || S5 == State::Sx || S6 == State::Sx) &&
|
||||
/*S6 == S7 &&*/
|
||||
(S7 == S8 || S7 == State::Sx || S8 == State::Sx);
|
||||
|
||||
ok = ok && follow_muxtree(T1, tree, bit, "AAS");
|
||||
ok = ok && follow_muxtree(T2, tree, bit, "ABS");
|
||||
ok = ok && follow_muxtree(T3, tree, bit, "BAS");
|
||||
ok = ok && follow_muxtree(T4, tree, bit, "BBS");
|
||||
|
||||
if (nodecode)
|
||||
ok = ok && (T1 == T2 || T1 == State::Sx || T2 == State::Sx) &&
|
||||
/*T2 == T3 &&*/
|
||||
(T3 == T4 || T3 == State::Sx || T4 == State::Sx);
|
||||
|
||||
ok = ok && follow_muxtree(U1, tree, bit, "AS");
|
||||
ok = ok && follow_muxtree(U2, tree, bit, "BS");
|
||||
|
||||
if (nodecode)
|
||||
ok = ok && (U1 == U2 || U1 == State::Sx || U2 == State::Sx);
|
||||
|
||||
ok = ok && follow_muxtree(V1, tree, bit, "S");
|
||||
|
||||
if (ok)
|
||||
{
|
||||
|
@ -454,27 +459,25 @@ struct MuxcoverWorker
|
|||
|
||||
mux.cost += prepare_decode_mux(U1, U2, V1, bit);
|
||||
|
||||
if (U1 != RTLIL::Sx) {
|
||||
if (U1 != State::Sx && U2 != State::Sx) {
|
||||
mux.cost += prepare_decode_mux(T1, T2, U1, bit);
|
||||
mux.cost += prepare_decode_mux(T3, T4, U2, bit);
|
||||
mux.cost += prepare_decode_mux(T1, T3, V1, bit);
|
||||
}
|
||||
|
||||
if (T1 != RTLIL::Sx) {
|
||||
mux.cost += prepare_decode_mux(S1, S2, T1, bit);
|
||||
mux.cost += prepare_decode_mux(S3, S4, T2, bit);
|
||||
mux.cost += prepare_decode_mux(S5, S6, T3, bit);
|
||||
mux.cost += prepare_decode_mux(S7, S8, T4, bit);
|
||||
mux.cost += prepare_decode_mux(S1, S3, U1, bit);
|
||||
mux.cost += prepare_decode_mux(S5, S7, U2, bit);
|
||||
mux.cost += prepare_decode_mux(S1, S5, V1, bit);
|
||||
}
|
||||
else
|
||||
S1 = RTLIL::Sx;
|
||||
if (T1 != T2 && T1 != State::Sx && T2 != State::Sx) {
|
||||
mux.cost += prepare_decode_mux(S1, S2, T1, bit);
|
||||
mux.cost += prepare_decode_mux(S3, S4, T2, bit);
|
||||
mux.cost += prepare_decode_mux(S1, S3, U1, bit);
|
||||
}
|
||||
else {
|
||||
T1 = RTLIL::Sx;
|
||||
S1 = RTLIL::Sx;
|
||||
if (T3 != T4 && T3 != State::Sx && T4 != State::Sx) {
|
||||
mux.cost += prepare_decode_mux(S5, S6, T3, bit);
|
||||
mux.cost += prepare_decode_mux(S7, S8, T4, bit);
|
||||
mux.cost += prepare_decode_mux(S5, S7, U2, bit);
|
||||
}
|
||||
if (T1 != T2 && T1 != State::Sx && T2 != State::Sx &&
|
||||
T3 != T4 && T3 != State::Sx && T4 != State::Sx)
|
||||
mux.cost += prepare_decode_mux(S1, S5, V1, bit);
|
||||
|
||||
mux.selects.push_back(S1);
|
||||
mux.selects.push_back(T1);
|
||||
|
|
|
@ -200,7 +200,7 @@ prep
|
|||
design -save gold
|
||||
|
||||
techmap
|
||||
muxcover -mux4=0 -nodecode
|
||||
muxcover -mux4=99 -nodecode
|
||||
clean
|
||||
opt_expr -mux_bool
|
||||
select -assert-count 0 t:$_MUX_
|
||||
|
@ -228,7 +228,7 @@ prep
|
|||
design -save gold
|
||||
|
||||
techmap
|
||||
muxcover -mux8=0 -nodecode
|
||||
muxcover -mux8=99 -nodecode
|
||||
clean
|
||||
opt_expr -mux_bool
|
||||
select -assert-count 0 t:$_MUX_
|
||||
|
@ -256,7 +256,7 @@ prep
|
|||
design -save gold
|
||||
|
||||
techmap
|
||||
muxcover -mux8=0 -nodecode
|
||||
muxcover -mux8=299 -nodecode
|
||||
clean
|
||||
opt_expr -mux_bool
|
||||
select -assert-count 0 t:$_MUX_
|
||||
|
@ -284,7 +284,7 @@ prep
|
|||
design -save gold
|
||||
|
||||
techmap
|
||||
muxcover -mux16=0 -nodecode
|
||||
muxcover -mux16=99 -nodecode
|
||||
clean
|
||||
opt_expr -mux_bool
|
||||
select -assert-count 0 t:$_MUX_
|
||||
|
@ -312,7 +312,7 @@ prep
|
|||
design -save gold
|
||||
|
||||
techmap
|
||||
muxcover -mux16=0 -nodecode
|
||||
muxcover -mux16=299 -nodecode
|
||||
clean
|
||||
opt_expr -mux_bool
|
||||
select -assert-count 0 t:$_MUX_
|
||||
|
@ -341,7 +341,7 @@ prep
|
|||
design -save gold
|
||||
|
||||
techmap
|
||||
muxcover -mux16=0 -nodecode
|
||||
muxcover -mux16=699 -nodecode
|
||||
clean
|
||||
opt_expr -mux_bool
|
||||
select -assert-count 0 t:$_MUX_
|
||||
|
@ -356,3 +356,155 @@ 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
|
||||
|
|
Loading…
Reference in New Issue