summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-09-01 16:35:25 +0200
committerClifford Wolf <clifford@clifford.at>2014-09-01 16:35:25 +0200
commitbae09dca2ba4d582bf7258b6419d4268f65f1476 (patch)
tree79d3122061fe89ad57084c47c98198e30cef5408
parent9923762461d2bc0822daef76bf0b58e772045bc8 (diff)
Added SAT model for $alu cells
-rw-r--r--kernel/satgen.h71
1 files changed, 69 insertions, 2 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h
index 5d1c11c9..beb03768 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -183,9 +183,9 @@ struct SatGen
bool importCell(RTLIL::Cell *cell, int timestep = -1)
{
bool arith_undef_handled = false;
- bool is_arith_compare = cell->type == "$lt" || cell->type == "$le" || cell->type == "$ge" || cell->type == "$gt";
+ bool is_arith_compare = cell->type.in("$lt", "$le", "$ge", "$gt");
- if (model_undef && (cell->type == "$add" || cell->type == "$sub" || cell->type == "$mul" || cell->type == "$div" || cell->type == "$mod" || is_arith_compare))
+ if (model_undef && (cell->type.in("$add", "$sub", "$mul", "$div", "$mod") || is_arith_compare))
{
std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
@@ -891,6 +891,73 @@ struct SatGen
return true;
}
+ if (cell->type == "$alu")
+ {
+ std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep);
+ std::vector<int> b = importDefSigSpec(cell->getPort("\\B"), timestep);
+ std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
+ std::vector<int> x = importDefSigSpec(cell->getPort("\\X"), timestep);
+ std::vector<int> ci = importDefSigSpec(cell->getPort("\\CI"), timestep);
+ std::vector<int> bi = importDefSigSpec(cell->getPort("\\BI"), timestep);
+ std::vector<int> co = importDefSigSpec(cell->getPort("\\CO"), timestep);
+
+ extendSignalWidth(a, b, y, cell);
+ extendSignalWidth(a, b, x, cell);
+ extendSignalWidth(a, b, co, cell);
+
+ std::vector<int> def_y = model_undef ? ez->vec_var(y.size()) : y;
+ std::vector<int> def_x = model_undef ? ez->vec_var(x.size()) : x;
+ std::vector<int> def_co = model_undef ? ez->vec_var(co.size()) : co;
+
+ log_assert(SIZE(y) == SIZE(x));
+ log_assert(SIZE(y) == SIZE(co));
+ log_assert(SIZE(ci) == 1);
+ log_assert(SIZE(bi) == 1);
+
+ for (int i = 0; i < SIZE(y); i++)
+ {
+ int s1 = a.at(i), s2 = ez->XOR(b.at(i), bi.at(0)), s3 = i ? co.at(i-1) : ci.at(0);
+ ez->SET(def_x.at(i), ez->XOR(s1, s2));
+ ez->SET(def_y.at(i), ez->XOR(def_x.at(i), s3));
+ ez->SET(def_co.at(i), ez->OR(ez->AND(s1, s2), ez->AND(s1, s3), ez->AND(s2, s3)));
+ }
+
+ if (model_undef)
+ {
+ std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep);
+ std::vector<int> undef_b = importUndefSigSpec(cell->getPort("\\B"), timestep);
+ std::vector<int> undef_ci = importUndefSigSpec(cell->getPort("\\CI"), timestep);
+ std::vector<int> undef_bi = importUndefSigSpec(cell->getPort("\\BI"), timestep);
+
+ std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
+ std::vector<int> undef_x = importUndefSigSpec(cell->getPort("\\X"), timestep);
+ std::vector<int> undef_co = importUndefSigSpec(cell->getPort("\\CO"), timestep);
+
+ extendSignalWidth(undef_a, undef_b, undef_y, cell, true);
+ extendSignalWidth(undef_a, undef_b, undef_x, cell, true);
+ extendSignalWidth(undef_a, undef_b, undef_co, cell, true);
+
+ std::vector<int> all_inputs_undef;
+ all_inputs_undef.insert(all_inputs_undef.end(), undef_a.begin(), undef_a.end());
+ all_inputs_undef.insert(all_inputs_undef.end(), undef_b.begin(), undef_b.end());
+ all_inputs_undef.insert(all_inputs_undef.end(), undef_ci.begin(), undef_ci.end());
+ all_inputs_undef.insert(all_inputs_undef.end(), undef_bi.begin(), undef_bi.end());
+ int undef_any = ez->expression(ezSAT::OpOr, all_inputs_undef);
+
+ for (int i = 0; i < SIZE(undef_y); i++) {
+ ez->SET(undef_y.at(i), undef_any);
+ ez->SET(undef_x.at(i), ez->OR(undef_a.at(i), undef_b.at(i), undef_bi.at(0)));
+ ez->SET(undef_co.at(i), undef_any);
+ }
+
+ undefGating(y, def_y, undef_y);
+ undefGating(x, def_x, undef_x);
+ undefGating(co, def_co, undef_co);
+ }
+ log_ping();
+ return true;
+ }
+
if (cell->type == "$slice")
{
RTLIL::SigSpec a = cell->getPort("\\A");