diff options
| author | Jannis Harder <me@jix.one> | 2022-12-21 14:40:58 +0100 |
|---|---|---|
| committer | Jannis Harder <me@jix.one> | 2023-01-11 18:07:16 +0100 |
| commit | f6458bab702e08ade0c15d7f7d8580cb5463d685 (patch) | |
| tree | 0cffa70adc2e04abae448b46436dea5ca982e464 | |
| parent | 9c6198a8272de1558d9f613d52a23c043e1c928a (diff) | |
| download | yosys-f6458bab702e08ade0c15d7f7d8580cb5463d685.tar.gz yosys-f6458bab702e08ade0c15d7f7d8580cb5463d685.tar.bz2 yosys-f6458bab702e08ade0c15d7f7d8580cb5463d685.zip | |
sim: Only check formal cells during gclk simulation updates
This is required for compatibility with non-multiclock formal semantics.
| -rw-r--r-- | passes/sat/sim.cc | 35 |
1 files changed, 19 insertions, 16 deletions
diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 86736eeb4..344ebb681 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -653,7 +653,7 @@ struct SimInstance return did_something; } - void update_ph3() + void update_ph3(bool check_assertions) { for (auto &it : ff_database) { @@ -688,27 +688,30 @@ struct SimInstance } } - for (auto cell : formal_database) + if (check_assertions) { - string label = log_id(cell); - if (cell->attributes.count(ID::src)) - label = cell->attributes.at(ID::src).decode_string(); + for (auto cell : formal_database) + { + string label = log_id(cell); + if (cell->attributes.count(ID::src)) + label = cell->attributes.at(ID::src).decode_string(); - State a = get_state(cell->getPort(ID::A))[0]; - State en = get_state(cell->getPort(ID::EN))[0]; + State a = get_state(cell->getPort(ID::A))[0]; + State en = get_state(cell->getPort(ID::EN))[0]; - if (cell->type == ID($cover) && en == State::S1 && a != State::S1) - log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str()); + if (cell->type == ID($cover) && en == State::S1 && a != State::S1) + log("Cover %s.%s (%s) reached.\n", hiername().c_str(), log_id(cell), label.c_str()); - if (cell->type == ID($assume) && en == State::S1 && a != State::S1) - log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); + if (cell->type == ID($assume) && en == State::S1 && a != State::S1) + log("Assumption %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); - if (cell->type == ID($assert) && en == State::S1 && a != State::S1) - log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); + if (cell->type == ID($assert) && en == State::S1 && a != State::S1) + log_warning("Assert %s.%s (%s) failed.\n", hiername().c_str(), log_id(cell), label.c_str()); + } } for (auto it : children) - it.second->update_ph3(); + it.second->update_ph3(check_assertions); } void set_initstate_outputs(State state) @@ -1116,7 +1119,7 @@ struct SimWorker : SimShared if (debug) log("\n-- ph3 --\n"); - top->update_ph3(); + top->update_ph3(gclk); } void initialize_stable_past() @@ -1126,7 +1129,7 @@ struct SimWorker : SimShared top->update_ph1(); if (debug) log("\n-- ph3 (initialize) --\n"); - top->update_ph3(); + top->update_ph3(false); } void set_inports(pool<IdString> ports, State value) |