diff options
| author | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-06-07 07:45:24 +0000 |
|---|---|---|
| committer | Alberto Gonzalez <boqwxp@airmail.cc> | 2020-06-21 02:16:52 +0000 |
| commit | a564cc806f2e710b9cbb8365fd63587351bf3040 (patch) | |
| tree | 8104a60e1882530305cec6f898f04af5a53ecc7a /passes/sat/qbfsat.cc | |
| parent | 62a9e62a1bc016122c2224bb157e86d8dbad5613 (diff) | |
| download | yosys-a564cc806f2e710b9cbb8365fd63587351bf3040.tar.gz yosys-a564cc806f2e710b9cbb8365fd63587351bf3040.tar.bz2 yosys-a564cc806f2e710b9cbb8365fd63587351bf3040.zip | |
log, qbfsat: Include child process time in `PerformanceTimer::query()` and report the time for each call to the QBF-SAT solver.
Diffstat (limited to 'passes/sat/qbfsat.cc')
| -rw-r--r-- | passes/sat/qbfsat.cc | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 35a0d0b1e..f4624ab3b 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -39,10 +39,11 @@ static inline unsigned int difference(unsigned int a, unsigned int b) { struct QbfSolutionType { std::vector<std::string> stdout_lines; dict<pool<std::string>, std::string> hole_to_value; + double solver_time; bool sat; bool unknown; //true if neither 'sat' nor 'unsat' - QbfSolutionType() : sat(false), unknown(true) {} + QbfSolutionType() : solver_time(0.0), sat(false), unknown(true) {} }; struct QbfSolveOptions { @@ -421,7 +422,11 @@ QbfSolutionType call_qbf_solver(RTLIL::Module *mod, const QbfSolveOptions &opt, }; log_header(mod->design, "Solving QBF-SAT problem.\n"); if (!quiet) log("Launching \"%s\".\n", smtbmc_cmd.c_str()); + int64_t begin = PerformanceTimer::query(); run_command(smtbmc_cmd, process_line); + int64_t end = PerformanceTimer::query(); + ret.solver_time = (end - begin) / 1e9f; + if (!quiet) log("Solver finished in %.3f seconds.\n", ret.solver_time); recover_solution(ret); return ret; |