Fixed bug in sequential sat proofs and improved handling of asserts

diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index f19befe2ab22d8c12ff6d000ca041f01b389fe1f..3d99511946b795dd429b22d27c34a4366f1a7253 100644 (file)
--- 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 0909e58ef587c83a010c7e63339e9c93ee65b0f8..473aa6166dc6ba38ab5b33bbbe5a8f8819a06564 100644 (file)
--- 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 389d01b974f65998ba6f3cae5d3d36f6bae51f55..e387d657537f8f0e7b74b5c0981f92f402036d3f 100644 (file)
--- 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();