Added satgen initstate support

diff --git a/kernel/satgen.h b/kernel/satgen.h
index eb1c6fe36f4331b19386d2747beb03960942370f..31b7a3e5a726ba12a9d683a4a5249c8b0752776a 100644 (file)
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -71,6 +71,7 @@ struct SatGen
        std::map<std::string, RTLIL::SigSpec> assumes_a, assumes_en;
        std::map<std::string, RTLIL::SigSpec> predict_a, predict_en;
        std::map<std::string, std::map<RTLIL::SigBit, int>> imported_signals;
+       std::map<std::pair<std::string, int>, bool> initstates;
        bool ignore_div_by_zero;
        bool model_undef;
 
@@ -267,6 +268,13 @@ struct SatGen
                ez->assume(ez->OR(undef, ez->IFF(y, yy)));
        }
 
+       void setInitState(int timestep)
+       {
+               auto key = make_pair(prefix, timestep);
+               log_assert(initstates.count(key) == 0 || initstates.at(key) == true);
+               initstates[key] = true;
+       }
+
        bool importCell(RTLIL::Cell *cell, int timestep = -1)
        {
                bool arith_undef_handled = false;
@@ -1331,6 +1339,25 @@ struct SatGen
                        return true;
                }
 
+               if (cell->type == "$initstate")
+               {
+                       auto key = make_pair(prefix, timestep);
+                       if (initstates.count(key) == 0)
+                               initstates[key] = false;
+
+                       std::vector<int> y = importDefSigSpec(cell->getPort("\\Y"), timestep);
+                       log_assert(GetSize(y) == 1);
+                       ez->SET(y[0], initstates[key] ? ez->CONST_TRUE : ez->CONST_FALSE);
+
+                       if (model_undef) {
+                               std::vector<int> undef_y = importUndefSigSpec(cell->getPort("\\Y"), timestep);
+                               log_assert(GetSize(undef_y) == 1);
+                               ez->SET(undef_y[0], ez->CONST_FALSE);
+                       }
+
+                       return true;
+               }
+
                if (cell->type == "$assert")
                {
                        std::string pf = prefix + (timestep == -1 ? "" : stringf("@%d:", timestep));