sbysrc/sby_core.py

   1 #
   2 # SymbiYosys (sby) -- Front-end for Yosys-based formal verification flows
   3 #
   4 # Copyright (C) 2016  Claire Xenia Wolf <claire@yosyshq.com>
   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, platform
  20 if os.name == "posix":
  21     import resource, fcntl
  22 import subprocess
  23 from shutil import copyfile, copytree, rmtree
  24 from select import select
  25 from time import time, localtime, sleep, strftime
  26 from sby_design import SbyProperty, SbyModule, design_hierarchy
  27
  28 all_procs_running = []
  29
  30 def force_shutdown(signum, frame):
  31     print("SBY ---- Keyboard interrupt or external termination signal ----", flush=True)
  32     for proc in list(all_procs_running):
  33         proc.terminate()
  34     sys.exit(1)
  35
  36 if os.name == "posix":
  37     signal.signal(signal.SIGHUP, force_shutdown)
  38 signal.signal(signal.SIGINT, force_shutdown)
  39 signal.signal(signal.SIGTERM, force_shutdown)
  40
  41 def process_filename(filename):
  42     if filename.startswith("~/"):
  43         filename = os.environ['HOME'] + filename[1:]
  44
  45     filename = os.path.expandvars(filename)
  46
  47     return filename
  48
  49 class SbyProc:
  50     def __init__(self, task, info, deps, cmdline, logfile=None, logstderr=True, silent=False):
  51         self.running = False
  52         self.finished = False
  53         self.terminated = False
  54         self.checkretcode = False
  55         self.retcodes = [0]
  56         self.task = task
  57         self.info = info
  58         self.deps = deps
  59         if os.name == "posix":
  60             self.cmdline = cmdline
  61         else:
  62             # Windows command interpreter equivalents for sequential
  63             # commands (; => &) command grouping ({} => ()).
  64             replacements = {
  65                 ";" : "&",
  66                 "{" : "(",
  67                 "}" : ")",
  68             }
  69             parts = cmdline.split("'")
  70             for i in range(len(parts)):
  71                 if i % 2 == 0:
  72                     cmdline_copy = parts[i]
  73                     for u, w in replacements.items():
  74                         cmdline_copy = cmdline_copy.replace(u, w)
  75                     parts[i] = cmdline_copy
  76             self.cmdline = '"'.join(parts)
  77         self.logfile = logfile
  78         self.noprintregex = None
  79         self.notify = []
  80         self.linebuffer = ""
  81         self.logstderr = logstderr
  82         self.silent = silent
  83
  84         self.task.procs_pending.append(self)
  85
  86         for dep in self.deps:
  87             dep.register_dep(self)
  88
  89         self.output_callback = None
  90         self.exit_callback = None
  91         self.error_callback = None
  92
  93     def register_dep(self, next_proc):
  94         if self.finished:
  95             next_proc.poll()
  96         else:
  97             self.notify.append(next_proc)
  98
  99     def log(self, line):
 100         if line is not None and (self.noprintregex is None or not self.noprintregex.match(line)):
 101             if self.logfile is not None:
 102                 print(line, file=self.logfile)
 103             self.task.log(f"{self.info}: {line}")
 104
 105     def handle_output(self, line):
 106         if self.terminated or len(line) == 0:
 107             return
 108         if self.output_callback is not None:
 109             line = self.output_callback(line)
 110         self.log(line)
 111
 112     def handle_exit(self, retcode):
 113         if self.terminated:
 114             return
 115         if self.logfile is not None:
 116             self.logfile.close()
 117         if self.exit_callback is not None:
 118             self.exit_callback(retcode)
 119
 120     def handle_error(self, retcode):
 121         if self.terminated:
 122             return
 123         if self.logfile is not None:
 124             self.logfile.close()
 125         if self.error_callback is not None:
 126             self.error_callback(retcode)
 127
 128     def terminate(self, timeout=False):
 129         if self.task.opt_wait and not timeout:
 130             return
 131         if self.running:
 132             if not self.silent:
 133                 self.task.log(f"{self.info}: terminating process")
 134             if os.name == "posix":
 135                 try:
 136                     os.killpg(self.p.pid, signal.SIGTERM)
 137                 except PermissionError:
 138                     pass
 139             self.p.terminate()
 140             self.task.procs_running.remove(self)
 141             all_procs_running.remove(self)
 142         self.terminated = True
 143
 144     def poll(self):
 145         if self.finished or self.terminated:
 146             return
 147
 148         if not self.running:
 149             for dep in self.deps:
 150                 if not dep.finished:
 151                     return
 152
 153             if not self.silent:
 154                 self.task.log(f"{self.info}: starting process \"{self.cmdline}\"")
 155
 156             if os.name == "posix":
 157                 def preexec_fn():
 158                     signal.signal(signal.SIGINT, signal.SIG_IGN)
 159                     os.setpgrp()
 160
 161                 self.p = subprocess.Popen(["/usr/bin/env", "bash", "-c", self.cmdline], stdin=subprocess.DEVNULL, stdout=subprocess.PIPE,
 162                         stderr=(subprocess.STDOUT if self.logstderr else None), preexec_fn=preexec_fn)
 163
 164                 fl = fcntl.fcntl(self.p.stdout, fcntl.F_GETFL)
 165                 fcntl.fcntl(self.p.stdout, fcntl.F_SETFL, fl | os.O_NONBLOCK)
 166
 167             else:
 168                 self.p = subprocess.Popen(self.cmdline, shell=True, stdin=subprocess.DEVNULL, stdout=subprocess.PIPE,
 169                         stderr=(subprocess.STDOUT if self.logstderr else None))
 170
 171             self.task.procs_pending.remove(self)
 172             self.task.procs_running.append(self)
 173             all_procs_running.append(self)
 174             self.running = True
 175             return
 176
 177         while True:
 178             outs = self.p.stdout.readline().decode("utf-8")
 179             if len(outs) == 0: break
 180             if outs[-1] != '\n':
 181                 self.linebuffer += outs
 182                 break
 183             outs = (self.linebuffer + outs).strip()
 184             self.linebuffer = ""
 185             self.handle_output(outs)
 186
 187         if self.p.poll() is not None:
 188             if not self.silent:
 189                 self.task.log(f"{self.info}: finished (returncode={self.p.returncode})")
 190             self.task.procs_running.remove(self)
 191             all_procs_running.remove(self)
 192             self.running = False
 193
 194             if self.p.returncode == 127:
 195                 self.task.status = "ERROR"
 196                 if not self.silent:
 197                     self.task.log(f"{self.info}: COMMAND NOT FOUND. ERROR.")
 198                 self.handle_error(self.p.returncode)
 199                 self.terminated = True
 200                 self.task.terminate()
 201                 return
 202
 203             if self.checkretcode and self.p.returncode not in self.retcodes:
 204                 self.task.status = "ERROR"
 205                 if not self.silent:
 206                     self.task.log(f"{self.info}: task failed. ERROR.")
 207                 self.handle_error(self.p.returncode)
 208                 self.terminated = True
 209                 self.task.terminate()
 210                 return
 211
 212             self.handle_exit(self.p.returncode)
 213
 214             self.finished = True
 215             for next_proc in self.notify:
 216                 next_proc.poll()
 217             return
 218
 219
 220 class SbyAbort(BaseException):
 221     pass
 222
 223
 224 class SbyConfig:
 225     def __init__(self):
 226         self.options = dict()
 227         self.engines = list()
 228         self.script = list()
 229         self.files = dict()
 230         self.verbatim_files = dict()
 231         pass
 232
 233     def parse_config(self, f):
 234         mode = None
 235
 236         for line in f:
 237             raw_line = line
 238             if mode in ["options", "engines", "files"]:
 239                 line = re.sub(r"\s*(\s#.*)?$", "", line)
 240                 if line == "" or line[0] == "#":
 241                     continue
 242             else:
 243                 line = line.rstrip()
 244             # print(line)
 245             if mode is None and (len(line) == 0 or line[0] == "#"):
 246                 continue
 247             match = re.match(r"^\s*\[(.*)\]\s*$", line)
 248             if match:
 249                 entries = match.group(1).split()
 250                 if len(entries) == 0:
 251                     self.error(f"sby file syntax error: {line}")
 252
 253                 if entries[0] == "options":
 254                     mode = "options"
 255                     if len(self.options) != 0 or len(entries) != 1:
 256                         self.error(f"sby file syntax error: {line}")
 257                     continue
 258
 259                 if entries[0] == "engines":
 260                     mode = "engines"
 261                     if len(self.engines) != 0 or len(entries) != 1:
 262                         self.error(f"sby file syntax error: {line}")
 263                     continue
 264
 265                 if entries[0] == "script":
 266                     mode = "script"
 267                     if len(self.script) != 0 or len(entries) != 1:
 268                         self.error(f"sby file syntax error: {line}")
 269                     continue
 270
 271                 if entries[0] == "file":
 272                     mode = "file"
 273                     if len(entries) != 2:
 274                         self.error(f"sby file syntax error: {line}")
 275                     current_verbatim_file = entries[1]
 276                     if current_verbatim_file in self.verbatim_files:
 277                         self.error(f"duplicate file: {entries[1]}")
 278                     self.verbatim_files[current_verbatim_file] = list()
 279                     continue
 280
 281                 if entries[0] == "files":
 282                     mode = "files"
 283                     if len(entries) != 1:
 284                         self.error(f"sby file syntax error: {line}")
 285                     continue
 286
 287                 self.error(f"sby file syntax error: {line}")
 288
 289             if mode == "options":
 290                 entries = line.split()
 291                 if len(entries) != 2:
 292                     self.error(f"sby file syntax error: {line}")
 293                 self.options[entries[0]] = entries[1]
 294                 continue
 295
 296             if mode == "engines":
 297                 entries = line.split()
 298                 self.engines.append(entries)
 299                 continue
 300
 301             if mode == "script":
 302                 self.script.append(line)
 303                 continue
 304
 305             if mode == "files":
 306                 entries = line.split()
 307                 if len(entries) == 1:
 308                     self.files[os.path.basename(entries[0])] = entries[0]
 309                 elif len(entries) == 2:
 310                     self.files[entries[0]] = entries[1]
 311                 else:
 312                     self.error(f"sby file syntax error: {line}")
 313                 continue
 314
 315             if mode == "file":
 316                 self.verbatim_files[current_verbatim_file].append(raw_line)
 317                 continue
 318
 319             self.error(f"sby file syntax error: {line}")
 320
 321     def error(self, logmessage):
 322         raise SbyAbort(logmessage)
 323
 324 class SbyTask(SbyConfig):
 325     def __init__(self, sbyconfig, workdir, early_logs, reusedir):
 326         super().__init__()
 327         self.used_options = set()
 328         self.models = dict()
 329         self.workdir = workdir
 330         self.reusedir = reusedir
 331         self.status = "UNKNOWN"
 332         self.total_time = 0
 333         self.expect = list()
 334         self.design_hierarchy = None
 335         self.precise_prop_status = False
 336
 337         yosys_program_prefix = "" ##yosys-program-prefix##
 338         self.exe_paths = {
 339             "yosys": os.getenv("YOSYS", yosys_program_prefix + "yosys"),
 340             "abc": os.getenv("ABC", yosys_program_prefix + "yosys-abc"),
 341             "smtbmc": os.getenv("SMTBMC", yosys_program_prefix + "yosys-smtbmc"),
 342             "suprove": os.getenv("SUPROVE", "suprove"),
 343             "aigbmc": os.getenv("AIGBMC", "aigbmc"),
 344             "avy": os.getenv("AVY", "avy"),
 345             "btormc": os.getenv("BTORMC", "btormc"),
 346             "pono": os.getenv("PONO", "pono"),
 347         }
 348
 349         self.procs_running = []
 350         self.procs_pending = []
 351
 352         self.start_clock_time = time()
 353
 354         if os.name == "posix":
 355             ru = resource.getrusage(resource.RUSAGE_CHILDREN)
 356             self.start_process_time = ru.ru_utime + ru.ru_stime
 357
 358         self.summary = list()
 359
 360         self.logfile = open(f"{workdir}/logfile.txt", "a")
 361
 362         for line in early_logs:
 363             print(line, file=self.logfile, flush=True)
 364
 365         if not reusedir:
 366             with open(f"{workdir}/config.sby", "w") as f:
 367                 for line in sbyconfig:
 368                     print(line, file=f)
 369
 370     def taskloop(self):
 371         for proc in self.procs_pending:
 372             proc.poll()
 373
 374         while len(self.procs_running):
 375             fds = []
 376             for proc in self.procs_running:
 377                 if proc.running:
 378                     fds.append(proc.p.stdout)
 379
 380             if os.name == "posix":
 381                 try:
 382                     select(fds, [], [], 1.0) == ([], [], [])
 383                 except InterruptedError:
 384                     pass
 385             else:
 386                 sleep(0.1)
 387
 388             for proc in self.procs_running:
 389                 proc.poll()
 390
 391             for proc in self.procs_pending:
 392                 proc.poll()
 393
 394             if self.opt_timeout is not None:
 395                 total_clock_time = int(time() - self.start_clock_time)
 396                 if total_clock_time > self.opt_timeout:
 397                     self.log(f"Reached TIMEOUT ({self.opt_timeout} seconds). Terminating all subprocesses.")
 398                     self.status = "TIMEOUT"
 399                     self.terminate(timeout=True)
 400
 401     def log(self, logmessage):
 402         tm = localtime()
 403         print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True)
 404         print("SBY {:2d}:{:02d}:{:02d} [{}] {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True)
 405
 406     def error(self, logmessage):
 407         tm = localtime()
 408         print("SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), flush=True)
 409         print("SBY {:2d}:{:02d}:{:02d} [{}] ERROR: {}".format(tm.tm_hour, tm.tm_min, tm.tm_sec, self.workdir, logmessage), file=self.logfile, flush=True)
 410         self.status = "ERROR"
 411         if "ERROR" not in self.expect:
 412             self.retcode = 16
 413         else:
 414             self.retcode = 0
 415         self.terminate()
 416         with open(f"{self.workdir}/{self.status}", "w") as f:
 417             print(f"ERROR: {logmessage}", file=f)
 418         raise SbyAbort(logmessage)
 419
 420     def makedirs(self, path):
 421         if self.reusedir and os.path.isdir(path):
 422             rmtree(path, ignore_errors=True)
 423         os.makedirs(path)
 424
 425     def copy_src(self):
 426         os.makedirs(self.workdir + "/src")
 427
 428         for dstfile, lines in self.verbatim_files.items():
 429             dstfile = self.workdir + "/src/" + dstfile
 430             self.log(f"Writing '{dstfile}'.")
 431
 432             with open(dstfile, "w") as f:
 433                 for line in lines:
 434                     f.write(line)
 435
 436         for dstfile, srcfile in self.files.items():
 437             if dstfile.startswith("/") or dstfile.startswith("../") or ("/../" in dstfile):
 438                 self.error(f"destination filename must be a relative path without /../: {dstfile}")
 439             dstfile = self.workdir + "/src/" + dstfile
 440
 441             srcfile = process_filename(srcfile)
 442
 443             basedir = os.path.dirname(dstfile)
 444             if basedir != "" and not os.path.exists(basedir):
 445                 os.makedirs(basedir)
 446
 447             self.log(f"Copy '{os.path.abspath(srcfile)}' to '{os.path.abspath(dstfile)}'.")
 448             if os.path.isdir(srcfile):
 449                 copytree(srcfile, dstfile, dirs_exist_ok=True)
 450             else:
 451                 copyfile(srcfile, dstfile)
 452
 453     def handle_str_option(self, option_name, default_value):
 454         if option_name in self.options:
 455             self.__dict__["opt_" + option_name] = self.options[option_name]
 456             self.used_options.add(option_name)
 457         else:
 458             self.__dict__["opt_" + option_name] = default_value
 459
 460     def handle_int_option(self, option_name, default_value):
 461         if option_name in self.options:
 462             self.__dict__["opt_" + option_name] = int(self.options[option_name])
 463             self.used_options.add(option_name)
 464         else:
 465             self.__dict__["opt_" + option_name] = default_value
 466
 467     def handle_bool_option(self, option_name, default_value):
 468         if option_name in self.options:
 469             if self.options[option_name] not in ["on", "off"]:
 470                 self.error(f"Invalid value '{self.options[option_name]}' for boolean option {option_name}.")
 471             self.__dict__["opt_" + option_name] = self.options[option_name] == "on"
 472             self.used_options.add(option_name)
 473         else:
 474             self.__dict__["opt_" + option_name] = default_value
 475
 476     def make_model(self, model_name):
 477         if not os.path.isdir(f"{self.workdir}/model"):
 478             os.makedirs(f"{self.workdir}/model")
 479
 480         def print_common_prep():
 481             if self.opt_multiclock:
 482                 print("clk2fflogic", file=f)
 483             else:
 484                 print("async2sync", file=f)
 485                 print("chformal -assume -early", file=f)
 486             if self.opt_mode in ["bmc", "prove"]:
 487                 print("chformal -live -fair -cover -remove", file=f)
 488             if self.opt_mode == "cover":
 489                 print("chformal -live -fair -remove", file=f)
 490             if self.opt_mode == "live":
 491                 print("chformal -assert2assume", file=f)
 492                 print("chformal -cover -remove", file=f)
 493             print("opt_clean", file=f)
 494             print("setundef -anyseq", file=f)
 495             print("opt -keepdc -fast", file=f)
 496             print("check", file=f)
 497             print("hierarchy -simcheck", file=f)
 498
 499         if model_name == "base":
 500             with open(f"""{self.workdir}/model/design.ys""", "w") as f:
 501                 print(f"# running in {self.workdir}/src/", file=f)
 502                 for cmd in self.script:
 503                     print(cmd, file=f)
 504                 # the user must designate a top module in [script]
 505                 print("hierarchy -simcheck", file=f)
 506                 print(f"""write_jny -no-connections ../model/design.json""", file=f)
 507                 print(f"""write_rtlil ../model/design.il""", file=f)
 508
 509             proc = SbyProc(
 510                 self,
 511                 model_name,
 512                 [],
 513                 "cd {}/src; {} -ql ../model/design.log ../model/design.ys".format(self.workdir, self.exe_paths["yosys"])
 514             )
 515             proc.checkretcode = True
 516
 517             def instance_hierarchy_callback(retcode):
 518                 if self.design_hierarchy == None:
 519                     with open(f"{self.workdir}/model/design.json") as f:
 520                         self.design_hierarchy = design_hierarchy(f)
 521
 522             def instance_hierarchy_error_callback(retcode):
 523                 self.precise_prop_status = False
 524
 525             proc.exit_callback = instance_hierarchy_callback
 526             proc.error_callback = instance_hierarchy_error_callback
 527
 528             return [proc]
 529
 530         if re.match(r"^smt2(_syn)?(_nomem)?(_stbv|_stdt)?$", model_name):
 531             with open(f"{self.workdir}/model/design_{model_name}.ys", "w") as f:
 532                 print(f"# running in {self.workdir}/model/", file=f)
 533                 print(f"""read_ilang design.il""", file=f)
 534                 if "_nomem" in model_name:
 535                     print("memory_map", file=f)
 536                 else:
 537                     print("memory_nordff", file=f)
 538                 print_common_prep()
 539                 if "_syn" in model_name:
 540                     print("techmap", file=f)
 541                     print("opt -fast", file=f)
 542                     print("abc", file=f)
 543                     print("opt_clean", file=f)
 544                 print("dffunmap", file=f)
 545                 print("stat", file=f)
 546                 if "_stbv" in model_name:
 547                     print(f"write_smt2 -stbv -wires design_{model_name}.smt2", file=f)
 548                 elif "_stdt" in model_name:
 549                     print(f"write_smt2 -stdt -wires design_{model_name}.smt2", file=f)
 550                 else:
 551                     print(f"write_smt2 -wires design_{model_name}.smt2", file=f)
 552
 553             proc = SbyProc(
 554                 self,
 555                 model_name,
 556                 self.model("base"),
 557                 "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name)
 558             )
 559             proc.checkretcode = True
 560
 561             return [proc]
 562
 563         if re.match(r"^btor(_syn)?(_nomem)?$", model_name):
 564             with open(f"{self.workdir}/model/design_{model_name}.ys", "w") as f:
 565                 print(f"# running in {self.workdir}/model/", file=f)
 566                 print(f"""read_ilang design.il""", file=f)
 567                 if "_nomem" in model_name:
 568                     print("memory_map", file=f)
 569                 else:
 570                     print("memory_nordff", file=f)
 571                 print_common_prep()
 572                 print("flatten", file=f)
 573                 print("setundef -undriven -anyseq", file=f)
 574                 if "_syn" in model_name:
 575                     print("opt -full", file=f)
 576                     print("techmap", file=f)
 577                     print("opt -fast", file=f)
 578                     print("abc", file=f)
 579                     print("opt_clean", file=f)
 580                 else:
 581                     print("opt -fast", file=f)
 582                 print("delete -output", file=f)
 583                 print("dffunmap", file=f)
 584                 print("stat", file=f)
 585                 print("write_btor {}-i design_{m}.info design_{m}.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f)
 586                 print("write_btor -s {}-i design_{m}_single.info design_{m}_single.btor".format("-c " if self.opt_mode == "cover" else "", m=model_name), file=f)
 587
 588             proc = SbyProc(
 589                 self,
 590                 model_name,
 591                 self.model("base"),
 592                 "cd {}/model; {} -ql design_{s}.log design_{s}.ys".format(self.workdir, self.exe_paths["yosys"], s=model_name)
 593             )
 594             proc.checkretcode = True
 595
 596             return [proc]
 597
 598         if model_name == "aig":
 599             with open(f"{self.workdir}/model/design_aiger.ys", "w") as f:
 600                 print(f"# running in {self.workdir}/model/", file=f)
 601                 print("read_ilang design.il", file=f)
 602                 print("memory_map", file=f)
 603                 print_common_prep()
 604                 print("flatten", file=f)
 605                 print("setundef -undriven -anyseq", file=f)
 606                 print("setattr -unset keep", file=f)
 607                 print("delete -output", file=f)
 608                 print("opt -full", file=f)
 609                 print("techmap", file=f)
 610                 print("opt -fast", file=f)
 611                 print("dffunmap", file=f)
 612                 print("abc -g AND -fast", file=f)
 613                 print("opt_clean", file=f)
 614                 print("stat", file=f)
 615                 print("write_aiger -I -B -zinit -no-startoffset -map design_aiger.aim design_aiger.aig", file=f)
 616
 617             proc = SbyProc(
 618                 self,
 619                 "aig",
 620                 self.model("base"),
 621                 f"""cd {self.workdir}/model; {self.exe_paths["yosys"]} -ql design_aiger.log design_aiger.ys"""
 622             )
 623             proc.checkretcode = True
 624
 625             return [proc]
 626
 627         assert False
 628
 629     def model(self, model_name):
 630         if model_name not in self.models:
 631             self.models[model_name] = self.make_model(model_name)
 632         return self.models[model_name]
 633
 634     def terminate(self, timeout=False):
 635         for proc in list(self.procs_running):
 636             proc.terminate(timeout=timeout)
 637
 638     def update_status(self, new_status):
 639         assert new_status in ["PASS", "FAIL", "UNKNOWN", "ERROR"]
 640
 641         if new_status == "UNKNOWN":
 642             return
 643
 644         if self.status == "ERROR":
 645             return
 646
 647         if new_status == "PASS":
 648             assert self.status != "FAIL"
 649             self.status = "PASS"
 650
 651         elif new_status == "FAIL":
 652             assert self.status != "PASS"
 653             self.status = "FAIL"
 654
 655         elif new_status == "ERROR":
 656             self.status = "ERROR"
 657
 658         else:
 659             assert 0
 660
 661     def run(self, setupmode):
 662         with open(f"{self.workdir}/config.sby", "r") as f:
 663             self.parse_config(f)
 664
 665         self.handle_str_option("mode", None)
 666
 667         if self.opt_mode not in ["bmc", "prove", "cover", "live"]:
 668             self.error(f"Invalid mode: {self.opt_mode}")
 669
 670         self.expect = ["PASS"]
 671         if "expect" in self.options:
 672             self.expect = self.options["expect"].upper().split(",")
 673             self.used_options.add("expect")
 674
 675         for s in self.expect:
 676             if s not in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"]:
 677                 self.error(f"Invalid expect value: {s}")
 678
 679         self.handle_bool_option("multiclock", False)
 680         self.handle_bool_option("wait", False)
 681         self.handle_int_option("timeout", None)
 682
 683         self.handle_str_option("smtc", None)
 684         self.handle_int_option("skip", None)
 685         self.handle_str_option("tbtop", None)
 686
 687         if self.opt_smtc is not None:
 688             for engine in self.engines:
 689                 if engine[0] != "smtbmc":
 690                     self.error("Option smtc is only valid for smtbmc engine.")
 691
 692         if self.opt_skip is not None:
 693             if self.opt_skip == 0:
 694                 self.opt_skip = None
 695             else:
 696                 for engine in self.engines:
 697                     if engine[0] not in ["smtbmc", "btor"]:
 698                         self.error("Option skip is only valid for smtbmc and btor engines.")
 699
 700         if len(self.engines) == 0:
 701             self.error("Config file is lacking engine configuration.")
 702
 703         if self.reusedir:
 704             rmtree(f"{self.workdir}/model", ignore_errors=True)
 705         else:
 706             self.copy_src()
 707
 708         if setupmode:
 709             self.retcode = 0
 710             return
 711
 712         if self.opt_mode == "bmc":
 713             import sby_mode_bmc
 714             sby_mode_bmc.run(self)
 715
 716         elif self.opt_mode == "prove":
 717             import sby_mode_prove
 718             sby_mode_prove.run(self)
 719
 720         elif self.opt_mode == "live":
 721             import sby_mode_live
 722             sby_mode_live.run(self)
 723
 724         elif self.opt_mode == "cover":
 725             import sby_mode_cover
 726             sby_mode_cover.run(self)
 727
 728         else:
 729             assert False
 730
 731         for opt in self.options.keys():
 732             if opt not in self.used_options:
 733                 self.error(f"Unused option: {opt}")
 734
 735         self.taskloop()
 736
 737         total_clock_time = int(time() - self.start_clock_time)
 738
 739         if os.name == "posix":
 740             ru = resource.getrusage(resource.RUSAGE_CHILDREN)
 741             total_process_time = int((ru.ru_utime + ru.ru_stime) - self.start_process_time)
 742             self.total_time = total_process_time
 743
 744             self.summary = [
 745                 "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format
 746                         (total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time),
 747                 "Elapsed process time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format
 748                         (total_process_time // (60*60), (total_process_time // 60) % 60, total_process_time % 60, total_process_time),
 749             ] + self.summary
 750         else:
 751             self.summary = [
 752                 "Elapsed clock time [H:MM:SS (secs)]: {}:{:02d}:{:02d} ({})".format
 753                         (total_clock_time // (60*60), (total_clock_time // 60) % 60, total_clock_time % 60, total_clock_time),
 754                 "Elapsed process time unvailable on Windows"
 755             ] + self.summary
 756
 757         for line in self.summary:
 758             self.log(f"summary: {line}")
 759
 760         assert self.status in ["PASS", "FAIL", "UNKNOWN", "ERROR", "TIMEOUT"]
 761
 762         if self.status in self.expect:
 763             self.retcode = 0
 764         else:
 765             if self.status == "PASS": self.retcode = 1
 766             if self.status == "FAIL": self.retcode = 2
 767             if self.status == "UNKNOWN": self.retcode = 4
 768             if self.status == "TIMEOUT": self.retcode = 8
 769             if self.status == "ERROR": self.retcode = 16
 770
 771         with open(f"{self.workdir}/{self.status}", "w") as f:
 772             for line in self.summary:
 773                 print(line, file=f)
 774
 775     def print_junit_result(self, f, junit_ts_name, junit_tc_name, junit_format_strict=False):
 776         junit_time = strftime('%Y-%m-%dT%H:%M:%S')
 777         if self.precise_prop_status:
 778             checks = self.design_hierarchy.get_property_list()
 779             junit_tests = len(checks)
 780             junit_failures = 0
 781             junit_errors = 0
 782             junit_skipped = 0
 783             for check in checks:
 784                 if check.status == "PASS":
 785                     pass
 786                 elif check.status == "FAIL":
 787                     junit_failures += 1
 788                 elif check.status == "UNKNOWN":
 789                     junit_skipped += 1
 790                 else:
 791                     junit_errors += 1
 792             if self.retcode == 16:
 793                 junit_errors += 1
 794             elif self.retcode != 0:
 795                 junit_failures += 1
 796         else:
 797             junit_tests = 1
 798             junit_errors = 1 if self.retcode == 16 else 0
 799             junit_failures = 1 if self.retcode != 0 and junit_errors == 0 else 0
 800             junit_skipped = 0
 801         print(f'<?xml version="1.0" encoding="UTF-8"?>', file=f)
 802         print(f'<testsuites>', file=f)
 803         print(f'<testsuite timestamp="{junit_time}" hostname="{platform.node()}" package="{junit_ts_name}" id="0" name="{junit_tc_name}" tests="{junit_tests}" errors="{junit_errors}" failures="{junit_failures}" time="{self.total_time}" skipped="{junit_skipped}">', file=f)
 804         print(f'<properties>', file=f)
 805         print(f'<property name="os" value="{platform.system()}"/>', file=f)
 806         print(f'<property name="expect" value="{", ".join(self.expect)}"/>', file=f)
 807         print(f'<property name="status" value="{self.status}"/>', file=f)
 808         print(f'</properties>', file=f)
 809         if self.precise_prop_status:
 810             print(f'<testcase classname="{junit_tc_name}" name="build execution" time="0">', file=f)
 811             if self.retcode == 16:
 812                 print(f'<error type="ERROR"/>', file=f) # type mandatory, message optional
 813             elif self.retcode != 0:
 814                 if len(self.expect) > 1 or "PASS" not in self.expect:
 815                     expected = " ".join(self.expect)
 816                     print(f'<failure type="EXPECT" message="Task returned status {self.status}. Expected values were: {expected}" />', file=f)
 817                 else:
 818                     print(f'<failure type="{self.status}" message="Task returned status {self.status}." />', file=f)
 819             print(f'</testcase>', file=f)
 820
 821             for check in checks:
 822                 if junit_format_strict:
 823                     detail_attrs = ''
 824                 else:
 825                     detail_attrs = f' type="{check.type}" location="{check.location}" id="{check.name}"'
 826                     if check.tracefile:
 827                         detail_attrs += f' tracefile="{check.tracefile}"'
 828                 if check.location:
 829                     junit_prop_name = f"Property {check.type} in {check.hierarchy} at {check.location}"
 830                 else:
 831                     junit_prop_name = f"Property {check.type} {check.name} in {check.hierarchy}"
 832                 print(f'<testcase classname="{junit_tc_name}" name="{junit_prop_name}" time="0"{detail_attrs}>', file=f)
 833                 if check.status == "PASS":
 834                     pass
 835                 elif check.status == "UNKNOWN":
 836                     print(f'<skipped />', file=f)
 837                 elif check.status == "FAIL":
 838                     traceinfo = f' Trace file: {check.tracefile}' if check.type == check.Type.ASSERT else ''
 839                     print(f'<failure type="{check.type}" message="{junit_prop_name} failed.{traceinfo}" />', file=f)
 840                 elif check.status == "ERROR":
 841                     print(f'<error type="ERROR"/>', file=f) # type mandatory, message optional
 842                 print(f'</testcase>', file=f)
 843         else:
 844             print(f'<testcase classname="{junit_tc_name}" name="{junit_tc_name}" time="{self.total_time}">', file=f)
 845             if junit_errors:
 846                 print(f'<error type="ERROR"/>', file=f) # type mandatory, message optional
 847             elif junit_failures:
 848                 junit_type = "assert" if self.opt_mode in ["bmc", "prove"] else self.opt_mode
 849                 print(f'<failure type="{junit_type}" message="{self.status}" />', file=f)
 850             print(f'</testcase>', file=f)
 851         print('<system-out>', end="", file=f)
 852         with open(f"{self.workdir}/logfile.txt", "r") as logf:
 853             for line in logf:
 854                 print(line.replace("&", "&amp;").replace("<", "&lt;").replace(">", "&gt;").replace("\"", "&quot;"), end="", file=f)
 855         print('</system-out>', file=f)
 856         print('<system-err>', file=f)
 857         #TODO: can we handle errors and still output this file?
 858         print('</system-err>', file=f)
 859         print(f'</testsuite>', file=f)
 860         print(f'</testsuites>', file=f)