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