diff options
Diffstat (limited to 'passes/sat')
-rw-r--r-- | passes/sat/miter.cc | 38 |
1 files changed, 31 insertions, 7 deletions
diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc index 4854e19bf..341a6bac8 100644 --- a/passes/sat/miter.cc +++ b/passes/sat/miter.cc @@ -312,18 +312,42 @@ void create_miter_assert(struct Pass *that, std::vector<std::string> args, RTLIL log_pop(); } - SigSpec or_signals; + SigSpec assert_signals, assume_signals; vector<Cell*> cell_list = module->cells(); - for (auto cell : cell_list) { + for (auto cell : cell_list) + { + if (!cell->type.in("$assert", "$assume")) + continue; + + SigBit is_active = module->Nex(NEW_ID, cell->getPort("\\A"), State::S1); + SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort("\\EN"), State::S1); + if (cell->type == "$assert") { - SigBit is_active = module->Nex(NEW_ID, cell->getPort("\\A"), State::S1); - SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort("\\EN"), State::S1); - or_signals.append(module->And(NEW_ID, is_active, is_enabled)); - module->remove(cell); + assert_signals.append(module->And(NEW_ID, is_active, is_enabled)); + } else { + assume_signals.append(module->And(NEW_ID, is_active, is_enabled)); } + + module->remove(cell); } - module->addReduceOr(NEW_ID, or_signals, trigger); + if (assume_signals.empty()) + { + module->addReduceOr(NEW_ID, assert_signals, trigger); + } + else + { + Wire *assume_q = module->addWire(NEW_ID); + assume_q->attributes["\\init"] = State::S1; + assume_signals.append(assume_q); + + SigSpec assume_nok = module->ReduceOr(NEW_ID, assume_signals); + SigSpec assume_ok = module->Not(NEW_ID, assume_nok); + module->addFf(NEW_ID, assume_ok, assume_q); + + SigSpec assert_fail = module->ReduceOr(NEW_ID, assert_signals); + module->addAnd(NEW_ID, assert_fail, assume_ok, trigger); + } if (flag_flatten) { log_push(); |