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