summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorClifford Wolf <clifford@clifford.at>2014-02-04 12:46:16 +0100
committerClifford Wolf <clifford@clifford.at>2014-02-04 12:46:16 +0100
commitd267bcde4eeb9ba6d6adac5e2efcb523fcd9ea20 (patch)
tree3b1f65f0482a6efb22933953926d9ca3ffeeabf8
parentecdf1f5577dec6a02c944e68d1e923140e51f5bc (diff)
Fixed bug in sequential sat proofs and improved handling of asserts
-rw-r--r--frontends/ast/simplify.cc2
-rw-r--r--kernel/satgen.h23
-rw-r--r--passes/sat/sat.cc29
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();