diff options
| -rw-r--r-- | kernel/satgen.h | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h index 53921044..d9bcb425 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -385,7 +385,7 @@ struct SatGen 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> 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; - if (cell->type == "$pos") { + if (cell->type == "$pos" || cell->type == "$bu0") { ez->assume(ez->vec_eq(a, yy)); } else { 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_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)); } else { int undef_any_a = ez->expression(ezSAT::OpOr, undef_a); |