diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/celltypes.h | 4 | ||||
| -rw-r--r-- | kernel/rtlil.cc | 2 | ||||
| -rw-r--r-- | kernel/satgen.h | 20 |
3 files changed, 21 insertions, 5 deletions
diff --git a/kernel/celltypes.h b/kernel/celltypes.h index e59f74d6..29eb490f 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -78,6 +78,8 @@ struct CellTypes cell_types.insert("$le"); cell_types.insert("$eq"); cell_types.insert("$ne"); + cell_types.insert("$eqx"); + cell_types.insert("$nex"); cell_types.insert("$ge"); cell_types.insert("$gt"); cell_types.insert("$add"); @@ -237,6 +239,8 @@ struct CellTypes HANDLE_CELL_TYPE(le) HANDLE_CELL_TYPE(eq) HANDLE_CELL_TYPE(ne) + HANDLE_CELL_TYPE(eqx) + HANDLE_CELL_TYPE(nex) HANDLE_CELL_TYPE(ge) HANDLE_CELL_TYPE(gt) HANDLE_CELL_TYPE(add) diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index 9dfe196d..47dc098a 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -408,7 +408,7 @@ namespace { } if (cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" || - cell->type == "$ge" || cell->type == "$gt") { + cell->type == "$eqx" || cell->type == "$nex" || cell->type == "$ge" || cell->type == "$gt") { param("\\A_SIGNED"); param("\\B_SIGNED"); port("\\A", param("\\A_WIDTH")); diff --git a/kernel/satgen.h b/kernel/satgen.h index 35e15aa6..c0807f55 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -451,7 +451,7 @@ struct SatGen return true; } - if (cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" || cell->type == "$ge" || cell->type == "$gt") + if (cell->type == "$lt" || cell->type == "$le" || cell->type == "$eq" || cell->type == "$ne" || cell->type == "$eqx" || cell->type == "$nex" || cell->type == "$ge" || cell->type == "$gt") { bool is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool(); std::vector<int> a = importDefSigSpec(cell->connections.at("\\A"), timestep); @@ -465,9 +465,9 @@ struct SatGen ez->SET(is_signed ? ez->vec_lt_signed(a, b) : ez->vec_lt_unsigned(a, b), yy.at(0)); if (cell->type == "$le") ez->SET(is_signed ? ez->vec_le_signed(a, b) : ez->vec_le_unsigned(a, b), yy.at(0)); - if (cell->type == "$eq") + if (cell->type == "$eq" || cell->type == "$eqx") ez->SET(ez->vec_eq(a, b), yy.at(0)); - if (cell->type == "$ne") + if (cell->type == "$ne" || cell->type == "$nex") ez->SET(ez->vec_ne(a, b), yy.at(0)); if (cell->type == "$ge") ez->SET(is_signed ? ez->vec_ge_signed(a, b) : ez->vec_ge_unsigned(a, b), yy.at(0)); @@ -476,7 +476,19 @@ struct SatGen for (size_t i = 1; i < y.size(); i++) ez->SET(ez->FALSE, yy.at(i)); - if (model_undef && (cell->type == "$eq" || cell->type == "$ne")) + 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); + 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)); + + for (size_t i = 0; i < y.size(); i++) + ez->SET(ez->FALSE, undef_y.at(i)); + + ez->assume(ez->vec_eq(y, yy)); + } + else if (model_undef && (cell->type == "$eq" || cell->type == "$ne")) { std::vector<int> undef_a = importUndefSigSpec(cell->connections.at("\\A"), timestep); std::vector<int> undef_b = importUndefSigSpec(cell->connections.at("\\B"), timestep); |