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