Added $assert support to satgen

diff --git a/kernel/satgen.h b/kernel/satgen.h
index a668c73a405f9256737516ff9f5ec338766bb3c4..0909e58ef587c83a010c7e63339e9c93ee65b0f8 100644 (file)
--- a/kernel/satgen.h
+++ b/kernel/satgen.h
@@ -38,6 +38,7 @@ struct SatGen
        SigMap *sigmap;
        std::string prefix;
        SigPool initial_state;
+       RTLIL::SigSpec asserts_a, asserts_en;
        bool ignore_div_by_zero;
        bool model_undef;
 
@@ -96,6 +97,19 @@ struct SatGen
                return importSigSpecWorker(sig, pf, true, false);
        }
 
+       int importAsserts(int timestep = -1)
+       {
+               std::vector<int> check_bits, enable_bits;
+               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));
+               } else {
+                       check_bits = importDefSigSpec(asserts_a, timestep);
+                       enable_bits = importDefSigSpec(asserts_en, timestep);
+               }
+               return ez->vec_reduce_and(ez->vec_or(check_bits, ez->vec_not(enable_bits)));
+       }
+
        int signals_eq(RTLIL::SigSpec lhs, RTLIL::SigSpec rhs, int timestep_lhs = -1, int timestep_rhs = -1)
        {
                if (timestep_rhs < 0)
@@ -765,6 +779,13 @@ struct SatGen
                        return true;
                }
 
+               if (cell->type == "$assert")
+               {
+                       asserts_a.append((*sigmap)(cell->connections.at("\\A")));
+                       asserts_en.append((*sigmap)(cell->connections.at("\\EN")));
+                       return true;
+               }
+
                // Unsupported internal cell types: $pow $lut
                // .. and all sequential cells except $dff and $_DFF_[NP]_
                return false;