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 /kernel | |
| 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 'kernel')
| -rw-r--r-- | kernel/satgen.h | 23 |
1 files changed, 16 insertions, 7 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h index 0909e58ef..473aa6166 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -38,7 +38,7 @@ struct SatGen SigMap *sigmap; std::string prefix; SigPool initial_state; - RTLIL::SigSpec asserts_a, asserts_en; + std::map<std::string, RTLIL::SigSpec> asserts_a, asserts_en; bool ignore_div_by_zero; bool model_undef; @@ -97,15 +97,23 @@ struct SatGen return importSigSpecWorker(sig, pf, true, false); } + void getAsserts(RTLIL::SigSpec &sig_a, RTLIL::SigSpec &sig_en, int timestep = -1) + { + std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep)); + sig_a = asserts_a[pf]; + sig_en = asserts_en[pf]; + } + int importAsserts(int timestep = -1) { std::vector<int> check_bits, enable_bits; + std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep)); if (model_undef) { - check_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_a, timestep)), importDefSigSpec(asserts_a, timestep)); - enable_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_en, timestep)), importDefSigSpec(asserts_en, timestep)); + check_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_a[pf], timestep)), importDefSigSpec(asserts_a[pf], timestep)); + enable_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_en[pf], timestep)), importDefSigSpec(asserts_en[pf], timestep)); } else { - check_bits = importDefSigSpec(asserts_a, timestep); - enable_bits = importDefSigSpec(asserts_en, timestep); + check_bits = importDefSigSpec(asserts_a[pf], timestep); + enable_bits = importDefSigSpec(asserts_en[pf], timestep); } return ez->vec_reduce_and(ez->vec_or(check_bits, ez->vec_not(enable_bits))); } @@ -781,8 +789,9 @@ struct SatGen if (cell->type == "$assert") { - asserts_a.append((*sigmap)(cell->connections.at("\\A"))); - asserts_en.append((*sigmap)(cell->connections.at("\\EN"))); + std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep)); + asserts_a[pf].append((*sigmap)(cell->connections.at("\\A"))); + asserts_en[pf].append((*sigmap)(cell->connections.at("\\EN"))); return true; } |