diff options
| -rw-r--r-- | frontends/ast/simplify.cc | 2 | ||||
| -rw-r--r-- | kernel/satgen.h | 23 | ||||
| -rw-r--r-- | passes/sat/sat.cc | 29 |
3 files changed, 45 insertions, 9 deletions
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index f19befe2..3d995119 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -993,6 +993,8 @@ skip_dynamic_range_lvalue_expansion:; AstNode *wire_en = new AstNode(AST_WIRE); wire_en->str = id_en; current_ast_mod->children.push_back(wire_en); + current_ast_mod->children.push_back(new AstNode(AST_INITIAL, new AstNode(AST_BLOCK, new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), AstNode::mkconst_int(0, false, 1))))); + current_ast_mod->children.back()->children[0]->children[0]->children[0]->str = id_en; current_scope[wire_en->str] = wire_en; while (wire_en->simplify(true, false, false, 1, -1, false)) { } diff --git a/kernel/satgen.h b/kernel/satgen.h index 0909e58e..473aa616 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; } diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 389d01b9..e387d657 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(); |