diff options
Diffstat (limited to 'kernel/satgen.h')
-rw-r--r-- | kernel/satgen.h | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/kernel/satgen.h b/kernel/satgen.h index a668c73a4..0909e58ef 100644 --- 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; |