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