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