diff options
author | clairexen <claire@symbioticeda.com> | 2020-06-25 18:18:09 +0200 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-25 18:18:09 +0200 |
commit | 21209d632e62983d008e121c6ffcf2815d2ae4d8 (patch) | |
tree | edf8e293dd468d7625f4da2cf868e7385fd91879 | |
parent | fb6441731a03f8156821bdcfa6e08542951ac3f1 (diff) | |
parent | 28c2dd470b085f0be83ce1c55a687638bb31a75d (diff) | |
download | yosys-21209d632e62983d008e121c6ffcf2815d2ae4d8.tar.gz yosys-21209d632e62983d008e121c6ffcf2815d2ae4d8.tar.bz2 yosys-21209d632e62983d008e121c6ffcf2815d2ae4d8.zip |
Merge pull request #2135 from boqwxp/qbfsat-timeinfo
log and qbfsat: Also include child process usage in `PerformanceTimer::query()` and report the time for each call to the QBF-SAT solver
-rw-r--r-- | kernel/log.h | 18 | ||||
-rw-r--r-- | passes/sat/qbfsat.cc | 7 |
2 files changed, 14 insertions, 11 deletions
diff --git a/kernel/log.h b/kernel/log.h index 501d20c09..5986e0075 100644 --- a/kernel/log.h +++ b/kernel/log.h @@ -308,19 +308,17 @@ struct PerformanceTimer static int64_t query() { # ifdef _WIN32 return 0; -# elif defined(_POSIX_TIMERS) && (_POSIX_TIMERS > 0) - struct timespec ts; - clock_gettime(CLOCK_PROCESS_CPUTIME_ID, &ts); - return int64_t(ts.tv_sec)*1000000000 + ts.tv_nsec; # elif defined(RUSAGE_SELF) struct rusage rusage; - int64_t t; - if (getrusage(RUSAGE_SELF, &rusage) == -1) { - log_cmd_error("getrusage failed!\n"); - log_abort(); + int64_t t = 0; + for (int who : {RUSAGE_SELF, RUSAGE_CHILDREN}) { + if (getrusage(who, &rusage) == -1) { + log_cmd_error("getrusage failed!\n"); + log_abort(); + } + t += 1000000000ULL * (int64_t) rusage.ru_utime.tv_sec + (int64_t) rusage.ru_utime.tv_usec * 1000ULL; + t += 1000000000ULL * (int64_t) rusage.ru_stime.tv_sec + (int64_t) rusage.ru_stime.tv_usec * 1000ULL; } - t = 1000000000ULL * (int64_t) rusage.ru_utime.tv_sec + (int64_t) rusage.ru_utime.tv_usec * 1000ULL; - t += 1000000000ULL * (int64_t) rusage.ru_stime.tv_sec + (int64_t) rusage.ru_stime.tv_usec * 1000ULL; return t; # else # error "Don't know how to measure per-process CPU time. Need alternative method (times()/clocks()/gettimeofday()?)." 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; |