diff options
Diffstat (limited to 'kernel/satgen.h')
| -rw-r--r-- | kernel/satgen.h | 131 |
1 files changed, 131 insertions, 0 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h index d44d61f1..0a65b490 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -70,6 +70,7 @@ struct SatGen std::map<std::string, RTLIL::SigSpec> asserts_a, asserts_en; std::map<std::string, RTLIL::SigSpec> assumes_a, assumes_en; std::map<std::string, std::map<RTLIL::SigBit, int>> imported_signals; + std::map<std::pair<std::string, int>, bool> initstates; bool ignore_div_by_zero; bool model_undef; @@ -266,6 +267,13 @@ struct SatGen ez->assume(ez->OR(undef, ez->IFF(y, yy))); } + void setInitState(int timestep) + { + auto key = make_pair(prefix, timestep); + log_assert(initstates.count(key) == 0 || initstates.at(key) == true); + initstates[key] = true; + } + bool importCell(RTLIL::Cell *cell, int timestep = -1) { bool arith_undef_handled = false; @@ -1048,6 +1056,88 @@ struct SatGen return true; } + if (cell->type == "$sop") + { + std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep); + int y = importDefSigSpec(cell->getPort("\\Y"), timestep).at(0); + + int width = cell->getParam("\\WIDTH").as_int(); + int depth = cell->getParam("\\DEPTH").as_int(); + + vector<State> table_raw = cell->getParam("\\TABLE").bits; + while (GetSize(table_raw) < 2*width*depth) + table_raw.push_back(State::S0); + + vector<vector<int>> table(depth); + + for (int i = 0; i < depth; i++) + for (int j = 0; j < width; j++) + { + bool pat0 = (table_raw[2*width*i + 2*j + 0] == State::S1); + bool pat1 = (table_raw[2*width*i + 2*j + 1] == State::S1); + + if (pat0 && !pat1) + table.at(i).push_back(0); + else if (!pat0 && pat1) + table.at(i).push_back(1); + else + table.at(i).push_back(-1); + } + + if (model_undef) + { + std::vector<int> products, undef_products; + std::vector<int> undef_a = importUndefSigSpec(cell->getPort("\\A"), timestep); + int undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep).at(0); + + for (int i = 0; i < depth; i++) + { + std::vector<int> cmp_a, cmp_ua, cmp_b; + + for (int j = 0; j < width; j++) + if (table.at(i).at(j) >= 0) { + cmp_a.push_back(a.at(j)); + cmp_ua.push_back(undef_a.at(j)); + cmp_b.push_back(table.at(i).at(j) ? ez->CONST_TRUE : ez->CONST_FALSE); + } + + std::vector<int> masked_a = ez->vec_or(cmp_a, cmp_ua); + std::vector<int> masked_b = ez->vec_or(cmp_b, cmp_ua); + + int masked_eq = ez->vec_eq(masked_a, masked_b); + int any_undef = ez->expression(ezSAT::OpOr, cmp_ua); + + undef_products.push_back(ez->AND(any_undef, masked_eq)); + products.push_back(ez->AND(ez->NOT(any_undef), masked_eq)); + } + + int yy = ez->expression(ezSAT::OpOr, products); + ez->SET(undef_y, ez->AND(ez->NOT(yy), ez->expression(ezSAT::OpOr, undef_products))); + undefGating(y, yy, undef_y); + } + else + { + std::vector<int> products; + + for (int i = 0; i < depth; i++) + { + std::vector<int> cmp_a, cmp_b; + + for (int j = 0; j < width; j++) + if (table.at(i).at(j) >= 0) { + cmp_a.push_back(a.at(j)); + cmp_b.push_back(table.at(i).at(j) ? ez->CONST_TRUE : ez->CONST_FALSE); + } + + products.push_back(ez->vec_eq(cmp_a, cmp_b)); + } + + ez->SET(y, ez->expression(ezSAT::OpOr, products)); + } + + return true; + } + if (cell->type == "$fa") { std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep); @@ -1229,6 +1319,28 @@ struct SatGen return true; } + if (cell->type == "$anyconst") + { + if (timestep < 2) + return true; + + std::vector<int> d = importDefSigSpec(cell->getPort("\\Y"), timestep-1); + std::vector<int> q = importDefSigSpec(cell->getPort("\\Y"), timestep); + + std::vector<int> qq = model_undef ? ez->vec_var(q.size()) : q; + ez->assume(ez->vec_eq(d, qq)); + + if (model_undef) + { + std::vector<int> undef_d = importUndefSigSpec(cell->getPort("\\D"), timestep-1); + std::vector<int> undef_q = importUndefSigSpec(cell->getPort("\\Q"), timestep); + + ez->assume(ez->vec_eq(undef_d, undef_q)); + undefGating(q, qq, undef_q); + } + return true; + } + if (cell->type == "$_BUF_" || cell->type == "$equiv") { std::vector<int> a = importDefSigSpec(cell->getPort("\\A"), timestep); @@ -1248,6 +1360,25 @@ struct SatGen return true; } + if (cell->type == "$initstate") + { + auto key = make_pair(prefix, timestep); + if (initstates.count(key) == 0) + initstates[key] = false; + + std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep); + log_assert(GetSize(y) == 1); + ez->SET(y[0], initstates[key] ? ez->CONST_TRUE : ez->CONST_FALSE); + + if (model_undef) { + std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep); + log_assert(GetSize(undef_y) == 1); + ez->SET(undef_y[0], ez->CONST_FALSE); + } + + return true; + } + if (cell->type == "$assert") { std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep)); |