mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-10-31 03:32:29 +00:00
Code Activity

Fixed bug in sequential sat proofs and improved handling of asserts

Browse source
This commit is contained in:
Clifford Wolf 2014-02-04 12:46:16 +01:00
parent ecdf1f5577
commit d267bcde4e
3 changed files with 45 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

2
frontends/ast/simplify.cc
View file

@ -993,6 +993,8 @@ skip_dynamic_range_lvalue_expansion:;
AstNode *wire_en = new AstNode(AST_WIRE); AstNode *wire_en = new AstNode(AST_WIRE);
wire_en->str = id_en; wire_en->str = id_en;
current_ast_mod->children.push_back(wire_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; current_scope[wire_en->str] = wire_en;
while (wire_en->simplify(true, false, false, 1, -1, false)) { } while (wire_en->simplify(true, false, false, 1, -1, false)) { }

23
kernel/satgen.h
View file

@ -38,7 +38,7 @@ struct SatGen
SigMap *sigmap; SigMap *sigmap;
std::string prefix; std::string prefix;
SigPool initial_state; 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 ignore_div_by_zero;
bool model_undef; bool model_undef;
@ -97,15 +97,23 @@ struct SatGen
return importSigSpecWorker(sig, pf, true, false); 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) int importAsserts(int timestep = -1)
{ {
std::vector<int> check_bits, enable_bits; std::vector<int> check_bits, enable_bits;
std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
if (model_undef) { if (model_undef) {
check_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_a, timestep)), importDefSigSpec(asserts_a, 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, timestep)), importDefSigSpec(asserts_en, timestep)); enable_bits = ez->vec_and(ez->vec_not(importUndefSigSpec(asserts_en[pf], timestep)), importDefSigSpec(asserts_en[pf], timestep));
} else { } else {
check_bits = importDefSigSpec(asserts_a, timestep); check_bits = importDefSigSpec(asserts_a[pf], timestep);
enable_bits = importDefSigSpec(asserts_en, timestep); enable_bits = importDefSigSpec(asserts_en[pf], timestep);
} }
return ez->vec_reduce_and(ez->vec_or(check_bits, ez->vec_not(enable_bits))); 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") if (cell->type == "$assert")
{ {
asserts_a.append((*sigmap)(cell->connections.at("\\A"))); std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));
asserts_en.append((*sigmap)(cell->connections.at("\\EN"))); asserts_a[pf].append((*sigmap)(cell->connections.at("\\A")));
asserts_en[pf].append((*sigmap)(cell->connections.at("\\EN")));
return true; return true;
} }

29
passes/sat/sat.cc
View file

@ -90,6 +90,21 @@ struct SatHelper
RTLIL::SigSpec big_lhs, big_rhs; 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) for (auto &s : sets_init)
{ {
RTLIL::SigSpec lhs, rhs; 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)))))); 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)); prove_bits.push_back(satgen.importAsserts(timestep));
}
return ez.expression(ezSAT::OpAnd, prove_bits); 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) if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts)
sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof())); sathelper.ez.assume(sathelper.ez.NOT(sathelper.setup_proof()));
} else { } else {
std::vector<int> prove_bits;
for (int timestep = 1; timestep <= seq_len; timestep++) { for (int timestep = 1; timestep <= seq_len; timestep++) {
sathelper.setup(timestep); sathelper.setup(timestep);
if (sathelper.prove.size() || sathelper.prove_x.size() || sathelper.prove_asserts) 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.setup_init();
} }
sathelper.generate_model(); sathelper.generate_model();