diff options
| author | Clifford Wolf <clifford@clifford.at> | 2014-02-04 12:46:16 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2014-02-04 12:46:16 +0100 |
| commit | d267bcde4eeb9ba6d6adac5e2efcb523fcd9ea20 (patch) | |
| tree | 3b1f65f0482a6efb22933953926d9ca3ffeeabf8 /passes | |
| parent | ecdf1f5577dec6a02c944e68d1e923140e51f5bc (diff) | |
| download | yosys-d267bcde4eeb9ba6d6adac5e2efcb523fcd9ea20.tar.gz yosys-d267bcde4eeb9ba6d6adac5e2efcb523fcd9ea20.tar.bz2 yosys-d267bcde4eeb9ba6d6adac5e2efcb523fcd9ea20.zip | |
Fixed bug in sequential sat proofs and improved handling of asserts
Diffstat (limited to 'passes')
| -rw-r--r-- | passes/sat/sat.cc | 29 |
1 files changed, 27 insertions, 2 deletions
diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 389d01b97..e387d6575 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -90,6 +90,21 @@ struct SatHelper RTLIL::SigSpec big_lhs, big_rhs; + for (auto &it : module->wires) + { + if (it.second->attributes.count("\\init") == 0) + continue; + + RTLIL::SigSpec lhs = sigmap(it.second); + RTLIL::SigSpec rhs = it.second->attributes.at("\\init"); + log_assert(lhs.width == rhs.width); + + log("Import set-constraint from init attribute: %s = %s\n", log_signal(lhs), log_signal(rhs)); + big_lhs.remove2(lhs, &big_rhs); + big_lhs.append(lhs); + big_rhs.append(rhs); + } + for (auto &s : sets_init) { RTLIL::SigSpec lhs, rhs; @@ -356,8 +371,15 @@ struct SatHelper prove_bits.push_back(ez.OR(undef_lhs.at(i), ez.AND(ez.NOT(undef_rhs.at(i)), ez.NOT(ez.XOR(value_lhs.at(i), value_rhs.at(i)))))); } - if (prove_asserts) + if (prove_asserts) { + RTLIL::SigSpec asserts_a, asserts_en; + satgen.getAsserts(asserts_a, asserts_en, timestep); + asserts_a.expand(); + asserts_en.expand(); + for (size_t i = 0; i < asserts_a.chunks.size(); i++) + log("Import proof for assert: %s when %s.\n", log_signal(asserts_a.chunks[i]), log_signal(asserts_en.chunks[i])); prove_bits.push_back(satgen.importAsserts(timestep)); + } return ez.expression(ezSAT::OpAnd, prove_bits); } @@ -1105,11 +1127,14 @@ struct SatPass : public Pass { if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts) sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof())); } else { + std::vector<int> prove_bits; for (int timestep = 1; timestep <= seq_len; timestep++) { sathelper.setup(timestep); if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts) - sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof(timestep))); + prove_bits.push_back(sathelper.setup_proof(timestep)); } + if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts) + sathelper.ez.assume(sathelper.ez.NOT(sathelper.ez.expression(ezSAT::OpAnd, prove_bits))); sathelper.setup_init(); } sathelper.generate_model(); |