backends/smt2/smtio.py

   1 #
   2 # yosys -- Yosys Open SYnthesis Suite
   3 #
   4 # Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
   5 #
   6 # Permission to use, copy, modify, and/or distribute this software for any
   7 # purpose with or without fee is hereby granted, provided that the above
   8 # copyright notice and this permission notice appear in all copies.
   9 #
  10 # THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  11 # WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  12 # MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  13 # ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  14 # WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  15 # ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  16 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  17 #
  18
  19 import sys, re, os, signal
  20 import subprocess
  21 if os.name == "posix":
  22     import resource
  23 from copy import deepcopy
  24 from select import select
  25 from time import time
  26 from queue import Queue, Empty
  27 from threading import Thread
  28
  29
  30 # This is needed so that the recursive SMT2 S-expression parser
  31 # does not run out of stack frames when parsing large expressions
  32 if os.name == "posix":
  33     smtio_reclimit = 64 * 1024
  34     if sys.getrecursionlimit() < smtio_reclimit:
  35         sys.setrecursionlimit(smtio_reclimit)
  36
  37     current_rlimit_stack = resource.getrlimit(resource.RLIMIT_STACK)
  38     if current_rlimit_stack[0] != resource.RLIM_INFINITY:
  39         smtio_stacksize = 128 * 1024 * 1024
  40         if os.uname().sysname == "Darwin":
  41             # MacOS has rather conservative stack limits
  42             smtio_stacksize = 16 * 1024 * 1024
  43         if current_rlimit_stack[1] != resource.RLIM_INFINITY:
  44             smtio_stacksize = min(smtio_stacksize, current_rlimit_stack[1])
  45         if current_rlimit_stack[0] < smtio_stacksize:
  46             try:
  47                 resource.setrlimit(resource.RLIMIT_STACK, (smtio_stacksize, current_rlimit_stack[1]))
  48             except ValueError:
  49                 # couldn't get more stack, just run with what we have
  50                 pass
  51
  52
  53 # currently running solvers (so we can kill them)
  54 running_solvers = dict()
  55 forced_shutdown = False
  56 solvers_index = 0
  57
  58 def force_shutdown(signum, frame):
  59     global forced_shutdown
  60     if not forced_shutdown:
  61         forced_shutdown = True
  62         if signum is not None:
  63             print("<%s>" % signal.Signals(signum).name)
  64         for p in running_solvers.values():
  65             # os.killpg(os.getpgid(p.pid), signal.SIGTERM)
  66             os.kill(p.pid, signal.SIGTERM)
  67     sys.exit(1)
  68
  69 if os.name == "posix":
  70     signal.signal(signal.SIGHUP, force_shutdown)
  71 signal.signal(signal.SIGINT, force_shutdown)
  72 signal.signal(signal.SIGTERM, force_shutdown)
  73
  74 def except_hook(exctype, value, traceback):
  75     if not forced_shutdown:
  76         sys.__excepthook__(exctype, value, traceback)
  77     force_shutdown(None, None)
  78
  79 sys.excepthook = except_hook
  80
  81
  82 hex_dict = {
  83     "0": "0000", "1": "0001", "2": "0010", "3": "0011",
  84     "4": "0100", "5": "0101", "6": "0110", "7": "0111",
  85     "8": "1000", "9": "1001", "A": "1010", "B": "1011",
  86     "C": "1100", "D": "1101", "E": "1110", "F": "1111",
  87     "a": "1010", "b": "1011", "c": "1100", "d": "1101",
  88     "e": "1110", "f": "1111"
  89 }
  90
  91
  92 class SmtModInfo:
  93     def __init__(self):
  94         self.inputs = set()
  95         self.outputs = set()
  96         self.registers = set()
  97         self.memories = dict()
  98         self.wires = set()
  99         self.wsize = dict()
 100         self.clocks = dict()
 101         self.cells = dict()
 102         self.asserts = dict()
 103         self.covers = dict()
 104         self.maximize = set()
 105         self.minimize = set()
 106         self.anyconsts = dict()
 107         self.anyseqs = dict()
 108         self.allconsts = dict()
 109         self.allseqs = dict()
 110         self.asize = dict()
 111
 112
 113 class SmtIo:
 114     def __init__(self, opts=None):
 115         global solvers_index
 116
 117         self.logic = None
 118         self.logic_qf = True
 119         self.logic_ax = True
 120         self.logic_uf = True
 121         self.logic_bv = True
 122         self.logic_dt = False
 123         self.forall = False
 124         self.timeout = 0
 125         self.produce_models = True
 126         self.smt2cache = [list()]
 127         self.p = None
 128         self.p_index = solvers_index
 129         solvers_index += 1
 130
 131         if opts is not None:
 132             self.logic = opts.logic
 133             self.solver = opts.solver
 134             self.solver_opts = opts.solver_opts
 135             self.debug_print = opts.debug_print
 136             self.debug_file = opts.debug_file
 137             self.dummy_file = opts.dummy_file
 138             self.timeinfo = opts.timeinfo
 139             self.timeout = opts.timeout
 140             self.unroll = opts.unroll
 141             self.noincr = opts.noincr
 142             self.info_stmts = opts.info_stmts
 143             self.nocomments = opts.nocomments
 144
 145         else:
 146             self.solver = "yices"
 147             self.solver_opts = list()
 148             self.debug_print = False
 149             self.debug_file = None
 150             self.dummy_file = None
 151             self.timeinfo = os.name != "nt"
 152             self.timeout = 0
 153             self.unroll = False
 154             self.noincr = False
 155             self.info_stmts = list()
 156             self.nocomments = False
 157
 158         self.start_time = time()
 159
 160         self.modinfo = dict()
 161         self.curmod = None
 162         self.topmod = None
 163         self.setup_done = False
 164
 165     def __del__(self):
 166         if self.p is not None and not forced_shutdown:
 167             os.killpg(os.getpgid(self.p.pid), signal.SIGTERM)
 168             if running_solvers is not None:
 169                 del running_solvers[self.p_index]
 170
 171     def setup(self):
 172         assert not self.setup_done
 173
 174         if self.forall:
 175             self.unroll = False
 176
 177         if self.solver == "yices":
 178             if self.noincr or self.forall:
 179                 self.popen_vargs = ['yices-smt2'] + self.solver_opts
 180             else:
 181                 self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
 182             if self.timeout != 0:
 183                 self.popen_vargs.append('-t')
 184                 self.popen_vargs.append('%d' % self.timeout);
 185
 186         if self.solver == "z3":
 187             self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
 188             if self.timeout != 0:
 189                 self.popen_vargs.append('-T:%d' % self.timeout);
 190
 191         if self.solver == "cvc4":
 192             if self.noincr:
 193                 self.popen_vargs = ['cvc4', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
 194             else:
 195                 self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
 196             if self.timeout != 0:
 197                 self.popen_vargs.append('--tlimit=%d000' % self.timeout);
 198
 199         if self.solver == "mathsat":
 200             self.popen_vargs = ['mathsat'] + self.solver_opts
 201             if self.timeout != 0:
 202                 print('timeout option is not supported for mathsat.')
 203                 sys.exit(1)
 204
 205         if self.solver == "boolector":
 206             if self.noincr:
 207                 self.popen_vargs = ['boolector', '--smt2'] + self.solver_opts
 208             else:
 209                 self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
 210             self.unroll = True
 211             if self.timeout != 0:
 212                 print('timeout option is not supported for boolector.')
 213                 sys.exit(1)
 214
 215         if self.solver == "abc":
 216             if len(self.solver_opts) > 0:
 217                 self.popen_vargs = ['yosys-abc', '-S', '; '.join(self.solver_opts)]
 218             else:
 219                 self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
 220             self.logic_ax = False
 221             self.unroll = True
 222             self.noincr = True
 223             if self.timeout != 0:
 224                 print('timeout option is not supported for abc.')
 225                 sys.exit(1)
 226
 227         if self.solver == "dummy":
 228             assert self.dummy_file is not None
 229             self.dummy_fd = open(self.dummy_file, "r")
 230         else:
 231             if self.dummy_file is not None:
 232                 self.dummy_fd = open(self.dummy_file, "w")
 233             if not self.noincr:
 234                 self.p_open()
 235
 236         if self.unroll:
 237             assert not self.forall
 238             self.logic_uf = False
 239             self.unroll_idcnt = 0
 240             self.unroll_buffer = ""
 241             self.unroll_sorts = set()
 242             self.unroll_objs = set()
 243             self.unroll_decls = dict()
 244             self.unroll_cache = dict()
 245             self.unroll_stack = list()
 246
 247         if self.logic is None:
 248             self.logic = ""
 249             if self.logic_qf: self.logic += "QF_"
 250             if self.logic_ax: self.logic += "A"
 251             if self.logic_uf: self.logic += "UF"
 252             if self.logic_bv: self.logic += "BV"
 253             if self.logic_dt: self.logic = "ALL"
 254             if self.solver == "yices" and self.forall: self.logic = "BV"
 255
 256         self.setup_done = True
 257
 258         for stmt in self.info_stmts:
 259             self.write(stmt)
 260
 261         if self.forall and self.solver == "yices":
 262             self.write("(set-option :yices-ef-max-iters 1000000000)")
 263
 264         if self.produce_models:
 265             self.write("(set-option :produce-models true)")
 266
 267         self.write("(set-logic %s)" % self.logic)
 268
 269     def timestamp(self):
 270         secs = int(time() - self.start_time)
 271         return "## %3d:%02d:%02d " % (secs // (60*60), (secs // 60) % 60, secs % 60)
 272
 273     def replace_in_stmt(self, stmt, pat, repl):
 274         if stmt == pat:
 275             return repl
 276
 277         if isinstance(stmt, list):
 278             return [self.replace_in_stmt(s, pat, repl) for s in stmt]
 279
 280         return stmt
 281
 282     def unroll_stmt(self, stmt):
 283         if not isinstance(stmt, list):
 284             return stmt
 285
 286         stmt = [self.unroll_stmt(s) for s in stmt]
 287
 288         if len(stmt) >= 2 and not isinstance(stmt[0], list) and stmt[0] in self.unroll_decls:
 289             assert stmt[1] in self.unroll_objs
 290
 291             key = tuple(stmt)
 292             if key not in self.unroll_cache:
 293                 decl = deepcopy(self.unroll_decls[key[0]])
 294
 295                 self.unroll_cache[key] = "|UNROLL#%d|" % self.unroll_idcnt
 296                 decl[1] = self.unroll_cache[key]
 297                 self.unroll_idcnt += 1
 298
 299                 if decl[0] == "declare-fun":
 300                     if isinstance(decl[3], list) or decl[3] not in self.unroll_sorts:
 301                         self.unroll_objs.add(decl[1])
 302                         decl[2] = list()
 303                     else:
 304                         self.unroll_objs.add(decl[1])
 305                         decl = list()
 306
 307                 elif decl[0] == "define-fun":
 308                     arg_index = 1
 309                     for arg_name, arg_sort in decl[2]:
 310                         decl[4] = self.replace_in_stmt(decl[4], arg_name, key[arg_index])
 311                         arg_index += 1
 312                     decl[2] = list()
 313
 314                 if len(decl) > 0:
 315                     decl = self.unroll_stmt(decl)
 316                     self.write(self.unparse(decl), unroll=False)
 317
 318             return self.unroll_cache[key]
 319
 320         return stmt
 321
 322     def p_thread_main(self):
 323         while True:
 324             data = self.p.stdout.readline().decode("ascii")
 325             if data == "": break
 326             self.p_queue.put(data)
 327         self.p_queue.put("")
 328         self.p_running = False
 329
 330     def p_open(self):
 331         assert self.p is None
 332         try:
 333             self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
 334         except FileNotFoundError:
 335             print("%s SMT Solver '%s' not found in path." % (self.timestamp(), self.popen_vargs[0]), flush=True)
 336             sys.exit(1)
 337         running_solvers[self.p_index] = self.p
 338         self.p_running = True
 339         self.p_next = None
 340         self.p_queue = Queue()
 341         self.p_thread = Thread(target=self.p_thread_main)
 342         self.p_thread.start()
 343
 344     def p_write(self, data, flush):
 345         assert self.p is not None
 346         self.p.stdin.write(bytes(data, "ascii"))
 347         if flush: self.p.stdin.flush()
 348
 349     def p_read(self):
 350         assert self.p is not None
 351         if self.p_next is not None:
 352             data = self.p_next
 353             self.p_next = None
 354             return data
 355         if not self.p_running:
 356             return ""
 357         return self.p_queue.get()
 358
 359     def p_poll(self, timeout=0.1):
 360         assert self.p is not None
 361         assert self.p_running
 362         if self.p_next is not None:
 363             return False
 364         try:
 365             self.p_next = self.p_queue.get(True, timeout)
 366             return False
 367         except Empty:
 368             return True
 369
 370     def p_close(self):
 371         assert self.p is not None
 372         self.p.stdin.close()
 373         self.p_thread.join()
 374         assert not self.p_running
 375         del running_solvers[self.p_index]
 376         self.p = None
 377         self.p_next = None
 378         self.p_queue = None
 379         self.p_thread = None
 380
 381     def write(self, stmt, unroll=True):
 382         if stmt.startswith(";"):
 383             self.info(stmt)
 384             if not self.setup_done:
 385                 self.info_stmts.append(stmt)
 386                 return
 387         elif not self.setup_done:
 388             self.setup()
 389
 390         stmt = stmt.strip()
 391
 392         if self.nocomments or self.unroll:
 393             stmt = re.sub(r" *;.*", "", stmt)
 394             if stmt == "": return
 395
 396         if unroll and self.unroll:
 397             stmt = self.unroll_buffer + stmt
 398             self.unroll_buffer = ""
 399
 400             s = re.sub(r"\|[^|]*\|", "", stmt)
 401             if s.count("(") != s.count(")"):
 402                 self.unroll_buffer = stmt + " "
 403                 return
 404
 405             s = self.parse(stmt)
 406
 407             if self.debug_print:
 408                 print("-> %s" % s)
 409
 410             if len(s) == 3 and s[0] == "declare-sort" and s[2] == "0":
 411                 self.unroll_sorts.add(s[1])
 412                 return
 413
 414             elif len(s) == 4 and s[0] == "declare-fun" and s[2] == [] and s[3] in self.unroll_sorts:
 415                 self.unroll_objs.add(s[1])
 416                 return
 417
 418             elif len(s) >= 4 and s[0] == "declare-fun":
 419                 for arg_sort in s[2]:
 420                     if arg_sort in self.unroll_sorts:
 421                         self.unroll_decls[s[1]] = s
 422                         return
 423
 424             elif len(s) >= 4 and s[0] == "define-fun":
 425                 for arg_name, arg_sort in s[2]:
 426                     if arg_sort in self.unroll_sorts:
 427                         self.unroll_decls[s[1]] = s
 428                         return
 429
 430             stmt = self.unparse(self.unroll_stmt(s))
 431
 432             if stmt == "(push 1)":
 433                 self.unroll_stack.append((
 434                     deepcopy(self.unroll_sorts),
 435                     deepcopy(self.unroll_objs),
 436                     deepcopy(self.unroll_decls),
 437                     deepcopy(self.unroll_cache),
 438                 ))
 439
 440             if stmt == "(pop 1)":
 441                 self.unroll_sorts, self.unroll_objs, self.unroll_decls, self.unroll_cache = self.unroll_stack.pop()
 442
 443         if self.debug_print:
 444             print("> %s" % stmt)
 445
 446         if self.debug_file:
 447             print(stmt, file=self.debug_file)
 448             self.debug_file.flush()
 449
 450         if self.solver != "dummy":
 451             if self.noincr:
 452                 if self.p is not None and not stmt.startswith("(get-"):
 453                     self.p_close()
 454                 if stmt == "(push 1)":
 455                     self.smt2cache.append(list())
 456                 elif stmt == "(pop 1)":
 457                     self.smt2cache.pop()
 458                 else:
 459                     if self.p is not None:
 460                         self.p_write(stmt + "\n", True)
 461                     self.smt2cache[-1].append(stmt)
 462             else:
 463                 self.p_write(stmt + "\n", True)
 464
 465     def info(self, stmt):
 466         if not stmt.startswith("; yosys-smt2-"):
 467             return
 468
 469         fields = stmt.split()
 470
 471         if fields[1] == "yosys-smt2-nomem":
 472             if self.logic is None:
 473                 self.logic_ax = False
 474
 475         if fields[1] == "yosys-smt2-nobv":
 476             if self.logic is None:
 477                 self.logic_bv = False
 478
 479         if fields[1] == "yosys-smt2-stdt":
 480             if self.logic is None:
 481                 self.logic_dt = True
 482
 483         if fields[1] == "yosys-smt2-forall":
 484             if self.logic is None:
 485                 self.logic_qf = False
 486             self.forall = True
 487
 488         if fields[1] == "yosys-smt2-module":
 489             self.curmod = fields[2]
 490             self.modinfo[self.curmod] = SmtModInfo()
 491
 492         if fields[1] == "yosys-smt2-cell":
 493             self.modinfo[self.curmod].cells[fields[3]] = fields[2]
 494
 495         if fields[1] == "yosys-smt2-topmod":
 496             self.topmod = fields[2]
 497
 498         if fields[1] == "yosys-smt2-input":
 499             self.modinfo[self.curmod].inputs.add(fields[2])
 500             self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
 501
 502         if fields[1] == "yosys-smt2-output":
 503             self.modinfo[self.curmod].outputs.add(fields[2])
 504             self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
 505
 506         if fields[1] == "yosys-smt2-register":
 507             self.modinfo[self.curmod].registers.add(fields[2])
 508             self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
 509
 510         if fields[1] == "yosys-smt2-memory":
 511             self.modinfo[self.curmod].memories[fields[2]] = (int(fields[3]), int(fields[4]), int(fields[5]), int(fields[6]), fields[7] == "async")
 512
 513         if fields[1] == "yosys-smt2-wire":
 514             self.modinfo[self.curmod].wires.add(fields[2])
 515             self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
 516
 517         if fields[1] == "yosys-smt2-clock":
 518             for edge in fields[3:]:
 519                 if fields[2] not in self.modinfo[self.curmod].clocks:
 520                     self.modinfo[self.curmod].clocks[fields[2]] = edge
 521                 elif self.modinfo[self.curmod].clocks[fields[2]] != edge:
 522                     self.modinfo[self.curmod].clocks[fields[2]] = "event"
 523
 524         if fields[1] == "yosys-smt2-assert":
 525             self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3]
 526
 527         if fields[1] == "yosys-smt2-cover":
 528             self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
 529
 530         if fields[1] == "yosys-smt2-maximize":
 531             self.modinfo[self.curmod].maximize.add(fields[2])
 532
 533         if fields[1] == "yosys-smt2-minimize":
 534             self.modinfo[self.curmod].minimize.add(fields[2])
 535
 536         if fields[1] == "yosys-smt2-anyconst":
 537             self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
 538             self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
 539
 540         if fields[1] == "yosys-smt2-anyseq":
 541             self.modinfo[self.curmod].anyseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
 542             self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
 543
 544         if fields[1] == "yosys-smt2-allconst":
 545             self.modinfo[self.curmod].allconsts[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
 546             self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
 547
 548         if fields[1] == "yosys-smt2-allseq":
 549             self.modinfo[self.curmod].allseqs[fields[2]] = (fields[4], None if len(fields) <= 5 else fields[5])
 550             self.modinfo[self.curmod].asize[fields[2]] = int(fields[3])
 551
 552     def hiernets(self, top, regs_only=False):
 553         def hiernets_worker(nets, mod, cursor):
 554             for netname in sorted(self.modinfo[mod].wsize.keys()):
 555                 if not regs_only or netname in self.modinfo[mod].registers:
 556                     nets.append(cursor + [netname])
 557             for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
 558                 hiernets_worker(nets, celltype, cursor + [cellname])
 559
 560         nets = list()
 561         hiernets_worker(nets, top, [])
 562         return nets
 563
 564     def hieranyconsts(self, top):
 565         def worker(results, mod, cursor):
 566             for name, value in sorted(self.modinfo[mod].anyconsts.items()):
 567                 width = self.modinfo[mod].asize[name]
 568                 results.append((cursor, name, value[0], value[1], width))
 569             for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
 570                 worker(results, celltype, cursor + [cellname])
 571
 572         results = list()
 573         worker(results, top, [])
 574         return results
 575
 576     def hieranyseqs(self, top):
 577         def worker(results, mod, cursor):
 578             for name, value in sorted(self.modinfo[mod].anyseqs.items()):
 579                 width = self.modinfo[mod].asize[name]
 580                 results.append((cursor, name, value[0], value[1], width))
 581             for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
 582                 worker(results, celltype, cursor + [cellname])
 583
 584         results = list()
 585         worker(results, top, [])
 586         return results
 587
 588     def hierallconsts(self, top):
 589         def worker(results, mod, cursor):
 590             for name, value in sorted(self.modinfo[mod].allconsts.items()):
 591                 width = self.modinfo[mod].asize[name]
 592                 results.append((cursor, name, value[0], value[1], width))
 593             for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
 594                 worker(results, celltype, cursor + [cellname])
 595
 596         results = list()
 597         worker(results, top, [])
 598         return results
 599
 600     def hierallseqs(self, top):
 601         def worker(results, mod, cursor):
 602             for name, value in sorted(self.modinfo[mod].allseqs.items()):
 603                 width = self.modinfo[mod].asize[name]
 604                 results.append((cursor, name, value[0], value[1], width))
 605             for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
 606                 worker(results, celltype, cursor + [cellname])
 607
 608         results = list()
 609         worker(results, top, [])
 610         return results
 611
 612     def hiermems(self, top):
 613         def hiermems_worker(mems, mod, cursor):
 614             for memname in sorted(self.modinfo[mod].memories.keys()):
 615                 mems.append(cursor + [memname])
 616             for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
 617                 hiermems_worker(mems, celltype, cursor + [cellname])
 618
 619         mems = list()
 620         hiermems_worker(mems, top, [])
 621         return mems
 622
 623     def read(self):
 624         stmt = []
 625         count_brackets = 0
 626
 627         while True:
 628             if self.solver == "dummy":
 629                 line = self.dummy_fd.readline().strip()
 630             else:
 631                 line = self.p_read().strip()
 632                 if self.dummy_file is not None:
 633                     self.dummy_fd.write(line + "\n")
 634
 635             count_brackets += line.count("(")
 636             count_brackets -= line.count(")")
 637             stmt.append(line)
 638
 639             if self.debug_print:
 640                 print("< %s" % line)
 641             if count_brackets == 0:
 642                 break
 643             if self.solver != "dummy" and self.p.poll():
 644                 print("%s Solver terminated unexpectedly: %s" % (self.timestamp(), "".join(stmt)), flush=True)
 645                 sys.exit(1)
 646
 647         stmt = "".join(stmt)
 648         if stmt.startswith("(error"):
 649             print("%s Solver Error: %s" % (self.timestamp(), stmt), flush=True)
 650             if self.solver != "dummy":
 651                 self.p_close()
 652             sys.exit(1)
 653
 654         return stmt
 655
 656     def check_sat(self):
 657         if self.debug_print:
 658             print("> (check-sat)")
 659         if self.debug_file and not self.nocomments:
 660             print("; running check-sat..", file=self.debug_file)
 661             self.debug_file.flush()
 662
 663         if self.solver != "dummy":
 664             if self.noincr:
 665                 if self.p is not None:
 666                     self.p_close()
 667                 self.p_open()
 668                 for cache_ctx in self.smt2cache:
 669                     for cache_stmt in cache_ctx:
 670                         self.p_write(cache_stmt + "\n", False)
 671
 672             self.p_write("(check-sat)\n", True)
 673
 674             if self.timeinfo:
 675                 i = 0
 676                 s = "/-\|"
 677
 678                 count = 0
 679                 num_bs = 0
 680                 while self.p_poll():
 681                     count += 1
 682
 683                     if count < 25:
 684                         continue
 685
 686                     if count % 10 == 0 or count == 25:
 687                         secs = count // 10
 688
 689                         if secs < 60:
 690                             m = "(%d seconds)" % secs
 691                         elif secs < 60*60:
 692                             m = "(%d seconds -- %d:%02d)" % (secs, secs // 60, secs % 60)
 693                         else:
 694                             m = "(%d seconds -- %d:%02d:%02d)" % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
 695
 696                         print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="", file=sys.stderr)
 697                         num_bs = len(m) + 3
 698
 699                     else:
 700                         print("\b" + s[i], end="", file=sys.stderr)
 701
 702                     sys.stderr.flush()
 703                     i = (i + 1) % len(s)
 704
 705                 if num_bs != 0:
 706                     print("\b \b" * num_bs, end="", file=sys.stderr)
 707                     sys.stderr.flush()
 708
 709             else:
 710                 count = 0
 711                 while self.p_poll(60):
 712                     count += 1
 713                     msg = None
 714
 715                     if count == 1:
 716                         msg = "1 minute"
 717
 718                     elif count in [5, 10, 15, 30]:
 719                         msg = "%d minutes" % count
 720
 721                     elif count == 60:
 722                         msg = "1 hour"
 723
 724                     elif count % 60 == 0:
 725                         msg = "%d hours" % (count // 60)
 726
 727                     if msg is not None:
 728                         print("%s waiting for solver (%s)" % (self.timestamp(), msg), flush=True)
 729
 730         if self.forall:
 731             result = self.read()
 732             while result not in ["sat", "unsat", "unknown", "timeout", "interrupted", ""]:
 733                 print("%s %s: %s" % (self.timestamp(), self.solver, result))
 734                 result = self.read()
 735         else:
 736             result = self.read()
 737
 738         if self.debug_file:
 739             print("(set-info :status %s)" % result, file=self.debug_file)
 740             print("(check-sat)", file=self.debug_file)
 741             self.debug_file.flush()
 742
 743         if result not in ["sat", "unsat", "unknown", "timeout", "interrupted"]:
 744             if result == "":
 745                 print("%s Unexpected EOF response from solver." % (self.timestamp()), flush=True)
 746             else:
 747                 print("%s Unexpected response from solver: %s" % (self.timestamp(), result), flush=True)
 748             if self.solver != "dummy":
 749                 self.p_close()
 750             sys.exit(1)
 751
 752         return result
 753
 754     def parse(self, stmt):
 755         def worker(stmt):
 756             if stmt[0] == '(':
 757                 expr = []
 758                 cursor = 1
 759                 while stmt[cursor] != ')':
 760                     el, le = worker(stmt[cursor:])
 761                     expr.append(el)
 762                     cursor += le
 763                 return expr, cursor+1
 764
 765             if stmt[0] == '|':
 766                 expr = "|"
 767                 cursor = 1
 768                 while stmt[cursor] != '|':
 769                     expr += stmt[cursor]
 770                     cursor += 1
 771                 expr += "|"
 772                 return expr, cursor+1
 773
 774             if stmt[0] in [" ", "\t", "\r", "\n"]:
 775                 el, le = worker(stmt[1:])
 776                 return el, le+1
 777
 778             expr = ""
 779             cursor = 0
 780             while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
 781                 expr += stmt[cursor]
 782                 cursor += 1
 783             return expr, cursor
 784         return worker(stmt)[0]
 785
 786     def unparse(self, stmt):
 787         if isinstance(stmt, list):
 788             return "(" + " ".join([self.unparse(s) for s in stmt]) + ")"
 789         return stmt
 790
 791     def bv2hex(self, v):
 792         h = ""
 793         v = self.bv2bin(v)
 794         while len(v) > 0:
 795             d = 0
 796             if len(v) > 0 and v[-1] == "1": d += 1
 797             if len(v) > 1 and v[-2] == "1": d += 2
 798             if len(v) > 2 and v[-3] == "1": d += 4
 799             if len(v) > 3 and v[-4] == "1": d += 8
 800             h = hex(d)[2:] + h
 801             if len(v) < 4: break
 802             v = v[:-4]
 803         return h
 804
 805     def bv2bin(self, v):
 806         if type(v) is list and len(v) == 3 and v[0] == "_" and v[1].startswith("bv"):
 807             x, n = int(v[1][2:]), int(v[2])
 808             return "".join("1" if (x & (1 << i)) else "0" for i in range(n-1, -1, -1))
 809         if v == "true": return "1"
 810         if v == "false": return "0"
 811         if v.startswith("#b"):
 812             return v[2:]
 813         if v.startswith("#x"):
 814             return "".join(hex_dict.get(x) for x in v[2:])
 815         assert False
 816
 817     def bv2int(self, v):
 818         return int(self.bv2bin(v), 2)
 819
 820     def get(self, expr):
 821         self.write("(get-value (%s))" % (expr))
 822         return self.parse(self.read())[0][1]
 823
 824     def get_list(self, expr_list):
 825         if len(expr_list) == 0:
 826             return []
 827         self.write("(get-value (%s))" % " ".join(expr_list))
 828         return [n[1] for n in self.parse(self.read())]
 829
 830     def get_path(self, mod, path):
 831         assert mod in self.modinfo
 832         path = path.replace("\\", "/").split(".")
 833
 834         for i in range(len(path)-1):
 835             first = ".".join(path[0:i+1])
 836             second = ".".join(path[i+1:])
 837
 838             if first in self.modinfo[mod].cells:
 839                 nextmod = self.modinfo[mod].cells[first]
 840                 return [first] + self.get_path(nextmod, second)
 841
 842         return [".".join(path)]
 843
 844     def net_expr(self, mod, base, path):
 845         if len(path) == 0:
 846             return base
 847
 848         if len(path) == 1:
 849             assert mod in self.modinfo
 850             if path[0] == "":
 851                 return base
 852             if path[0] in self.modinfo[mod].cells:
 853                 return "(|%s_h %s| %s)" % (mod, path[0], base)
 854             if path[0] in self.modinfo[mod].wsize:
 855                 return "(|%s_n %s| %s)" % (mod, path[0], base)
 856             if path[0] in self.modinfo[mod].memories:
 857                 return "(|%s_m %s| %s)" % (mod, path[0], base)
 858             assert 0
 859
 860         assert mod in self.modinfo
 861         assert path[0] in self.modinfo[mod].cells
 862
 863         nextmod = self.modinfo[mod].cells[path[0]]
 864         nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
 865         return self.net_expr(nextmod, nextbase, path[1:])
 866
 867     def net_width(self, mod, net_path):
 868         for i in range(len(net_path)-1):
 869             assert mod in self.modinfo
 870             assert net_path[i] in self.modinfo[mod].cells
 871             mod = self.modinfo[mod].cells[net_path[i]]
 872
 873         assert mod in self.modinfo
 874         assert net_path[-1] in self.modinfo[mod].wsize
 875         return self.modinfo[mod].wsize[net_path[-1]]
 876
 877     def net_clock(self, mod, net_path):
 878         for i in range(len(net_path)-1):
 879             assert mod in self.modinfo
 880             assert net_path[i] in self.modinfo[mod].cells
 881             mod = self.modinfo[mod].cells[net_path[i]]
 882
 883         assert mod in self.modinfo
 884         if net_path[-1] not in self.modinfo[mod].clocks:
 885             return None
 886         return self.modinfo[mod].clocks[net_path[-1]]
 887
 888     def net_exists(self, mod, net_path):
 889         for i in range(len(net_path)-1):
 890             if mod not in self.modinfo: return False
 891             if net_path[i] not in self.modinfo[mod].cells: return False
 892             mod = self.modinfo[mod].cells[net_path[i]]
 893
 894         if mod not in self.modinfo: return False
 895         if net_path[-1] not in self.modinfo[mod].wsize: return False
 896         return True
 897
 898     def mem_exists(self, mod, mem_path):
 899         for i in range(len(mem_path)-1):
 900             if mod not in self.modinfo: return False
 901             if mem_path[i] not in self.modinfo[mod].cells: return False
 902             mod = self.modinfo[mod].cells[mem_path[i]]
 903
 904         if mod not in self.modinfo: return False
 905         if mem_path[-1] not in self.modinfo[mod].memories: return False
 906         return True
 907
 908     def mem_expr(self, mod, base, path, port=None, infomode=False):
 909         if len(path) == 1:
 910             assert mod in self.modinfo
 911             assert path[0] in self.modinfo[mod].memories
 912             if infomode:
 913                 return self.modinfo[mod].memories[path[0]]
 914             return "(|%s_m%s %s| %s)" % (mod, "" if port is None else ":%s" % port, path[0], base)
 915
 916         assert mod in self.modinfo
 917         assert path[0] in self.modinfo[mod].cells
 918
 919         nextmod = self.modinfo[mod].cells[path[0]]
 920         nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
 921         return self.mem_expr(nextmod, nextbase, path[1:], port=port, infomode=infomode)
 922
 923     def mem_info(self, mod, path):
 924         return self.mem_expr(mod, "", path, infomode=True)
 925
 926     def get_net(self, mod_name, net_path, state_name):
 927         return self.get(self.net_expr(mod_name, state_name, net_path))
 928
 929     def get_net_list(self, mod_name, net_path_list, state_name):
 930         return self.get_list([self.net_expr(mod_name, state_name, n) for n in net_path_list])
 931
 932     def get_net_hex(self, mod_name, net_path, state_name):
 933         return self.bv2hex(self.get_net(mod_name, net_path, state_name))
 934
 935     def get_net_hex_list(self, mod_name, net_path_list, state_name):
 936         return [self.bv2hex(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]
 937
 938     def get_net_bin(self, mod_name, net_path, state_name):
 939         return self.bv2bin(self.get_net(mod_name, net_path, state_name))
 940
 941     def get_net_bin_list(self, mod_name, net_path_list, state_name):
 942         return [self.bv2bin(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]
 943
 944     def wait(self):
 945         if self.p is not None:
 946             self.p.wait()
 947             self.p_close()
 948
 949
 950 class SmtOpts:
 951     def __init__(self):
 952         self.shortopts = "s:S:v"
 953         self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
 954         self.solver = "yices"
 955         self.solver_opts = list()
 956         self.debug_print = False
 957         self.debug_file = None
 958         self.dummy_file = None
 959         self.unroll = False
 960         self.noincr = False
 961         self.timeinfo = os.name != "nt"
 962         self.timeout = 0
 963         self.logic = None
 964         self.info_stmts = list()
 965         self.nocomments = False
 966
 967     def handle(self, o, a):
 968         if o == "-s":
 969             self.solver = a
 970         elif o == "-S":
 971             self.solver_opts.append(a)
 972         elif o == "--timeout":
 973             self.timeout = int(a)
 974         elif o == "-v":
 975             self.debug_print = True
 976         elif o == "--unroll":
 977             self.unroll = True
 978         elif o == "--noincr":
 979             self.noincr = True
 980         elif o == "--noprogress":
 981             self.timeinfo = False
 982         elif o == "--dump-smt2":
 983             self.debug_file = open(a, "w")
 984         elif o == "--logic":
 985             self.logic = a
 986         elif o == "--dummy":
 987             self.dummy_file = a
 988         elif o == "--info":
 989             self.info_stmts.append(a)
 990         elif o == "--nocomments":
 991             self.nocomments = True
 992         else:
 993             return False
 994         return True
 995
 996     def helpmsg(self):
 997         return """
 998     -s <solver>
 999         set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy
1000         default: yices
1001
1002     -S <opt>
1003         pass <opt> as command line argument to the solver
1004
1005     --timeout <value>
1006         set the solver timeout to the specified value (in seconds).
1007
1008     --logic <smt2_logic>
1009         use the specified SMT2 logic (e.g. QF_AUFBV)
1010
1011     --dummy <filename>
1012         if solver is "dummy", read solver output from that file
1013         otherwise: write solver output to that file
1014
1015     -v
1016         enable debug output
1017
1018     --unroll
1019         unroll uninterpreted functions
1020
1021     --noincr
1022         don't use incremental solving, instead restart solver for
1023         each (check-sat). This also avoids (push) and (pop).
1024
1025     --noprogress
1026         disable timer display during solving
1027         (this option is set implicitly on Windows)
1028
1029     --dump-smt2 <filename>
1030         write smt2 statements to file
1031
1032     --info <smt2-info-stmt>
1033         include the specified smt2 info statement in the smt2 output
1034
1035     --nocomments
1036         strip all comments from the generated smt2 code
1037 """
1038
1039
1040 class MkVcd:
1041     def __init__(self, f):
1042         self.f = f
1043         self.t = -1
1044         self.nets = dict()
1045         self.clocks = dict()
1046
1047     def add_net(self, path, width):
1048         path = tuple(path)
1049         assert self.t == -1
1050         key = "n%d" % len(self.nets)
1051         self.nets[path] = (key, width)
1052
1053     def add_clock(self, path, edge):
1054         path = tuple(path)
1055         assert self.t == -1
1056         key = "n%d" % len(self.nets)
1057         self.nets[path] = (key, 1)
1058         self.clocks[path] = (key, edge)
1059
1060     def set_net(self, path, bits):
1061         path = tuple(path)
1062         assert self.t >= 0
1063         assert path in self.nets
1064         if path not in self.clocks:
1065             print("b%s %s" % (bits, self.nets[path][0]), file=self.f)
1066
1067     def escape_name(self, name):
1068         name = re.sub(r"\[([0-9a-zA-Z_]*[a-zA-Z_][0-9a-zA-Z_]*)\]", r"<\1>", name)
1069         if re.match("[\[\]]", name) and name[0] != "\\":
1070             name = "\\" + name
1071         return name
1072
1073     def set_time(self, t):
1074         assert t >= self.t
1075         if t != self.t:
1076             if self.t == -1:
1077                 print("$version Generated by Yosys-SMTBMC $end", file=self.f)
1078                 print("$timescale 1ns $end", file=self.f)
1079                 print("$var integer 32 t smt_step $end", file=self.f)
1080                 print("$var event 1 ! smt_clock $end", file=self.f)
1081
1082                 def vcdescape(n):
1083                     if n.startswith("$") or ":" in n:
1084                         return "\\" + n
1085                     return n
1086
1087                 scope = []
1088                 for path in sorted(self.nets):
1089                     key, width = self.nets[path]
1090
1091                     uipath = list(path)
1092                     if "." in uipath[-1] and not uipath[-1].startswith("$"):
1093                         uipath = uipath[0:-1] + uipath[-1].split(".")
1094                     for i in range(len(uipath)):
1095                         uipath[i] = re.sub(r"\[([^\]]*)\]", r"<\1>", uipath[i])
1096
1097                     while uipath[:len(scope)] != scope:
1098                         print("$upscope $end", file=self.f)
1099                         scope = scope[:-1]
1100
1101                     while uipath[:-1] != scope:
1102                         scopename = uipath[len(scope)]
1103                         print("$scope module %s $end" % vcdescape(scopename), file=self.f)
1104                         scope.append(uipath[len(scope)])
1105
1106                     if path in self.clocks and self.clocks[path][1] == "event":
1107                         print("$var event 1 %s %s $end" % (key, vcdescape(uipath[-1])), file=self.f)
1108                     else:
1109                         print("$var wire %d %s %s $end" % (width, key, vcdescape(uipath[-1])), file=self.f)
1110
1111                 for i in range(len(scope)):
1112                     print("$upscope $end", file=self.f)
1113
1114                 print("$enddefinitions $end", file=self.f)
1115
1116             self.t = t
1117             assert self.t >= 0
1118
1119             if self.t > 0:
1120                 print("#%d" % (10 * self.t - 5), file=self.f)
1121                 for path in sorted(self.clocks.keys()):
1122                     if self.clocks[path][1] == "posedge":
1123                         print("b0 %s" % self.nets[path][0], file=self.f)
1124                     elif self.clocks[path][1] == "negedge":
1125                         print("b1 %s" % self.nets[path][0], file=self.f)
1126
1127             print("#%d" % (10 * self.t), file=self.f)
1128             print("1!", file=self.f)
1129             print("b%s t" % format(self.t, "032b"), file=self.f)
1130
1131             for path in sorted(self.clocks.keys()):
1132                 if self.clocks[path][1] == "negedge":
1133                     print("b0 %s" % self.nets[path][0], file=self.f)
1134                 else:
1135                     print("b1 %s" % self.nets[path][0], file=self.f)