aboutsummaryrefslogtreecommitdiffstats
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/calc.cc37
-rw-r--r--kernel/celltypes.h6
-rw-r--r--kernel/log.h54
-rw-r--r--kernel/rtlil.cc20
-rw-r--r--kernel/rtlil.h3
-rw-r--r--kernel/satgen.h85
6 files changed, 173 insertions, 32 deletions
diff --git a/kernel/calc.cc b/kernel/calc.cc
index 61025104d..a56db93aa 100644
--- a/kernel/calc.cc
+++ b/kernel/calc.cc
@@ -386,6 +386,35 @@ RTLIL::Const RTLIL::const_ne(const RTLIL::Const &arg1, const RTLIL::Const &arg2,
return result;
}
+RTLIL::Const RTLIL::const_eqx(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
+{
+ RTLIL::Const arg1_ext = arg1;
+ RTLIL::Const arg2_ext = arg2;
+ RTLIL::Const result(RTLIL::State::S0, result_len);
+
+ int width = std::max(arg1_ext.bits.size(), arg2_ext.bits.size());
+ extend_u0(arg1_ext, width, signed1 && signed2);
+ extend_u0(arg2_ext, width, signed1 && signed2);
+
+ for (size_t i = 0; i < arg1_ext.bits.size(); i++) {
+ if (arg1_ext.bits.at(i) != arg2_ext.bits.at(i))
+ return result;
+ }
+
+ result.bits.front() = RTLIL::State::S1;
+ return result;
+}
+
+RTLIL::Const RTLIL::const_nex(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
+{
+ RTLIL::Const result = RTLIL::const_eqx(arg1, arg2, signed1, signed2, result_len);
+ if (result.bits.front() == RTLIL::State::S0)
+ result.bits.front() = RTLIL::State::S1;
+ else if (result.bits.front() == RTLIL::State::S1)
+ result.bits.front() = RTLIL::State::S0;
+ return result;
+}
+
RTLIL::Const RTLIL::const_ge(const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len)
{
int undef_bit_pos = -1;
@@ -514,6 +543,14 @@ RTLIL::Const RTLIL::const_pos(const RTLIL::Const &arg1, const RTLIL::Const&, boo
return arg1_ext;
}
+RTLIL::Const RTLIL::const_bu0(const RTLIL::Const &arg1, const RTLIL::Const&, bool signed1, bool, int result_len)
+{
+ RTLIL::Const arg1_ext = arg1;
+ extend_u0(arg1_ext, result_len, signed1);
+
+ return arg1_ext;
+}
+
RTLIL::Const RTLIL::const_neg(const RTLIL::Const &arg1, const RTLIL::Const&, bool signed1, bool, int result_len)
{
RTLIL::Const arg1_ext = arg1;
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index e59f74d66..2f311c826 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -60,6 +60,7 @@ struct CellTypes
{
cell_types.insert("$not");
cell_types.insert("$pos");
+ cell_types.insert("$bu0");
cell_types.insert("$neg");
cell_types.insert("$and");
cell_types.insert("$or");
@@ -78,6 +79,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 +240,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)
@@ -246,6 +251,7 @@ struct CellTypes
HANDLE_CELL_TYPE(mod)
HANDLE_CELL_TYPE(pow)
HANDLE_CELL_TYPE(pos)
+ HANDLE_CELL_TYPE(bu0)
HANDLE_CELL_TYPE(neg)
#undef HANDLE_CELL_TYPE
diff --git a/kernel/log.h b/kernel/log.h
index d88dda889..5ee6b5651 100644
--- a/kernel/log.h
+++ b/kernel/log.h
@@ -93,4 +93,58 @@ struct PerformanceTimer
#endif
};
+// simple API for quickly dumping values when debugging
+
+static inline void log_dump_val_worker(int v) { log("%d", v); }
+static inline void log_dump_val_worker(size_t v) { log("%zd", v); }
+static inline void log_dump_val_worker(long int v) { log("%ld", v); }
+static inline void log_dump_val_worker(long long int v) { log("%lld", v); }
+static inline void log_dump_val_worker(char c) { log(c >= 32 && c < 127 ? "'%c'" : "'\\x%02x'", c); }
+static inline void log_dump_val_worker(bool v) { log("%s", v ? "true" : "false"); }
+static inline void log_dump_val_worker(double v) { log("%f", v); }
+static inline void log_dump_val_worker(const char *v) { log("%s", v); }
+static inline void log_dump_val_worker(std::string v) { log("%s", v.c_str()); }
+static inline void log_dump_val_worker(RTLIL::SigSpec v) { log("%s", log_signal(v)); }
+static inline void log_dump_args_worker(const char *p) { log_assert(*p == 0); }
+
+template <typename T, typename ... Args>
+void log_dump_args_worker(const char *p, T first, Args ... args)
+{
+ int next_p_state = 0;
+ const char *next_p = p;
+ while (*next_p && (next_p_state != 0 || *next_p != ',')) {
+ if (*next_p == '"')
+ do {
+ next_p++;
+ while (*next_p == '\\' && *(next_p + 1))
+ next_p += 2;
+ } while (*next_p && *next_p != '"');
+ if (*next_p == '\'') {
+ next_p++;
+ if (*next_p == '\\')
+ next_p++;
+ if (*next_p)
+ next_p++;
+ }
+ if (*next_p == '(' || *next_p == '[' || *next_p == '{')
+ next_p_state++;
+ if ((*next_p == ')' || *next_p == ']' || *next_p == '}') && next_p_state > 0)
+ next_p_state--;
+ next_p++;
+ }
+ log("\n\t%.*s => ", int(next_p - p), p);
+ if (*next_p == ',')
+ next_p++;
+ while (*next_p == ' ' || *next_p == '\t' || *next_p == '\r' || *next_p == '\n')
+ next_p++;
+ log_dump_val_worker(first);
+ log_dump_args_worker(next_p, args ...);
+}
+
+#define log_dump(...) do { \
+ log("DEBUG DUMP IN %s AT %s:%d:", __PRETTY_FUNCTION__, __FILE__, __LINE__); \
+ log_dump_args_worker(#__VA_ARGS__, __VA_ARGS__); \
+ log("\n"); \
+} while (0)
+
#endif
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index 9dfe196dc..1311f31cc 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -337,7 +337,7 @@ namespace {
expected_ports.insert(name);
}
- void check_expected()
+ void check_expected(bool check_matched_sign = true)
{
for (auto &para : cell->parameters)
if (expected_params.count(para.first) == 0)
@@ -345,6 +345,13 @@ namespace {
for (auto &conn : cell->connections)
if (expected_ports.count(conn.first) == 0)
error(__LINE__);
+
+ if (expected_params.count("\\A_SIGNED") != 0 && expected_params.count("\\B_SIGNED") && check_matched_sign) {
+ bool a_is_signed = param("\\A_SIGNED") != 0;
+ bool b_is_signed = param("\\B_SIGNED") != 0;
+ if (a_is_signed != b_is_signed)
+ error(__LINE__);
+ }
}
void check_gate(const char *ports)
@@ -370,7 +377,7 @@ namespace {
void check()
{
- if (cell->type == "$not" || cell->type == "$pos" || cell->type == "$neg") {
+ if (cell->type == "$not" || cell->type == "$pos" || cell->type == "$bu0" || cell->type == "$neg") {
param("\\A_SIGNED");
port("\\A", param("\\A_WIDTH"));
port("\\Y", param("\\Y_WIDTH"));
@@ -403,12 +410,12 @@ namespace {
port("\\A", param("\\A_WIDTH"));
port("\\B", param("\\B_WIDTH"));
port("\\Y", param("\\Y_WIDTH"));
- check_expected();
+ check_expected(false);
return;
}
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"));
@@ -425,7 +432,7 @@ namespace {
port("\\A", param("\\A_WIDTH"));
port("\\B", param("\\B_WIDTH"));
port("\\Y", param("\\Y_WIDTH"));
- check_expected();
+ check_expected(cell->type != "$pow");
return;
}
@@ -443,7 +450,7 @@ namespace {
port("\\A", param("\\A_WIDTH"));
port("\\B", param("\\B_WIDTH"));
port("\\Y", param("\\Y_WIDTH"));
- check_expected();
+ check_expected(false);
return;
}
@@ -560,6 +567,7 @@ namespace {
param("\\MEMID");
param("\\CLK_ENABLE");
param("\\CLK_POLARITY");
+ param("\\PRIORITY");
port("\\CLK", 1);
port("\\EN", 1);
port("\\ADDR", param("\\ABITS"));
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index fbdab53eb..8e3b78eef 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -174,6 +174,8 @@ namespace RTLIL
RTLIL::Const const_le (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
RTLIL::Const const_eq (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
RTLIL::Const const_ne (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
+ RTLIL::Const const_eqx (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
+ RTLIL::Const const_nex (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
RTLIL::Const const_ge (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
RTLIL::Const const_gt (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
@@ -185,6 +187,7 @@ namespace RTLIL
RTLIL::Const const_pow (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
RTLIL::Const const_pos (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
+ RTLIL::Const const_bu0 (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
RTLIL::Const const_neg (const RTLIL::Const &arg1, const RTLIL::Const &arg2, bool signed1, bool signed2, int result_len);
};
diff --git a/kernel/satgen.h b/kernel/satgen.h
index 35e15aa6c..208ae1658 100644
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -35,21 +35,19 @@ typedef ezSAT ezDefaultSAT;
struct SatGen
{
ezSAT *ez;
- RTLIL::Design *design;
SigMap *sigmap;
std::string prefix;
SigPool initial_state;
bool ignore_div_by_zero;
bool model_undef;
- SatGen(ezSAT *ez, RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string()) :
- ez(ez), design(design), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false)
+ SatGen(ezSAT *ez, SigMap *sigmap, std::string prefix = std::string()) :
+ ez(ez), sigmap(sigmap), prefix(prefix), ignore_div_by_zero(false), model_undef(false)
{
}
- void setContext(RTLIL::Design *design, SigMap *sigmap, std::string prefix = std::string())
+ void setContext(SigMap *sigmap, std::string prefix = std::string())
{
- this->design = design;
this->sigmap = sigmap;
this->prefix = prefix;
}
@@ -121,11 +119,10 @@ struct SatGen
return ez->expression(ezSAT::OpAnd, eq_bits);
}
- void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell, size_t y_width = 0, bool undef_mode = false)
+ void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, RTLIL::Cell *cell, size_t y_width = 0, bool forced_signed = false)
{
- log_assert(!undef_mode || model_undef);
- bool is_signed = undef_mode;
- if (!undef_mode && cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters.count("\\B_SIGNED") > 0)
+ bool is_signed = forced_signed;
+ if (!forced_signed && cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters.count("\\B_SIGNED") > 0)
is_signed = cell->parameters["\\A_SIGNED"].as_bool() && cell->parameters["\\B_SIGNED"].as_bool();
while (vec_a.size() < vec_b.size() || vec_a.size() < y_width)
vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
@@ -133,18 +130,16 @@ struct SatGen
vec_b.push_back(is_signed && vec_b.size() > 0 ? vec_b.back() : ez->FALSE);
}
- void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell, bool undef_mode = false)
+ void extendSignalWidth(std::vector<int> &vec_a, std::vector<int> &vec_b, std::vector<int> &vec_y, RTLIL::Cell *cell, bool forced_signed = false)
{
- log_assert(!undef_mode || model_undef);
- extendSignalWidth(vec_a, vec_b, cell, vec_y.size(), undef_mode);
+ extendSignalWidth(vec_a, vec_b, cell, vec_y.size(), forced_signed);
while (vec_y.size() < vec_a.size())
vec_y.push_back(ez->literal());
}
- void extendSignalWidthUnary(std::vector<int> &vec_a, std::vector<int> &vec_y, RTLIL::Cell *cell, bool undef_mode = false)
+ void extendSignalWidthUnary(std::vector<int> &vec_a, std::vector<int> &vec_y, RTLIL::Cell *cell, bool forced_signed = false)
{
- log_assert(!undef_mode || model_undef);
- bool is_signed = undef_mode || (cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters["\\A_SIGNED"].as_bool());
+ bool is_signed = forced_signed || (cell->parameters.count("\\A_SIGNED") > 0 && cell->parameters["\\A_SIGNED"].as_bool());
while (vec_a.size() < vec_y.size())
vec_a.push_back(is_signed && vec_a.size() > 0 ? vec_a.back() : ez->FALSE);
while (vec_y.size() < vec_a.size())
@@ -161,7 +156,6 @@ struct SatGen
{
bool arith_undef_handled = false;
bool is_arith_compare = cell->type == "$lt" || cell->type == "$le" || cell->type == "$ge" || cell->type == "$gt";
- int arith_undef_result = ez->FALSE;
if (model_undef && (cell->type == "$add" || cell->type == "$sub" || cell->type == "$mul" || cell->type == "$div" || cell->type == "$mod" || is_arith_compare))
{
@@ -191,7 +185,6 @@ struct SatGen
ez->assume(ez->vec_eq(undef_y_bits, undef_y));
}
- arith_undef_result = undef_y_bit;
arith_undef_handled = true;
}
@@ -224,7 +217,7 @@ struct SatGen
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);
- extendSignalWidth(undef_a, undef_b, undef_y, cell, true);
+ extendSignalWidth(undef_a, undef_b, undef_y, cell, false);
if (cell->type == "$and" || cell->type == "$_AND_") {
std::vector<int> a0 = ez->vec_and(ez->vec_not(a), ez->vec_not(undef_a));
@@ -306,6 +299,9 @@ struct SatGen
std::vector<int> b = importDefSigSpec(cell->connections.at("\\B"), timestep);
std::vector<int> s = importDefSigSpec(cell->connections.at("\\S"), timestep);
std::vector<int> y = importDefSigSpec(cell->connections.at("\\Y"), timestep);
+
+ std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+
std::vector<int> tmp = a;
for (size_t i = 0; i < s.size(); i++) {
std::vector<int> part_of_b(b.begin()+i*a.size(), b.begin()+(i+1)*a.size());
@@ -313,12 +309,24 @@ struct SatGen
}
if (cell->type == "$safe_pmux")
tmp = ez->vec_ite(ez->onehot(s, true), tmp, a);
- ez->assume(ez->vec_eq(tmp, y));
+ ez->assume(ez->vec_eq(tmp, yy));
- if (model_undef) {
- log("FIXME: No SAT undef model cell type %s!\n", RTLIL::id2cstr(cell->type));
+ if (model_undef)
+ {
+ 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_s = importUndefSigSpec(cell->connections.at("\\S"), timestep);
std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep);
- ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_y)));
+
+ tmp = a;
+ for (size_t i = 0; i < s.size(); i++) {
+ std::vector<int> part_of_undef_b(undef_b.begin()+i*a.size(), undef_b.begin()+(i+1)*a.size());
+ tmp = ez->vec_ite(s.at(i), part_of_undef_b, tmp);
+ }
+ tmp = ez->vec_ite(ez->onehot(s, true), tmp, cell->type == "$safe_pmux" ? a : std::vector<int>(tmp.size(), ez->TRUE));
+ tmp = ez->vec_ite(ez->expression(ezSAT::OpOr, undef_s), std::vector<int>(tmp.size(), ez->TRUE), tmp);
+ ez->assume(ez->vec_eq(tmp, undef_y));
+ undefGating(y, yy, undef_y);
}
return true;
}
@@ -451,7 +459,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);
@@ -461,13 +469,21 @@ struct SatGen
std::vector<int> yy = model_undef ? ez->vec_var(y.size()) : y;
+ 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);
+ extendSignalWidth(undef_a, undef_b, cell, true);
+ a = ez->vec_or(a, undef_a);
+ b = ez->vec_or(b, undef_b);
+ }
+
if (cell->type == "$lt")
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 +492,24 @@ 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);
+ extendSignalWidth(undef_a, undef_b, cell, true);
+
+ if (cell->type == "$eqx")
+ yy.at(0) = ez->AND(yy.at(0), ez->vec_eq(undef_a, undef_b));
+ else
+ yy.at(0) = ez->OR(yy.at(0), ez->vec_ne(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);
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-24 17:58:52 +0000