riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

satgen, simlib: Consistent x-propagation for `$pmux` cells 

This updates satgen and simlib to use a `$pmux` model where the output
is fully X when the S input is not all zero or one-hot with no x bits.
This commit is contained in:
Jannis Harder 2022-11-10 16:17:54 +01:00
parent 1e67c3a3c2
commit b982ab4f59
2 changed files with 20 additions and 18 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

23
kernel/satgen.cc
View File

@ -375,29 +375,24 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
std::vector<int> undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep); std::vector<int> undef_s = importUndefSigSpec(cell->getPort(ID::S), timestep);
std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep); std::vector<int> undef_y = importUndefSigSpec(cell->getPort(ID::Y), timestep);
int maybe_a = ez->CONST_TRUE; int all_undef = ez->CONST_FALSE;
int found_active = ez->CONST_FALSE;
std::vector<int> bits_set = std::vector<int>(undef_y.size(), ez->CONST_FALSE); std::vector<int> undef_tmp = undef_a;
std::vector<int> bits_clr = std::vector<int>(undef_y.size(), ez->CONST_FALSE);
for (size_t i = 0; i < s.size(); i++) for (size_t i = 0; i < s.size(); i++)
{ {
std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
std::vector<int> part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size()); std::vector<int> part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size());
int maybe_s = ez->OR(s.at(i), undef_s.at(i)); undef_tmp = ez->vec_ite(s.at(i), part_of_undef_b, undef_tmp);
int sure_s = ez->AND(s.at(i), ez->NOT(undef_s.at(i))); all_undef = ez->OR(all_undef, undef_s.at(i));
all_undef = ez->OR(all_undef, ez->AND(s.at(i), found_active));
maybe_a = ez->AND(maybe_a, ez->NOT(sure_s)); found_active = ez->OR(found_active, s.at(i));
bits_set = ez->vec_ite(maybe_s, ez->vec_or(bits_set, ez->vec_or(part_of_b, part_of_undef_b)), bits_set);
bits_clr = ez->vec_ite(maybe_s, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(part_of_b), part_of_undef_b)), bits_clr);
} }
bits_set = ez->vec_ite(maybe_a, ez->vec_or(bits_set, ez->vec_or(bits_set, ez->vec_or(a, undef_a))), bits_set); undef_tmp = ez->vec_or(undef_tmp, std::vector<int>(a.size(), all_undef));
bits_clr = ez->vec_ite(maybe_a, ez->vec_or(bits_clr, ez->vec_or(bits_clr, ez->vec_or(ez->vec_not(a), undef_a))), bits_clr);
ez->assume(ez->vec_eq(ez->vec_not(ez->vec_xor(bits_set, bits_clr)), undef_y)); ez->assume(ez->vec_eq(undef_tmp, undef_y));
undefGating(y, yy, undef_y); undefGating(y, yy, undef_y);
} }
return true; return true;

15
techlibs/common/simlib.v
View File

@ -1331,10 +1331,17 @@ always @* begin
Y = A; Y = A;
found_active_sel_bit = 0; found_active_sel_bit = 0;
for (i = 0; i < S_WIDTH; i = i+1) for (i = 0; i < S_WIDTH; i = i+1)
if (S[i]) begin case (S[i])
Y = found_active_sel_bit ? 'bx : B >> (WIDTH*i); 1'b1: begin
found_active_sel_bit = 1; Y = found_active_sel_bit ? 'bx : B >> (WIDTH*i);
end found_active_sel_bit = 1;
end
1'b0: ;
1'bx: begin
Y = 'bx;
found_active_sel_bit = 'bx;
end
endcase
end end
endmodule endmodule