summaryrefslogtreecommitdiff
path: root/kernel/satgen.h
diff options
context:
space:
mode:
Diffstat (limited to 'kernel/satgen.h')
-rw-r--r--kernel/satgen.h8
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);