mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-06 17:44:09 +00:00
Code Activity

Merge pull request #2135 from boqwxp/qbfsat-timeinfo

Browse source 
log and qbfsat: Also include child process usage in `PerformanceTimer::query()` and report the time for each call to the QBF-SAT solver
This commit is contained in:
clairexen 2020-06-25 18:18:09 +02:00 committed by GitHub
parent fb6441731a 28c2dd470b
commit 21209d632e
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
2 changed files with 14 additions and 11 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
kernel/log.h
View file

@ -308,19 +308,17 @@ struct PerformanceTimer
static int64_t query() { static int64_t query() {
# ifdef _WIN32 # ifdef _WIN32
return 0; 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) # elif defined(RUSAGE_SELF)
struct rusage rusage; struct rusage rusage;
int64_t t; int64_t t = 0;
if (getrusage(RUSAGE_SELF, &rusage) == -1) { for (int who : {RUSAGE_SELF, RUSAGE_CHILDREN}) {
log_cmd_error("getrusage failed!\n"); if (getrusage(who, &rusage) == -1) {
log_abort(); 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; return t;
# else # else
# error "Don't know how to measure per-process CPU time. Need alternative method (times()/clocks()/gettimeofday()?)." # error "Don't know how to measure per-process CPU time. Need alternative method (times()/clocks()/gettimeofday()?)."

7
passes/sat/qbfsat.cc
View file

@ -39,10 +39,11 @@ static inline unsigned int difference(unsigned int a, unsigned int b) {
struct QbfSolutionType { struct QbfSolutionType {
std::vector<std::string> stdout_lines; std::vector<std::string> stdout_lines;
dict<pool<std::string>, std::string> hole_to_value; dict<pool<std::string>, std::string> hole_to_value;
double solver_time;
bool sat; bool sat;
bool unknown; //true if neither 'sat' nor 'unsat' bool unknown; //true if neither 'sat' nor 'unsat'
QbfSolutionType() : sat(false), unknown(true) {} QbfSolutionType() : solver_time(0.0), sat(false), unknown(true) {}
}; };
struct QbfSolveOptions { 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"); log_header(mod->design, "Solving QBF-SAT problem.\n");
if (!quiet) log("Launching \"%s\".\n", smtbmc_cmd.c_str()); if (!quiet) log("Launching \"%s\".\n", smtbmc_cmd.c_str());
int64_t begin = PerformanceTimer::query();
run_command(smtbmc_cmd, process_line); 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); recover_solution(ret);
return ret; return ret;