summaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2013-12-27 14:20:15 +0100
committerClifford Wolf <clifford@clifford.at>2013-12-27 14:20:15 +0100
commit369bf81a7049c96f62af084bb5007fbf45e36ab4 (patch)
tree92071580c9bd60888ee5861d59457947a8adfde7 /kernel
parentecc30255ba70910777a4586f5bd6abc818073293 (diff)
Added support for non-const === and !== (for miter circuits)
Diffstat (limited to 'kernel')
-rw-r--r--kernel/celltypes.h4
-rw-r--r--kernel/rtlil.cc2
-rw-r--r--kernel/satgen.h20
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);