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

Fixed sat handling of $eqx and $nex cells

This commit is contained in:
Clifford Wolf 2013-12-27 14:32:42 +01:00
parent 7b02a44efb
commit ebf9abfeb6
1 changed files with 12 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

13
kernel/satgen.h
View File

@ -461,6 +461,13 @@ struct SatGen
std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y; std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
if (model_undef && (cell->type == "$eqx" || cell->type == "$nex")) {
std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
a = ez->vec_or(a, undef_a);
b = ez->vec_or(b, undef_b);
}
if (cell->type == "$lt") if (cell->type == "$lt")
ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), yy.at(0)); ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), yy.at(0));
if (cell->type == "$le") if (cell->type == "$le")
@ -481,7 +488,11 @@ struct SatGen
std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep); std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep);
std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep); std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep);
std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep); std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
if (cell->type == "$eqx")
yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
else
yy.at(0) = ez->OR(yy.at(0), ez->vec_ne(undef_a, undef_b));
for (size_t i = 0; i < y.size(); i++) for (size_t i = 0; i < y.size(); i++)
ez->SET(ez->FALSE, undef_y.at(i)); ez->SET(ez->FALSE, undef_y.at(i));