From: Alberto Gonzalez <boqwxp@airmail.cc>
Date: Sun, 7 Jun 2020 07:45:24 +0000 (+0000)
Subject: log, qbfsat: Include child process time in `PerformanceTimer::query()` and report... 
X-Git-Tag: working-ls180~448^2~1
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=a564cc806f2e710b9cbb8365fd63587351bf3040;p=yosys.git

log, qbfsat: Include child process time in `PerformanceTimer::query()` and report the time for each call to the QBF-SAT solver.
---

diff --git a/kernel/log.h b/kernel/log.h
index 501d20c09..d8e748ff8 100644
--- a/kernel/log.h
+++ b/kernel/log.h
@@ -314,13 +314,15 @@ struct PerformanceTimer
 		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;