Added support for $bu0 to SatGen

This commit is contained in:
Clifford Wolf 2014-02-26 21:31:34 +01:00
parent 6bc94b7eb2
commit aaaa604853
1 changed files with 4 additions and 4 deletions

View File

@ -385,7 +385,7 @@ struct SatGen
return true; return true;
} }
if (cell->type == "$pos" || cell->type == "$neg") if (cell->type == "$pos" || cell->type == "$bu0" || cell->type == "$neg")
{ {
std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep); std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep);
std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep); std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
@ -393,7 +393,7 @@ 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 (cell->type == "$pos") { if (cell->type == "$pos" || cell->type == "$bu0") {
ez->assume(ez->vec_eq(a, yy)); ez->assume(ez->vec_eq(a, yy));
} else { } else {
std::vector<int> zero(a.size(), ez->FALSE); std::vector<int> zero(a.size(), ez->FALSE);
@ -404,9 +404,9 @@ 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_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep); std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
extendSignalWidthUnary(undef_a, undef_y, cell, true); extendSignalWidthUnary(undef_a, undef_y, cell, cell->type != "$bu0");
if (cell->type == "$pos") { if (cell->type == "$pos" || cell->type == "$bu0") {
ez->assume(ez->vec_eq(undef_a, undef_y)); ez->assume(ez->vec_eq(undef_a, undef_y));
} else { } else {
int undef_any_a = ez->expression(ezSAT::OpOr, undef_a); int undef_any_a = ez->expression(ezSAT::OpOr, undef_a);