backends/smt2/smtio.py

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