diff options
Diffstat (limited to 'passes')
| -rw-r--r-- | passes/cmds/select.cc | 2 | ||||
| -rw-r--r-- | passes/fsm/fsm.cc | 9 | ||||
| -rw-r--r-- | passes/fsm/fsm_detect.cc | 9 | ||||
| -rw-r--r-- | passes/sat/sat.cc | 1 | ||||
| -rw-r--r-- | passes/sat/sim.cc | 25 |
5 files changed, 33 insertions, 13 deletions
diff --git a/passes/cmds/select.cc b/passes/cmds/select.cc index fdf56641c..03d00816e 100644 --- a/passes/cmds/select.cc +++ b/passes/cmds/select.cc @@ -1607,12 +1607,14 @@ struct CdPass : public Pass { log("with the specified name in the current module, then this is equivalent\n"); log("to 'cd <celltype>'.\n"); log("\n"); + log("\n"); log(" cd ..\n"); log("\n"); log("Remove trailing substrings that start with '.' in current module name until\n"); log("the name of a module in the current design is generated, then switch to that\n"); log("module. Otherwise clear the current selection.\n"); log("\n"); + log("\n"); log(" cd\n"); log("\n"); log("This is just a shortcut for 'select -clear'.\n"); diff --git a/passes/fsm/fsm.cc b/passes/fsm/fsm.cc index 0c5e624dc..8e7e09d4c 100644 --- a/passes/fsm/fsm.cc +++ b/passes/fsm/fsm.cc @@ -67,6 +67,15 @@ struct FsmPass : public Pass { log(" -encfile file\n"); log(" passed through to fsm_recode pass\n"); log("\n"); + log("This pass uses a subset of FF types to detect FSMs. Run 'opt -nosdff -nodffe'\n"); + log("before this pass to prepare the design.\n"); + log("\n"); +#ifdef YOSYS_ENABLE_VERIFIC + log("The Verific frontend may merge multiplexers in a way that interferes with FSM\n"); + log("detection. Run 'verific -cfg db_infer_wide_muxes_post_elaboration 0' before\n"); + log("reading the source, and 'bmuxmap' after 'proc' for best results.\n"); + log("\n"); +#endif } void execute(std::vector<std::string> args, RTLIL::Design *design) override { diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc index f829714c4..5378ec89e 100644 --- a/passes/fsm/fsm_detect.cc +++ b/passes/fsm/fsm_detect.cc @@ -272,6 +272,15 @@ struct FsmDetectPass : public Pass { log("Signals can be protected from being detected by this pass by setting the\n"); log("'fsm_encoding' attribute to \"none\".\n"); log("\n"); + log("This pass uses a subset of FF types to detect FSMs. Run 'opt -nosdff -nodffe'\n"); + log("before this pass to prepare the design for fsm_detect.\n"); + log("\n"); +#ifdef YOSYS_ENABLE_VERIFIC + log("The Verific frontend may merge multiplexers in a way that interferes with FSM\n"); + log("detection. Run 'verific -cfg db_infer_wide_muxes_post_elaboration 0' before\n"); + log("reading the source, and 'bmuxmap' after 'proc' for best results.\n"); + log("\n"); +#endif } void execute(std::vector<std::string> args, RTLIL::Design *design) override { diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index df2725b3c..e10517d72 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -758,6 +758,7 @@ struct SatHelper if (last_timestep == -2) log(" no model variables selected for display.\n"); + fprintf(f, "#%d\n", last_timestep+1); fclose(f); } diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index b68783f20..1cd1ebc71 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -813,18 +813,6 @@ struct SimInstance std::string v = shared->fst->valueOf(item.second); did_something |= set_state(item.first, Const::from_string(v)); } - for (auto &it : ff_database) - { - ff_state_t &ff = it.second; - SigSpec dsig = it.second.data.sig_d; - Const value = get_state(dsig); - if (dsig.is_wire()) { - ff.past_d = value; - if (ff.data.has_aload) - ff.past_ad = value; - did_something |= true; - } - } for (auto cell : module->cells()) { if (cell->is_mem_cell()) { @@ -1019,6 +1007,16 @@ struct SimWorker : SimShared top->update_ph3(); } + void initialize_stable_past() + { + if (debug) + log("\n-- ph1 (initialize) --\n"); + top->update_ph1(); + if (debug) + log("\n-- ph3 (initialize) --\n"); + top->update_ph3(); + } + void set_inports(pool<IdString> ports, State value) { for (auto portname : ports) @@ -1191,6 +1189,7 @@ struct SimWorker : SimShared if (initial) { did_something |= top->setInitState(); + initialize_stable_past(); initial = false; } if (did_something) @@ -2015,7 +2014,7 @@ struct SimPass : public Pass { log(" -r\n"); log(" read simulation results file\n"); log(" File formats supported: FST, VCD, AIW and WIT\n"); - log(" VCD support requires vcd2fst external tool to be present\n"); + log(" VCD support requires vcd2fst external tool to be present\n"); log("\n"); log(" -map <filename>\n"); log(" read file with port and latch symbols, needed for AIGER witness input\n"); |