diff options
author | Clifford Wolf <clifford@clifford.at> | 2013-12-07 17:28:51 +0100 |
---|---|---|
committer | Clifford Wolf <clifford@clifford.at> | 2013-12-07 17:28:51 +0100 |
commit | 8a815ac74169f62a90511b9b4bda99ceaf5ae774 (patch) | |
tree | 881465190aed3ad3ca834131e82a0fcfcc3d6b65 /kernel | |
parent | ccf083e5b0a41373dc433b7490d8bf9a1ff726d0 (diff) | |
download | yosys-8a815ac74169f62a90511b9b4bda99ceaf5ae774.tar.gz yosys-8a815ac74169f62a90511b9b4bda99ceaf5ae774.tar.bz2 yosys-8a815ac74169f62a90511b9b4bda99ceaf5ae774.zip |
Added "sat" undef support and "sat -set-init" options
Diffstat (limited to 'kernel')
-rw-r--r-- | kernel/satgen.h | 37 |
1 files changed, 24 insertions, 13 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h index c2aa4fc2b..35e15aa6c 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -98,18 +98,21 @@ struct SatGen return importSigSpecWorker(sig, pf, true, false); } - int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep = -1) + int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep_lhs = -1, int timestep_rhs = -1) { + if (timestep_rhs < 0) + timestep_rhs = timestep_lhs; + assert(lhs.width == rhs.width); - std::vector<int> vec_lhs = importSigSpec(lhs, timestep); - std::vector<int> vec_rhs = importSigSpec(rhs, timestep); + std::vector<int> vec_lhs = importSigSpec(lhs, timestep_lhs); + std::vector<int> vec_rhs = importSigSpec(rhs, timestep_rhs); if (!model_undef) return ez->vec_eq(vec_lhs, vec_rhs); - std::vector<int> undef_lhs = importUndefSigSpec(lhs, timestep); - std::vector<int> undef_rhs = importUndefSigSpec(rhs, timestep); + std::vector<int> undef_lhs = importUndefSigSpec(lhs, timestep_lhs); + std::vector<int> undef_rhs = importUndefSigSpec(rhs, timestep_rhs); std::vector<int> eq_bits; for (int i = 0; i < lhs.width; i++) @@ -674,18 +677,26 @@ struct SatGen if (timestep > 0 && (cell->type == "$dff" || cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_")) { - if (timestep == 1) { + if (timestep == 1) + { initial_state.add((*sigmap)(cell->connections.at("\\Q"))); - } else { + } + else + { std::vector<int> d = importDefSigSpec(cell->connections.at("\\D"), timestep-1); std::vector<int> q = importDefSigSpec(cell->connections.at("\\Q"), timestep); - ez->assume(ez->vec_eq(d, q)); - } - if (model_undef) { - log("FIXME: No SAT undef model cell type %s!\n", RTLIL::id2cstr(cell->type)); - std::vector<int> undef_y = importUndefSigSpec(cell->connections.at("\\Y"), timestep); - ez->assume(ez->NOT(ez->expression(ezSAT::OpOr, undef_y))); + 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->connections.at("\\D"), timestep-1); + std::vector<int> undef_q = importUndefSigSpec(cell->connections.at("\\Q"), timestep); + + ez->assume(ez->vec_eq(undef_d, undef_q)); + undefGating(q, qq, undef_q); + } } return true; } |