sbysrc/sby_core.py

   1 #
   2 # SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
   3 #
   4 # Copyright (C) 2016  Clifford Wolf <clifford@clifford.at>
   5 #
   6 # Permission to use, copy, modify, and/or distribute this software for any
   7 # purpose with or without fee is hereby granted, provided that the above
   8 # copyright notice and this permission notice appear in all copies.
   9 #
  10 # THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11 # WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12 # MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13 # ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14 # WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15 # ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17 #
  18
  19 import os, re, sys, signal
  20 if os.name == "posix":
  21     import resource, fcntl
  22 import subprocess
  23 from shutil import copyfile, rmtree
  24 from select import select
  25 from time import time, localtime, sleep
  26
  27 all_tasks_running = []
  28
  29 def force_shutdown(signum, frame):
  30     print("SBY ---- Keyboard interrupt or external termination signal ----", flush=True)
  31     for task in list(all_tasks_running):
  32         task.terminate()
  33     sys.exit(1)
  34
  35 if os.name == "posix":
  36     signal.signal(signal.SIGHUP, force_shutdown)
  37 signal.signal(signal.SIGINT, force_shutdown)
  38 signal.signal(signal.SIGTERM, force_shutdown)
  39
  40 def process_filename(filename):
  41     if filename.startswith("~/"):
  42         filename = os.environ['HOME'] + filename[1:]
  43
  44     filename = os.path.expandvars(filename)
  45
  46     return filename
  47
  48 class SbyTask:
  49     def __init__(self, job, info, deps, cmdline, logfile=None, logstderr=True, silent=False):
  50         self.running = False
  51         self.finished = False
  52         self.terminated = False
  53         self.checkretcode = False
  54         self.job = job
  55         self.info = info
  56         self.deps = deps
  57         if os.name == "posix":
  58             self.cmdline = cmdline
  59         else:
  60             # Windows command interpreter equivalents for sequential
  61             # commands (; => &) command grouping ({} => ()).
  62             replacements = {
  63                 ";" : "&",
  64                 "{" : "(",
  65                 "}" : ")",
  66             }
  67             parts = cmdline.split("'")
  68             for i in range(len(parts)):
  69                 if i % 2 == 0:
  70                     cmdline_copy = parts[i]
  71                     for u, w in replacements.items():
  72                         cmdline_copy = cmdline_copy.replace(u, w)
  73                     parts[i] = cmdline_copy
  74             self.cmdline = '"'.join(parts)
  75         self.logfile = logfile
  76         self.noprintregex = None
  77         self.notify = []
  78         self.linebuffer = ""
  79         self.logstderr = logstderr
  80         self.silent = silent
  81
  82         self.job.tasks_pending.append(self)
  83
  84         for dep in self.deps:
  85             dep.register_dep(self)
  86
  87         self.output_callback = None
  88         self.exit_callback = None
  89
  90     def register_dep(self, next_task):
  91         if self.finished:
  92             next_task.poll()
  93         else:
  94             self.notify.append(next_task)
  95
  96     def log(self, line):
  97         if line is not None and (self.noprintregex is None or not self.noprintregex.match(line)):
  98             if self.logfile is not None:
  99                 print(line, file=self.logfile)
 100             self.job.log(f"{self.info}: {line}")
 101
 102     def handle_output(self, line):
 103         if self.terminated or len(line) == 0:
 104             return
 105         if self.output_callback is not None:
 106             line = self.output_callback(line)
 107         self.log(line)
 108
 109     def handle_exit(self, retcode):
 110         if self.terminated:
 111             return
 112         if self.logfile is not None:
 113             self.logfile.close()
 114         if self.exit_callback is not None:
 115             self.exit_callback(retcode)
 116
 117     def terminate(self, timeout=False):
 118         if self.job.opt_wait and not timeout:
 119             return
 120         if self.running:
 121             if not self.silent:
 122                 self.job.log(f"{self.info}: terminating process")
 123             if os.name == "posix":
 124                 try:
 125                     os.killpg(self.p.pid, signal.SIGTERM)
 126                 except PermissionError:
 127                     pass
 128             self.p.terminate()
 129             self.job.tasks_running.remove(self)
 130             all_tasks_running.remove(self)
 131         self.terminated = True
 132
 133     def poll(self):
 134         if self.finished or self.terminated:
 135             return
 136
 137         if not self.running:
 138             for dep in self.deps:
 139                 if not dep.finished:
 140                     return
 141
 142             if not self.silent:
 143                 self.job.log(f"{self.info}: starting process \"{self.cmdline}\"")
 144
 145             if os.name == "posix":
 146                 def preexec_fn():
 147                     signal.signal(signal.SIGINT, signal.SIG_IGN)
 148                     os.setpgrp()
 149
 150                 self.p = subprocess.Popen(["/usr/bin/env", "bash", "-c", self.cmdline], stdin=subprocess.DEVNULL, stdout=subprocess.PIPE,
 151                         stderr=(subprocess.STDOUT if self.logstderr else None), preexec_fn=preexec_fn)
 152
 153                 fl = fcntl.fcntl(self.p.stdout, fcntl.F_GETFL)
 154                 fcntl.fcntl(self.p.stdout, fcntl.F_SETFL, fl | os.O_NONBLOCK)
 155
 156             else:
 157                 self.p = subprocess.Popen(self.cmdline, shell=True, stdin=subprocess.DEVNULL, stdout=subprocess.PIPE,
 158                         stderr=(subprocess.STDOUT if self.logstderr else None))
 159
 160             self.job.tasks_pending.remove(self)
 161             self.job.tasks_running.append(self)
 162             all_tasks_running.append(self)
 163             self.running = True
 164             return
 165
 166         while True:
 167             outs = self.p.stdout.readline().decode("utf-8")
 168             if len(outs) == 0: break
 169             if outs[-1] != '\n':
 170                 self.linebuffer += outs
 171                 break
 172             outs = (self.linebuffer + outs).strip()
 173             self.linebuffer = ""
 174             self.handle_output(outs)
 175
 176         if self.p.poll() is not None:
 177             if not self.silent:
 178                 self.job.log(f"{self.info}: finished (returncode={self.p.returncode})")
 179             self.job.tasks_running.remove(self)
 180             all_tasks_running.remove(self)
 181             self.running = False
 182
 183             if self.p.returncode == 127:
 184                 self.job.status = "ERROR"
 185                 if not self.silent:
 186                     self.job.log(f"{self.info}: COMMAND NOT FOUND. ERROR.")
 187                 self.terminated = True
 188                 self.job.terminate()
 189                 return
 190
 191             self.handle_exit(self.p.returncode)
 192
 193             if self.checkretcode and self.p.returncode != 0:
 194                 self.job.status = "ERROR"
 195                 if not self.silent:
 196                     self.job.log(f"{self.info}: job failed. ERROR.")
 197                 self.terminated = True
 198                 self.job.terminate()
 199                 return
 200
 201             self.finished = True
 202             for next_task in self.notify:
 203                 next_task.poll()
 204             return
 205
 206
 207 class SbyAbort(BaseException):
 208     pass
 209
 210
 211 class SbyJob:
 212     def __init__(self, sbyconfig, workdir, early_logs, reusedir):
 213         self.options = dict()
 214         self.used_options = set()
 215         self.engines = list()
 216         self.script = list()
 217         self.files = dict()
 218         self.verbatim_files = dict()
 219         self.models = dict()
 220         self.workdir = workdir
 221         self.reusedir = reusedir
 222         self.status = "UNKNOWN"
 223         self.total_time = 0
 224         self.expect = []
 225
 226         yosys_program_prefix = "" ##yosys-program-prefix##
 227         self.exe_paths = {
 228             "yosys": os.getenv("YOSYS", yosys_program_prefix + "yosys"),
 229             "abc": os.getenv("ABC", yosys_program_prefix + "yosys-abc"),
 230             "smtbmc": os.getenv("SMTBMC", yosys_program_prefix + "yosys-smtbmc"),
 231             "suprove": os.getenv("SUPROVE", "suprove"),
 232             "aigbmc": os.getenv("AIGBMC", "aigbmc"),
 233             "avy": os.getenv("AVY", "avy"),
 234             "btormc": os.getenv("BTORMC", "btormc"),
 235             "pono": os.getenv("PONO", "pono"),
 236         }
 237
 238         self.tasks_running = []
 239         self.tasks_pending = []
 240
 241         self.start_clock_time = time()
 242
 243         if os.name == "posix":
 244             ru = resource.getrusage(resource.RUSAGE_CHILDREN)
 245             self.start_process_time = ru.ru_utime + ru.ru_stime
 246
 247         self.summary = list()
 248
 249         self.logfile = open(f"{workdir}/logfile.txt", "a")
 250
 251         for line in early_logs:
 252             print(line, file=self.logfile, flush=True)
 253
 254         if not reusedir:
 255             with open(f"{workdir}/config.sby", "w") as f:
 256                 for line in sbyconfig:
 257                     print(line, file=f)
 258
 259     def taskloop(self):
 260         for task in self.tasks_pending:
 261             task.poll()
 262
 263         while len(self.tasks_running):
 264             fds = []
 265             for task in self.tasks_running:
 266                 if task.running:
 267                     fds.append(task.p.stdout)
 268
 269             if os.name == "posix":
 270                 try:
 271                     select(fds, [], [], 1.0) == ([], [], [])
 272                 except InterruptedError:
 273                     pass
 274             else:
 275                 sleep(0.1)
 276
 277             for task in self.tasks_running:
 278                 task.poll()
 279
 280             for task in self.tasks_pending:
 281                 task.poll()
 282
 283             if self.opt_timeout is not None:
 284                 total_clock_time = int(time() - self.start_clock_time)
 285                 if total_clock_time > self.opt_timeout:
 286                     self.log(f"Reached TIMEOUT ({self.opt_timeout} seconds). Terminating all tasks.")
 287                     self.status = "TIMEOUT"
 288                     self.terminate(timeout=True)
 289
 290     def log(self, logmessage):
 291         tm = localtime()
 292         print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True)
 293         print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True)
 294
 295     def error(self, logmessage):
 296         tm = localtime()
 297         print("SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True)
 298         print("SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True)
 299         self.status = "ERROR"
 300         if "ERROR" not in self.expect:
 301             self.retcode = 16
 302         self.terminate()
 303         with open(f"{self.workdir}/{self.status}", "w") as f:
 304             print(f"ERROR: {logmessage}", file=f)
 305         raise SbyAbort(logmessage)
 306
 307     def makedirs(self, path):
 308         if self.reusedir and os.path.isdir(path):
 309             rmtree(path, ignore_errors=True)
 310         os.makedirs(path)
 311
 312     def copy_src(self):
 313         os.makedirs(self.workdir + "/src")
 314
 315         for dstfile, lines in self.verbatim_files.items():
 316             dstfile = self.workdir + "/src/" + dstfile
 317             self.log(f"Writing '{dstfile}'.")
 318
 319             with open(dstfile, "w") as f:
 320                 for line in lines:
 321                     f.write(line)
 322
 323         for dstfile, srcfile in self.files.items():
 324             if dstfile.startswith("/") or dstfile.startswith("../") or ("/../" in dstfile):
 325                 self.error(f"destination filename must be a relative path without /../: {dstfile}")
 326             dstfile = self.workdir + "/src/" + dstfile
 327
 328             srcfile = process_filename(srcfile)
 329
 330             basedir = os.path.dirname(dstfile)
 331             if basedir != "" and not os.path.exists(basedir):
 332                 os.makedirs(basedir)
 333
 334             self.log(f"Copy '{os.path.abspath(srcfile)}' to '{os.path.abspath(dstfile)}'.")
 335             copyfile(srcfile, dstfile)
 336
 337     def handle_str_option(self, option_name, default_value):
 338         if option_name in self.options:
 339             self.__dict__["opt_" + option_name] = self.options[option_name]
 340             self.used_options.add(option_name)
 341         else:
 342             self.__dict__["opt_" + option_name] = default_value
 343
 344     def handle_int_option(self, option_name, default_value):
 345         if option_name in self.options:
 346             self.__dict__["opt_" + option_name] = int(self.options[option_name])
 347             self.used_options.add(option_name)
 348         else:
 349             self.__dict__["opt_" + option_name] = default_value
 350
 351     def handle_bool_option(self, option_name, default_value):
 352         if option_name in self.options:
 353             if self.options[option_name] not in ["on", "off"]:
 354                 self.error(f"Invalid value '{self.options[option_name]}' for boolean option {option_name}.")
 355             self.__dict__["opt_" + option_name] = self.options[option_name] == "on"
 356             self.used_options.add(option_name)
 357         else:
 358             self.__dict__["opt_" + option_name] = default_value
 359
 360     def make_model(self, model_name):
 361         if not os.path.isdir(f"{self.workdir}/model"):
 362             os.makedirs(f"{self.workdir}/model")
 363
 364         if model_name in ["base", "nomem"]:
 365             with open(f"""{self.workdir}/model/design{"" if model_name == "base" else "_nomem"}.ys""", "w") as f:
 366                 print(f"# running in {self.workdir}/src/", file=f)
 367                 for cmd in self.script:
 368                     print(cmd, file=f)
 369                 if model_name == "base":
 370                     print("memory_nordff", file=f)
 371                 else:
 372                     print("memory_map", file=f)
 373                 if self.opt_multiclock:
 374                     print("clk2fflogic", file=f)
 375                 else:
 376                     print("async2sync", file=f)
 377                     print("chformal -assume -early", file=f)
 378                 if self.opt_mode in ["bmc", "prove"]:
 379                     print("chformal -live -fair -cover -remove", file=f)
 380                 if self.opt_mode == "cover":
 381                     print("chformal -live -fair -remove", file=f)
 382                 if self.opt_mode == "live":
 383                     print("chformal -assert2assume", file=f)
 384                     print("chformal -cover -remove", file=f)
 385                 print("opt_clean", file=f)
 386                 print("setundef -anyseq", file=f)
 387                 print("opt -keepdc -fast", file=f)
 388                 print("check", file=f)
 389                 print("hierarchy -simcheck", file=f)
 390                 print(f"""write_ilang ../model/design{"" if model_name == "base" else "_nomem"}.il""", file=f)
 391
 392             task = SbyTask(
 393                 self,
 394                 model_name,
 395                 [],
 396                 "cd {}/src; {} -ql ../model/design{s}.log ../model/design{s}.ys".format(self.workdir, self.exe_paths["yosys"],
 397                     s="" if model_name == "base" else "_nomem")
 398             )
 399             task.checkretcode = True
 400
 401             return [task]
 402
 403         if re.match(r"^smt2(_syn)?(_nomem)?(_stbv|_stdt)?$", model_name):
 404             with open(f"{self.workdir}/model/design_{model_name}.ys", "w") as f:
 405                 print(f"# running in {self.workdir}/model/", file=f)
 406                 print(f"""read_ilang design{"_nomem" if "_nomem" in model_name else ""}.il""", file=f)
 407                 if "_syn" in model_name:
 408                     print("techmap", file=f)
 409                     print("opt -fast", file=f)
 410                     print("abc", file=f)
 411                     print("opt_clean", file=f)
 412                 print("dffunmap", file=f)
 413                 print("stat", file=f)
 414                 if "_stbv" in model_name:
 415                     print(f"write_smt2 -stbv -wires design_{model_name}.smt2", file=f)
 416                 elif "_stdt" in model_name:
 417                     print(f"write_smt2 -stdt -wires design_{model_name}.smt2", file=f)
 418                 else:
 419                     print(f"write_smt2 -wires design_{model_name}.smt2", file=f)
 420
 421             task = SbyTask(
 422                 self,
 423                 model_name,
 424                 self.model("nomem" if "_nomem" in model_name else "base"),
 425                 "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name)
 426             )
 427             task.checkretcode = True
 428
 429             return [task]
 430
 431         if re.match(r"^btor(_syn)?(_nomem)?$", model_name):
 432             with open(f"{self.workdir}/model/design_{model_name}.ys", "w") as f:
 433                 print(f"# running in {self.workdir}/model/", file=f)
 434                 print(f"""read_ilang design{"_nomem" if "_nomem" in model_name else ""}.il""", file=f)
 435                 print("flatten", file=f)
 436                 print("setundef -undriven -anyseq", file=f)
 437                 if "_syn" in model_name:
 438                     print("opt -full", file=f)
 439                     print("techmap", file=f)
 440                     print("opt -fast", file=f)
 441                     print("abc", file=f)
 442                     print("opt_clean", file=f)
 443                 else:
 444                     print("opt -fast", file=f)
 445                 print("delete -output", file=f)
 446                 print("dffunmap", file=f)
 447                 print("stat", file=f)
 448                 print("write_btor {}-i design_{m}.info design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f)
 449
 450             task = SbyTask(
 451                 self,
 452                 model_name,
 453                 self.model("nomem" if "_nomem" in model_name else "base"),
 454                 "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name)
 455             )
 456             task.checkretcode = True
 457
 458             return [task]
 459
 460         if model_name == "aig":
 461             with open(f"{self.workdir}/model/design_aiger.ys", "w") as f:
 462                 print(f"# running in {self.workdir}/model/", file=f)
 463                 print("read_ilang design_nomem.il", file=f)
 464                 print("flatten", file=f)
 465                 print("setundef -undriven -anyseq", file=f)
 466                 print("setattr -unset keep", file=f)
 467                 print("delete -output", file=f)
 468                 print("opt -full", file=f)
 469                 print("techmap", file=f)
 470                 print("opt -fast", file=f)
 471                 print("dffunmap", file=f)
 472                 print("abc -g AND -fast", file=f)
 473                 print("opt_clean", file=f)
 474                 print("stat", file=f)
 475                 print("write_aiger -I -B -zinit -map design_aiger.aim design_aiger.aig", file=f)
 476
 477             task = SbyTask(
 478                 self,
 479                 "aig",
 480                 self.model("nomem"),
 481                 f"""cd {self.workdir}/model; {self.exe_paths["yosys"]} -ql design_aiger.log design_aiger.ys"""
 482             )
 483             task.checkretcode = True
 484
 485             return [task]
 486
 487         assert False
 488
 489     def model(self, model_name):
 490         if model_name not in self.models:
 491             self.models[model_name] = self.make_model(model_name)
 492         return self.models[model_name]
 493
 494     def terminate(self, timeout=False):
 495         for task in list(self.tasks_running):
 496             task.terminate(timeout=timeout)
 497
 498     def update_status(self, new_status):
 499         assert new_status in ["PASS", "FAIL", "UNKNOWN", "ERROR"]
 500
 501         if new_status == "UNKNOWN":
 502             return
 503
 504         if self.status == "ERROR":
 505             return
 506
 507         if new_status == "PASS":
 508             assert self.status != "FAIL"
 509             self.status = "PASS"
 510
 511         elif new_status == "FAIL":
 512             assert self.status != "PASS"
 513             self.status = "FAIL"
 514
 515         elif new_status == "ERROR":
 516             self.status = "ERROR"
 517
 518         else:
 519             assert 0
 520
 521     def run(self, setupmode):
 522         mode = None
 523         key = None
 524
 525         with open(f"{self.workdir}/config.sby", "r") as f:
 526             for line in f:
 527                 raw_line = line
 528                 if mode in ["options", "engines", "files"]:
 529                     line = re.sub(r"\s*(\s#.*)?$", "", line)
 530                     if line == "" or line[0] == "#":
 531                         continue
 532                 else:
 533                     line = line.rstrip()
 534                 # print(line)
 535                 if mode is None and (len(line) == 0 or line[0] == "#"):
 536                     continue
 537                 match = re.match(r"^\s*\[(.*)\]\s*$", line)
 538                 if match:
 539                     entries = match.group(1).split()
 540                     if len(entries) == 0:
 541                         self.error(f"sby file syntax error: {line}")
 542
 543                     if entries[0] == "options":
 544                         mode = "options"
 545                         if len(self.options) != 0 or len(entries) != 1:
 546                             self.error(f"sby file syntax error: {line}")
 547                         continue
 548
 549                     if entries[0] == "engines":
 550                         mode = "engines"
 551                         if len(self.engines) != 0 or len(entries) != 1:
 552                             self.error(f"sby file syntax error: {line}")
 553                         continue
 554
 555                     if entries[0] == "script":
 556                         mode = "script"
 557                         if len(self.script) != 0 or len(entries) != 1:
 558                             self.error(f"sby file syntax error: {line}")
 559                         continue
 560
 561                     if entries[0] == "file":
 562                         mode = "file"
 563                         if len(entries) != 2:
 564                             self.error(f"sby file syntax error: {line}")
 565                         current_verbatim_file = entries[1]
 566                         if current_verbatim_file in self.verbatim_files:
 567                             self.error(f"duplicate file: {entries[1]}")
 568                         self.verbatim_files[current_verbatim_file] = list()
 569                         continue
 570
 571                     if entries[0] == "files":
 572                         mode = "files"
 573                         if len(entries) != 1:
 574                             self.error(f"sby file syntax error: {line}")
 575                         continue
 576
 577                     self.error(f"sby file syntax error: {line}")
 578
 579                 if mode == "options":
 580                     entries = line.split()
 581                     if len(entries) != 2:
 582                         self.error(f"sby file syntax error: {line}")
 583                     self.options[entries[0]] = entries[1]
 584                     continue
 585
 586                 if mode == "engines":
 587                     entries = line.split()
 588                     self.engines.append(entries)
 589                     continue
 590
 591                 if mode == "script":
 592                     self.script.append(line)
 593                     continue
 594
 595                 if mode == "files":
 596                     entries = line.split()
 597                     if len(entries) == 1:
 598                         self.files[os.path.basename(entries[0])] = entries[0]
 599                     elif len(entries) == 2:
 600                         self.files[entries[0]] = entries[1]
 601                     else:
 602                         self.error(f"sby file syntax error: {line}")
 603                     continue
 604
 605                 if mode == "file":
 606                     self.verbatim_files[current_verbatim_file].append(raw_line)
 607                     continue
 608
 609                 self.error(f"sby file syntax error: {line}")
 610
 611         self.handle_str_option("mode", None)
 612
 613         if self.opt_mode not in ["bmc", "prove", "cover", "live"]:
 614             self.error(f"Invalid mode: {self.opt_mode}")
 615
 616         self.expect = ["PASS"]
 617         if "expect" in self.options:
 618             self.expect = self.options["expect"].upper().split(",")
 619             self.used_options.add("expect")
 620
 621         for s in self.expect:
 622             if s not in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"]:
 623                 self.error(f"Invalid expect value: {s}")
 624
 625         self.handle_bool_option("multiclock", False)
 626         self.handle_bool_option("wait", False)
 627         self.handle_int_option("timeout", None)
 628
 629         self.handle_str_option("smtc", None)
 630         self.handle_int_option("skip", None)
 631         self.handle_str_option("tbtop", None)
 632
 633         if self.opt_smtc is not None:
 634             for engine in self.engines:
 635                 if engine[0] != "smtbmc":
 636                     self.error("Option smtc is only valid for smtbmc engine.")
 637
 638         if self.opt_skip is not None:
 639             if self.opt_skip == 0:
 640                 self.opt_skip = None
 641             else:
 642                 for engine in self.engines:
 643                     if engine[0] not in ["smtbmc", "btor"]:
 644                         self.error("Option skip is only valid for smtbmc and btor engines.")
 645
 646         if len(self.engines) == 0:
 647             self.error("Config file is lacking engine configuration.")
 648
 649         if self.reusedir:
 650             rmtree(f"{self.workdir}/model", ignore_errors=True)
 651         else:
 652             self.copy_src()
 653
 654         if setupmode:
 655             self.retcode = 0
 656             return
 657
 658         if self.opt_mode == "bmc":
 659             import sby_mode_bmc
 660             sby_mode_bmc.run(self)
 661
 662         elif self.opt_mode == "prove":
 663             import sby_mode_prove
 664             sby_mode_prove.run(self)
 665
 666         elif self.opt_mode == "live":
 667             import sby_mode_live
 668             sby_mode_live.run(self)
 669
 670         elif self.opt_mode == "cover":
 671             import sby_mode_cover
 672             sby_mode_cover.run(self)
 673
 674         else:
 675             assert False
 676
 677         for opt in self.options.keys():
 678             if opt not in self.used_options:
 679                 self.error(f"Unused option: {opt}")
 680
 681         self.taskloop()
 682
 683         total_clock_time = int(time() - self.start_clock_time)
 684
 685         if os.name == "posix":
 686             ru = resource.getrusage(resource.RUSAGE_CHILDREN)
 687             total_process_time = int((ru.ru_utime + ru.ru_stime) - self.start_process_time)
 688             self.total_time = total_process_time
 689
 690             self.summary = [
 691                 "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format
 692                         (total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time),
 693                 "Elapsed process time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format
 694                         (total_process_time // (60*60), (total_process_time // 60) % 60, total_process_time % 60, total_process_time),
 695             ] + self.summary
 696         else:
 697             self.summary = [
 698                 "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format
 699                         (total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time),
 700                 "Elapsed process time unvailable on Windows"
 701             ] + self.summary
 702
 703         for line in self.summary:
 704             self.log(f"summary: {line}")
 705
 706         assert self.status in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"]
 707
 708         if self.status in self.expect:
 709             self.retcode = 0
 710         else:
 711             if self.status == "PASS": self.retcode = 1
 712             if self.status == "FAIL": self.retcode = 2
 713             if self.status == "UNKNOWN": self.retcode = 4
 714             if self.status == "TIMEOUT": self.retcode = 8
 715             if self.status == "ERROR": self.retcode = 16
 716
 717         with open(f"{self.workdir}/{self.status}", "w") as f:
 718             for line in self.summary:
 719                 print(line, file=f)