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, subprocess, re, os
  20 from copy import deepcopy
  21 from select import select
  22 from time import time
  23
  24
  25 hex_dict = {
  26     "0": "0000", "1": "0001", "2": "0010", "3": "0011",
  27     "4": "0100", "5": "0101", "6": "0110", "7": "0111",
  28     "8": "1000", "9": "1001", "A": "1010", "B": "1011",
  29     "C": "1100", "D": "1101", "E": "1110", "F": "1111",
  30     "a": "1010", "b": "1011", "c": "1100", "d": "1101",
  31     "e": "1110", "f": "1111"
  32 }
  33
  34
  35 class SmtModInfo:
  36     def __init__(self):
  37         self.inputs = set()
  38         self.outputs = set()
  39         self.registers = set()
  40         self.memories = dict()
  41         self.wires = set()
  42         self.wsize = dict()
  43         self.cells = dict()
  44         self.asserts = dict()
  45         self.covers = dict()
  46         self.anyconsts = dict()
  47         self.anyseqs = dict()
  48
  49
  50 class SmtIo:
  51     def __init__(self, opts=None):
  52         self.logic = None
  53         self.logic_qf = True
  54         self.logic_ax = True
  55         self.logic_uf = True
  56         self.logic_bv = True
  57         self.logic_dt = False
  58         self.produce_models = True
  59         self.smt2cache = [list()]
  60         self.p = None
  61         self.p_buffer = []
  62
  63         if opts is not None:
  64             self.logic = opts.logic
  65             self.solver = opts.solver
  66             self.solver_opts = opts.solver_opts
  67             self.debug_print = opts.debug_print
  68             self.debug_file = opts.debug_file
  69             self.dummy_file = opts.dummy_file
  70             self.timeinfo = opts.timeinfo
  71             self.unroll = opts.unroll
  72             self.noincr = opts.noincr
  73             self.info_stmts = opts.info_stmts
  74             self.nocomments = opts.nocomments
  75
  76         else:
  77             self.solver = "yices"
  78             self.solver_opts = list()
  79             self.debug_print = False
  80             self.debug_file = None
  81             self.dummy_file = None
  82             self.timeinfo = os.name != "nt"
  83             self.unroll = False
  84             self.noincr = False
  85             self.info_stmts = list()
  86             self.nocomments = False
  87
  88         self.start_time = time()
  89
  90         self.modinfo = dict()
  91         self.curmod = None
  92         self.topmod = None
  93         self.setup_done = False
  94
  95     def setup(self):
  96         assert not self.setup_done
  97
  98         if self.solver == "yices":
  99             self.popen_vargs = ['yices-smt2', '--incremental'] + self.solver_opts
 100
 101         if self.solver == "z3":
 102             self.popen_vargs = ['z3', '-smt2', '-in'] + self.solver_opts
 103
 104         if self.solver == "cvc4":
 105             self.popen_vargs = ['cvc4', '--incremental', '--lang', 'smt2.6' if self.logic_dt else 'smt2'] + self.solver_opts
 106
 107         if self.solver == "mathsat":
 108             self.popen_vargs = ['mathsat'] + self.solver_opts
 109
 110         if self.solver == "boolector":
 111             self.popen_vargs = ['boolector', '--smt2', '-i'] + self.solver_opts
 112             self.unroll = True
 113
 114         if self.solver == "abc":
 115             if len(self.solver_opts) > 0:
 116                 self.popen_vargs = ['yosys-abc', '-S', '; '.join(self.solver_opts)]
 117             else:
 118                 self.popen_vargs = ['yosys-abc', '-S', '%blast; &sweep -C 5000; &syn4; &cec -s -m -C 2000']
 119             self.logic_ax = False
 120             self.unroll = True
 121             self.noincr = True
 122
 123         if self.solver == "dummy":
 124             assert self.dummy_file is not None
 125             self.dummy_fd = open(self.dummy_file, "r")
 126         else:
 127             if self.dummy_file is not None:
 128                 self.dummy_fd = open(self.dummy_file, "w")
 129             if not self.noincr:
 130                 self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
 131
 132         if self.unroll:
 133             self.logic_uf = False
 134             self.unroll_idcnt = 0
 135             self.unroll_buffer = ""
 136             self.unroll_sorts = set()
 137             self.unroll_objs = set()
 138             self.unroll_decls = dict()
 139             self.unroll_cache = dict()
 140             self.unroll_stack = list()
 141
 142         if self.logic is None:
 143             self.logic = ""
 144             if self.logic_qf: self.logic += "QF_"
 145             if self.logic_ax: self.logic += "A"
 146             if self.logic_uf: self.logic += "UF"
 147             if self.logic_bv: self.logic += "BV"
 148             if self.logic_dt: self.logic = "ALL"
 149
 150         self.setup_done = True
 151
 152         if self.produce_models:
 153             self.write("(set-option :produce-models true)")
 154
 155         self.write("(set-logic %s)" % self.logic)
 156
 157         for stmt in self.info_stmts:
 158             self.write(stmt)
 159
 160     def timestamp(self):
 161         secs = int(time() - self.start_time)
 162         return "## %6d %3d:%02d:%02d " % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
 163
 164     def replace_in_stmt(self, stmt, pat, repl):
 165         if stmt == pat:
 166             return repl
 167
 168         if isinstance(stmt, list):
 169             return [self.replace_in_stmt(s, pat, repl) for s in stmt]
 170
 171         return stmt
 172
 173     def unroll_stmt(self, stmt):
 174         if not isinstance(stmt, list):
 175             return stmt
 176
 177         stmt = [self.unroll_stmt(s) for s in stmt]
 178
 179         if len(stmt) >= 2 and not isinstance(stmt[0], list) and stmt[0] in self.unroll_decls:
 180             assert stmt[1] in self.unroll_objs
 181
 182             key = tuple(stmt)
 183             if key not in self.unroll_cache:
 184                 decl = deepcopy(self.unroll_decls[key[0]])
 185
 186                 self.unroll_cache[key] = "|UNROLL#%d|" % self.unroll_idcnt
 187                 decl[1] = self.unroll_cache[key]
 188                 self.unroll_idcnt += 1
 189
 190                 if decl[0] == "declare-fun":
 191                     if isinstance(decl[3], list) or decl[3] not in self.unroll_sorts:
 192                         self.unroll_objs.add(decl[1])
 193                         decl[2] = list()
 194                     else:
 195                         self.unroll_objs.add(decl[1])
 196                         decl = list()
 197
 198                 elif decl[0] == "define-fun":
 199                     arg_index = 1
 200                     for arg_name, arg_sort in decl[2]:
 201                         decl[4] = self.replace_in_stmt(decl[4], arg_name, key[arg_index])
 202                         arg_index += 1
 203                     decl[2] = list()
 204
 205                 if len(decl) > 0:
 206                     decl = self.unroll_stmt(decl)
 207                     self.write(self.unparse(decl), unroll=False)
 208
 209             return self.unroll_cache[key]
 210
 211         return stmt
 212
 213     def p_write(self, data):
 214         # select_result = select([self.p.stdout], [self.p.stdin], [], 0.1):
 215         wlen = self.p.stdin.write(data)
 216         assert wlen == len(data)
 217
 218     def p_flush(self):
 219         self.p.stdin.flush()
 220
 221     def p_read(self):
 222         if len(self.p_buffer) == 0:
 223             return self.p.stdout.readline().decode("ascii")
 224         assert 0
 225
 226     def write(self, stmt, unroll=True):
 227         if stmt.startswith(";"):
 228             self.info(stmt)
 229             if not self.setup_done:
 230                 self.info_stmts.append(stmt)
 231                 return
 232         elif not self.setup_done:
 233             self.setup()
 234
 235         stmt = stmt.strip()
 236
 237         if self.nocomments or self.unroll:
 238             stmt = re.sub(r" *;.*", "", stmt)
 239             if stmt == "": return
 240
 241         if unroll and self.unroll:
 242             stmt = self.unroll_buffer + stmt
 243             self.unroll_buffer = ""
 244
 245             s = re.sub(r"\|[^|]*\|", "", stmt)
 246             if s.count("(") != s.count(")"):
 247                 self.unroll_buffer = stmt + " "
 248                 return
 249
 250             s = self.parse(stmt)
 251
 252             if self.debug_print:
 253                 print("-> %s" % s)
 254
 255             if len(s) == 3 and s[0] == "declare-sort" and s[2] == "0":
 256                 self.unroll_sorts.add(s[1])
 257                 return
 258
 259             elif len(s) == 4 and s[0] == "declare-fun" and s[2] == [] and s[3] in self.unroll_sorts:
 260                 self.unroll_objs.add(s[1])
 261                 return
 262
 263             elif len(s) >= 4 and s[0] == "declare-fun":
 264                 for arg_sort in s[2]:
 265                     if arg_sort in self.unroll_sorts:
 266                         self.unroll_decls[s[1]] = s
 267                         return
 268
 269             elif len(s) >= 4 and s[0] == "define-fun":
 270                 for arg_name, arg_sort in s[2]:
 271                     if arg_sort in self.unroll_sorts:
 272                         self.unroll_decls[s[1]] = s
 273                         return
 274
 275             stmt = self.unparse(self.unroll_stmt(s))
 276
 277             if stmt == "(push 1)":
 278                 self.unroll_stack.append((
 279                     deepcopy(self.unroll_sorts),
 280                     deepcopy(self.unroll_objs),
 281                     deepcopy(self.unroll_decls),
 282                     deepcopy(self.unroll_cache),
 283                 ))
 284
 285             if stmt == "(pop 1)":
 286                 self.unroll_sorts, self.unroll_objs, self.unroll_decls, self.unroll_cache = self.unroll_stack.pop()
 287
 288         if self.debug_print:
 289             print("> %s" % stmt)
 290
 291         if self.debug_file:
 292             print(stmt, file=self.debug_file)
 293             self.debug_file.flush()
 294
 295         if self.solver != "dummy":
 296             if self.noincr:
 297                 if self.p is not None and not stmt.startswith("(get-"):
 298                     self.p.stdin.close()
 299                     self.p = None
 300                     self.p_buffer = []
 301                 if stmt == "(push 1)":
 302                     self.smt2cache.append(list())
 303                 elif stmt == "(pop 1)":
 304                     self.smt2cache.pop()
 305                 else:
 306                     if self.p is not None:
 307                         self.p_write(bytes(stmt + "\n", "ascii"))
 308                         self.p_flush()
 309                     self.smt2cache[-1].append(stmt)
 310             else:
 311                 self.p_write(bytes(stmt + "\n", "ascii"))
 312                 self.p_flush()
 313
 314     def info(self, stmt):
 315         if not stmt.startswith("; yosys-smt2-"):
 316             return
 317
 318         fields = stmt.split()
 319
 320         if fields[1] == "yosys-smt2-nomem":
 321             if self.logic is None:
 322                 self.logic_ax = False
 323
 324         if fields[1] == "yosys-smt2-nobv":
 325             if self.logic is None:
 326                 self.logic_bv = False
 327
 328         if fields[1] == "yosys-smt2-stdt":
 329             if self.logic is None:
 330                 self.logic_dt = True
 331
 332         if fields[1] == "yosys-smt2-module":
 333             self.curmod = fields[2]
 334             self.modinfo[self.curmod] = SmtModInfo()
 335
 336         if fields[1] == "yosys-smt2-cell":
 337             self.modinfo[self.curmod].cells[fields[3]] = fields[2]
 338
 339         if fields[1] == "yosys-smt2-topmod":
 340             self.topmod = fields[2]
 341
 342         if fields[1] == "yosys-smt2-input":
 343             self.modinfo[self.curmod].inputs.add(fields[2])
 344             self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
 345
 346         if fields[1] == "yosys-smt2-output":
 347             self.modinfo[self.curmod].outputs.add(fields[2])
 348             self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
 349
 350         if fields[1] == "yosys-smt2-register":
 351             self.modinfo[self.curmod].registers.add(fields[2])
 352             self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
 353
 354         if fields[1] == "yosys-smt2-memory":
 355             self.modinfo[self.curmod].memories[fields[2]] = (int(fields[3]), int(fields[4]), int(fields[5]), int(fields[6]))
 356
 357         if fields[1] == "yosys-smt2-wire":
 358             self.modinfo[self.curmod].wires.add(fields[2])
 359             self.modinfo[self.curmod].wsize[fields[2]] = int(fields[3])
 360
 361         if fields[1] == "yosys-smt2-assert":
 362             self.modinfo[self.curmod].asserts["%s_a %s" % (self.curmod, fields[2])] = fields[3]
 363
 364         if fields[1] == "yosys-smt2-cover":
 365             self.modinfo[self.curmod].covers["%s_c %s" % (self.curmod, fields[2])] = fields[3]
 366
 367         if fields[1] == "yosys-smt2-anyconst":
 368             self.modinfo[self.curmod].anyconsts[fields[2]] = (fields[3], None if len(fields) <= 4 else fields[4])
 369
 370         if fields[1] == "yosys-smt2-anyseq":
 371             self.modinfo[self.curmod].anyseqs[fields[2]] = (fields[3], None if len(fields) <= 4 else fields[4])
 372
 373     def hiernets(self, top, regs_only=False):
 374         def hiernets_worker(nets, mod, cursor):
 375             for netname in sorted(self.modinfo[mod].wsize.keys()):
 376                 if not regs_only or netname in self.modinfo[mod].registers:
 377                     nets.append(cursor + [netname])
 378             for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
 379                 hiernets_worker(nets, celltype, cursor + [cellname])
 380
 381         nets = list()
 382         hiernets_worker(nets, top, [])
 383         return nets
 384
 385     def hieranyconsts(self, top):
 386         def worker(results, mod, cursor):
 387             for name, value in sorted(self.modinfo[mod].anyconsts.items()):
 388                 results.append((cursor, name, value[0], value[1]))
 389             for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
 390                 worker(results, celltype, cursor + [cellname])
 391
 392         results = list()
 393         worker(results, top, [])
 394         return results
 395
 396     def hieranyseqs(self, top):
 397         def worker(results, mod, cursor):
 398             for name, value in sorted(self.modinfo[mod].anyseqs.items()):
 399                 results.append((cursor, name, value[0], value[1]))
 400             for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
 401                 worker(results, celltype, cursor + [cellname])
 402
 403         results = list()
 404         worker(results, top, [])
 405         return results
 406
 407     def hiermems(self, top):
 408         def hiermems_worker(mems, mod, cursor):
 409             for memname in sorted(self.modinfo[mod].memories.keys()):
 410                 mems.append(cursor + [memname])
 411             for cellname, celltype in sorted(self.modinfo[mod].cells.items()):
 412                 hiermems_worker(mems, celltype, cursor + [cellname])
 413
 414         mems = list()
 415         hiermems_worker(mems, top, [])
 416         return mems
 417
 418     def read(self):
 419         stmt = []
 420         count_brackets = 0
 421
 422         while True:
 423             if self.solver == "dummy":
 424                 line = self.dummy_fd.readline().strip()
 425             else:
 426                 line = self.p_read().strip()
 427                 if self.dummy_file is not None:
 428                     self.dummy_fd.write(line + "\n")
 429
 430             count_brackets += line.count("(")
 431             count_brackets -= line.count(")")
 432             stmt.append(line)
 433
 434             if self.debug_print:
 435                 print("< %s" % line)
 436             if count_brackets == 0:
 437                 break
 438             if self.solver != "dummy" and self.p.poll():
 439                 print("SMT Solver terminated unexpectedly: %s" % "".join(stmt))
 440                 sys.exit(1)
 441
 442         stmt = "".join(stmt)
 443         if stmt.startswith("(error"):
 444             print("SMT Solver Error: %s" % stmt, file=sys.stderr)
 445             sys.exit(1)
 446
 447         return stmt
 448
 449     def check_sat(self):
 450         if self.debug_print:
 451             print("> (check-sat)")
 452         if self.debug_file and not self.nocomments:
 453             print("; running check-sat..", file=self.debug_file)
 454             self.debug_file.flush()
 455
 456         if self.solver != "dummy":
 457             if self.noincr:
 458                 if self.p is not None:
 459                     self.p.stdin.close()
 460                     self.p = None
 461                     self.p_buffer = []
 462                 self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
 463                 for cache_ctx in self.smt2cache:
 464                     for cache_stmt in cache_ctx:
 465                         self.p_write(bytes(cache_stmt + "\n", "ascii"))
 466
 467             self.p_write(bytes("(check-sat)\n", "ascii"))
 468             self.p_flush()
 469
 470             if self.timeinfo:
 471                 i = 0
 472                 s = "/-\|"
 473
 474                 count = 0
 475                 num_bs = 0
 476                 while select([self.p.stdout], [], [], 0.1) == ([], [], []):
 477                     count += 1
 478
 479                     if count < 25:
 480                         continue
 481
 482                     if count % 10 == 0 or count == 25:
 483                         secs = count // 10
 484
 485                         if secs < 60:
 486                             m = "(%d seconds)" % secs
 487                         elif secs < 60*60:
 488                             m = "(%d seconds -- %d:%02d)" % (secs, secs // 60, secs % 60)
 489                         else:
 490                             m = "(%d seconds -- %d:%02d:%02d)" % (secs, secs // (60*60), (secs // 60) % 60, secs % 60)
 491
 492                         print("%s %s %c" % ("\b \b" * num_bs, m, s[i]), end="", file=sys.stderr)
 493                         num_bs = len(m) + 3
 494
 495                     else:
 496                         print("\b" + s[i], end="", file=sys.stderr)
 497
 498                     sys.stderr.flush()
 499                     i = (i + 1) % len(s)
 500
 501                 if num_bs != 0:
 502                     print("\b \b" * num_bs, end="", file=sys.stderr)
 503                     sys.stderr.flush()
 504
 505         result = self.read()
 506         if self.debug_file:
 507             print("(set-info :status %s)" % result, file=self.debug_file)
 508             print("(check-sat)", file=self.debug_file)
 509             self.debug_file.flush()
 510         return result
 511
 512     def parse(self, stmt):
 513         def worker(stmt):
 514             if stmt[0] == '(':
 515                 expr = []
 516                 cursor = 1
 517                 while stmt[cursor] != ')':
 518                     el, le = worker(stmt[cursor:])
 519                     expr.append(el)
 520                     cursor += le
 521                 return expr, cursor+1
 522
 523             if stmt[0] == '|':
 524                 expr = "|"
 525                 cursor = 1
 526                 while stmt[cursor] != '|':
 527                     expr += stmt[cursor]
 528                     cursor += 1
 529                 expr += "|"
 530                 return expr, cursor+1
 531
 532             if stmt[0] in [" ", "\t", "\r", "\n"]:
 533                 el, le = worker(stmt[1:])
 534                 return el, le+1
 535
 536             expr = ""
 537             cursor = 0
 538             while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]:
 539                 expr += stmt[cursor]
 540                 cursor += 1
 541             return expr, cursor
 542         return worker(stmt)[0]
 543
 544     def unparse(self, stmt):
 545         if isinstance(stmt, list):
 546             return "(" + " ".join([self.unparse(s) for s in stmt]) + ")"
 547         return stmt
 548
 549     def bv2hex(self, v):
 550         h = ""
 551         v = self.bv2bin(v)
 552         while len(v) > 0:
 553             d = 0
 554             if len(v) > 0 and v[-1] == "1": d += 1
 555             if len(v) > 1 and v[-2] == "1": d += 2
 556             if len(v) > 2 and v[-3] == "1": d += 4
 557             if len(v) > 3 and v[-4] == "1": d += 8
 558             h = hex(d)[2:] + h
 559             if len(v) < 4: break
 560             v = v[:-4]
 561         return h
 562
 563     def bv2bin(self, v):
 564         if v == "true": return "1"
 565         if v == "false": return "0"
 566         if v.startswith("#b"):
 567             return v[2:]
 568         if v.startswith("#x"):
 569             return "".join(hex_dict.get(x) for x in v[2:])
 570         assert False
 571
 572     def bv2int(self, v):
 573         return int(self.bv2bin(v), 2)
 574
 575     def get(self, expr):
 576         self.write("(get-value (%s))" % (expr))
 577         return self.parse(self.read())[0][1]
 578
 579     def get_list(self, expr_list):
 580         if len(expr_list) == 0:
 581             return []
 582         self.write("(get-value (%s))" % " ".join(expr_list))
 583         return [n[1] for n in self.parse(self.read())]
 584
 585     def get_path(self, mod, path):
 586         assert mod in self.modinfo
 587         path = path.split(".")
 588
 589         for i in range(len(path)-1):
 590             first = ".".join(path[0:i+1])
 591             second = ".".join(path[i+1:])
 592
 593             if first in self.modinfo[mod].cells:
 594                 nextmod = self.modinfo[mod].cells[first]
 595                 return [first] + self.get_path(nextmod, second)
 596
 597         return [".".join(path)]
 598
 599     def net_expr(self, mod, base, path):
 600         if len(path) == 0:
 601             return base
 602
 603         if len(path) == 1:
 604             assert mod in self.modinfo
 605             if path[0] == "":
 606                 return base
 607             if path[0] in self.modinfo[mod].cells:
 608                 return "(|%s_h %s| %s)" % (mod, path[0], base)
 609             if path[0] in self.modinfo[mod].wsize:
 610                 return "(|%s_n %s| %s)" % (mod, path[0], base)
 611             if path[0] in self.modinfo[mod].memories:
 612                 return "(|%s_m %s| %s)" % (mod, path[0], base)
 613             assert 0
 614
 615         assert mod in self.modinfo
 616         assert path[0] in self.modinfo[mod].cells
 617
 618         nextmod = self.modinfo[mod].cells[path[0]]
 619         nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
 620         return self.net_expr(nextmod, nextbase, path[1:])
 621
 622     def net_width(self, mod, net_path):
 623         for i in range(len(net_path)-1):
 624             assert mod in self.modinfo
 625             assert net_path[i] in self.modinfo[mod].cells
 626             mod = self.modinfo[mod].cells[net_path[i]]
 627
 628         assert mod in self.modinfo
 629         assert net_path[-1] in self.modinfo[mod].wsize
 630         return self.modinfo[mod].wsize[net_path[-1]]
 631
 632     def net_exists(self, mod, net_path):
 633         for i in range(len(net_path)-1):
 634             if mod not in self.modinfo: return False
 635             if net_path[i] not in self.modinfo[mod].cells: return False
 636             mod = self.modinfo[mod].cells[net_path[i]]
 637
 638         if mod not in self.modinfo: return False
 639         if net_path[-1] not in self.modinfo[mod].wsize: return False
 640         return True
 641
 642     def mem_exists(self, mod, mem_path):
 643         for i in range(len(mem_path)-1):
 644             if mod not in self.modinfo: return False
 645             if mem_path[i] not in self.modinfo[mod].cells: return False
 646             mod = self.modinfo[mod].cells[mem_path[i]]
 647
 648         if mod not in self.modinfo: return False
 649         if mem_path[-1] not in self.modinfo[mod].memories: return False
 650         return True
 651
 652     def mem_expr(self, mod, base, path, port=None, infomode=False):
 653         if len(path) == 1:
 654             assert mod in self.modinfo
 655             assert path[0] in self.modinfo[mod].memories
 656             if infomode:
 657                 return self.modinfo[mod].memories[path[0]]
 658             return "(|%s_m%s %s| %s)" % (mod, "" if port is None else ":%s" % port, path[0], base)
 659
 660         assert mod in self.modinfo
 661         assert path[0] in self.modinfo[mod].cells
 662
 663         nextmod = self.modinfo[mod].cells[path[0]]
 664         nextbase = "(|%s_h %s| %s)" % (mod, path[0], base)
 665         return self.mem_expr(nextmod, nextbase, path[1:], port=port, infomode=infomode)
 666
 667     def mem_info(self, mod, path):
 668         return self.mem_expr(mod, "", path, infomode=True)
 669
 670     def get_net(self, mod_name, net_path, state_name):
 671         return self.get(self.net_expr(mod_name, state_name, net_path))
 672
 673     def get_net_list(self, mod_name, net_path_list, state_name):
 674         return self.get_list([self.net_expr(mod_name, state_name, n) for n in net_path_list])
 675
 676     def get_net_hex(self, mod_name, net_path, state_name):
 677         return self.bv2hex(self.get_net(mod_name, net_path, state_name))
 678
 679     def get_net_hex_list(self, mod_name, net_path_list, state_name):
 680         return [self.bv2hex(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]
 681
 682     def get_net_bin(self, mod_name, net_path, state_name):
 683         return self.bv2bin(self.get_net(mod_name, net_path, state_name))
 684
 685     def get_net_bin_list(self, mod_name, net_path_list, state_name):
 686         return [self.bv2bin(v) for v in self.get_net_list(mod_name, net_path_list, state_name)]
 687
 688     def wait(self):
 689         if self.p is not None:
 690             self.p.wait()
 691
 692
 693 class SmtOpts:
 694     def __init__(self):
 695         self.shortopts = "s:S:v"
 696         self.longopts = ["unroll", "noincr", "noprogress", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
 697         self.solver = "yices"
 698         self.solver_opts = list()
 699         self.debug_print = False
 700         self.debug_file = None
 701         self.dummy_file = None
 702         self.unroll = False
 703         self.noincr = False
 704         self.timeinfo = os.name != "nt"
 705         self.logic = None
 706         self.info_stmts = list()
 707         self.nocomments = False
 708
 709     def handle(self, o, a):
 710         if o == "-s":
 711             self.solver = a
 712         elif o == "-S":
 713             self.solver_opts.append(a)
 714         elif o == "-v":
 715             self.debug_print = True
 716         elif o == "--unroll":
 717             self.unroll = True
 718         elif o == "--noincr":
 719             self.noincr = True
 720         elif o == "--noprogress":
 721             self.timeinfo = False
 722         elif o == "--dump-smt2":
 723             self.debug_file = open(a, "w")
 724         elif o == "--logic":
 725             self.logic = a
 726         elif o == "--dummy":
 727             self.dummy_file = a
 728         elif o == "--info":
 729             self.info_stmts.append(a)
 730         elif o == "--nocomments":
 731             self.nocomments = True
 732         else:
 733             return False
 734         return True
 735
 736     def helpmsg(self):
 737         return """
 738     -s <solver>
 739         set SMT solver: z3, yices, boolector, cvc4, mathsat, dummy
 740         default: yices
 741
 742     -S <opt>
 743         pass <opt> as command line argument to the solver
 744
 745     --logic <smt2_logic>
 746         use the specified SMT2 logic (e.g. QF_AUFBV)
 747
 748     --dummy <filename>
 749         if solver is "dummy", read solver output from that file
 750         otherwise: write solver output to that file
 751
 752     -v
 753         enable debug output
 754
 755     --unroll
 756         unroll uninterpreted functions
 757
 758     --noincr
 759         don't use incremental solving, instead restart solver for
 760         each (check-sat). This also avoids (push) and (pop).
 761
 762     --noprogress
 763         disable timer display during solving
 764         (this option is set implicitly on Windows)
 765
 766     --dump-smt2 <filename>
 767         write smt2 statements to file
 768
 769     --info <smt2-info-stmt>
 770         include the specified smt2 info statement in the smt2 output
 771
 772     --nocomments
 773         strip all comments from the generated smt2 code
 774 """
 775
 776
 777 class MkVcd:
 778     def __init__(self, f):
 779         self.f = f
 780         self.t = -1
 781         self.nets = dict()
 782
 783     def add_net(self, path, width):
 784         path = tuple(path)
 785         assert self.t == -1
 786         key = "n%d" % len(self.nets)
 787         self.nets[path] = (key, width)
 788
 789     def set_net(self, path, bits):
 790         path = tuple(path)
 791         assert self.t >= 0
 792         assert path in self.nets
 793         print("b%s %s" % (bits, self.nets[path][0]), file=self.f)
 794
 795     def set_time(self, t):
 796         assert t >= self.t
 797         if t != self.t:
 798             if self.t == -1:
 799                 print("$var integer 32 t smt_step $end", file=self.f)
 800                 print("$var event 1 ! smt_clock $end", file=self.f)
 801                 scope = []
 802                 for path in sorted(self.nets):
 803                     while len(scope)+1 > len(path) or (len(scope) > 0 and scope[-1] != path[len(scope)-1]):
 804                         print("$upscope $end", file=self.f)
 805                         scope = scope[:-1]
 806                     while len(scope)+1 < len(path):
 807                         print("$scope module %s $end" % path[len(scope)], file=self.f)
 808                         scope.append(path[len(scope)-1])
 809                     key, width = self.nets[path]
 810                     print("$var wire %d %s %s $end" % (width, key, path[-1]), file=self.f)
 811                 for i in range(len(scope)):
 812                     print("$upscope $end", file=self.f)
 813                 print("$enddefinitions $end", file=self.f)
 814             self.t = t
 815             assert self.t >= 0
 816             print("#%d" % (10 * self.t), file=self.f)
 817             print("1!", file=self.f)
 818             print("b%s t" % format(self.t, "032b"), file=self.f)
 819