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 /passes | |
| 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
Diffstat (limited to 'passes')
| -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; |