backends/smt2/smtbmc.py

   1 #!/usr/bin/env python3
   2 #
   3 # yosys -- Yosys Open SYnthesis Suite
   4 #
   5 # Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
   6 #
   7 # Permission to use, copy, modify, and/or distribute this software for any
   8 # purpose with or without fee is hereby granted, provided that the above
   9 # copyright notice and this permission notice appear in all copies.
  10 #
  11 # THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  12 # WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  13 # MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  14 # ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  15 # WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  16 # ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  17 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  18 #
  19
  20 import os, sys, getopt, re
  21 ##yosys-sys-path##
  22 from smtio import SmtIo, SmtOpts, MkVcd
  23 from collections import defaultdict
  24
  25 got_topt = False
  26 skip_steps = 0
  27 step_size = 1
  28 num_steps = 20
  29 append_steps = 0
  30 vcdfile = None
  31 cexfile = None
  32 aimfile = None
  33 aiwfile = None
  34 aigheader = True
  35 vlogtbfile = None
  36 vlogtbtop = None
  37 inconstr = list()
  38 outconstr = None
  39 gentrace = False
  40 covermode = False
  41 tempind = False
  42 dumpall = False
  43 assume_skipped = None
  44 final_only = False
  45 topmod = None
  46 noinfo = False
  47 presat = False
  48 smtcinit = False
  49 smtctop = None
  50 noinit = False
  51 so = SmtOpts()
  52
  53
  54 def usage():
  55     print("""
  56 yosys-smtbmc [options] <yosys_smt2_output>
  57
  58     -t <num_steps>
  59     -t <skip_steps>:<num_steps>
  60     -t <skip_steps>:<step_size>:<num_steps>
  61         default: skip_steps=0, step_size=1, num_steps=20
  62
  63     -g
  64         generate an arbitrary trace that satisfies
  65         all assertions and assumptions.
  66
  67     -i
  68         instead of BMC run temporal induction
  69
  70     -c
  71         instead of regular BMC run cover analysis
  72
  73     -m <module_name>
  74         name of the top module
  75
  76     --smtc <constr_filename>
  77         read constraints file
  78
  79     --cex <cex_filename>
  80         read cex file as written by ABC's "write_cex -n"
  81
  82     --aig <prefix>
  83         read AIGER map file (as written by Yosys' "write_aiger -map")
  84         and AIGER witness file. The file names are <prefix>.aim for
  85         the map file and <prefix>.aiw for the witness file.
  86
  87     --aig <aim_filename>:<aiw_filename>
  88         like above, but for map files and witness files that do not
  89         share a filename prefix (or use differen file extensions).
  90
  91     --aig-noheader
  92         the AIGER witness file does not include the status and
  93         properties lines.
  94
  95     --noinfo
  96         only run the core proof, do not collect and print any
  97         additional information (e.g. which assert failed)
  98
  99     --presat
 100         check if the design with assumptions but without assertions
 101         is SAT before checking if assertions are UNSAT. This will
 102         detect if there are contradicting assumtions. In some cases
 103         this will also help to "warmup" the solver, potentially
 104         yielding a speedup.
 105
 106     --final-only
 107         only check final constraints, assume base case
 108
 109     --assume-skipped <start_step>
 110         assume asserts in skipped steps in BMC.
 111         no assumptions are created for skipped steps
 112         before <start_step>.
 113
 114     --dump-vcd <vcd_filename>
 115         write trace to this VCD file
 116         (hint: use 'write_smt2 -wires' for maximum
 117         coverage of signals in generated VCD file)
 118
 119     --dump-vlogtb <verilog_filename>
 120         write trace as Verilog test bench
 121
 122     --vlogtb-top <hierarchical_name>
 123         use the given entity as top module for the generated
 124         Verilog test bench. The <hierarchical_name> is relative
 125         to the design top module without the top module name.
 126
 127     --dump-smtc <constr_filename>
 128         write trace as constraints file
 129
 130     --smtc-init
 131         write just the last state as initial constraint to smtc file
 132
 133     --smtc-top <old>[:<new>]
 134         replace <old> with <new> in constraints dumped to smtc
 135         file and only dump object below <old> in design hierarchy.
 136
 137     --noinit
 138         do not assume initial conditions in state 0
 139
 140     --dump-all
 141         when using -g or -i, create a dump file for each
 142         step. The character '%' is replaces in all dump
 143         filenames with the step number.
 144
 145     --append <num_steps>
 146         add <num_steps> time steps at the end of the trace
 147         when creating a counter example (this additional time
 148         steps will still be constrained by assumtions)
 149 """ + so.helpmsg())
 150     sys.exit(1)
 151
 152
 153 try:
 154     opts, args = getopt.getopt(sys.argv[1:], so.shortopts + "t:igcm:", so.longopts +
 155             ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "presat",
 156              "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
 157              "smtc-init", "smtc-top=", "noinit"])
 158 except:
 159     usage()
 160
 161 for o, a in opts:
 162     if o == "-t":
 163         got_topt = True
 164         a = a.split(":")
 165         if len(a) == 1:
 166             num_steps = int(a[0])
 167         elif len(a) == 2:
 168             skip_steps = int(a[0])
 169             num_steps = int(a[1])
 170         elif len(a) == 3:
 171             skip_steps = int(a[0])
 172             step_size = int(a[1])
 173             num_steps = int(a[2])
 174         else:
 175             assert False
 176     elif o == "--assume-skipped":
 177         assume_skipped = int(a)
 178     elif o == "--final-only":
 179         final_only = True
 180     elif o == "--smtc":
 181         inconstr.append(a)
 182     elif o == "--cex":
 183         cexfile = a
 184     elif o == "--aig":
 185         if ":" in a:
 186             aimfile, aiwfile = a.split(":")
 187         else:
 188             aimfile = a + ".aim"
 189             aiwfile = a + ".aiw"
 190     elif o == "--aig-noheader":
 191         aigheader = False
 192     elif o == "--dump-vcd":
 193         vcdfile = a
 194     elif o == "--dump-vlogtb":
 195         vlogtbfile = a
 196     elif o == "--vlogtb-top":
 197         vlogtbtop = a
 198     elif o == "--dump-smtc":
 199         outconstr = a
 200     elif o == "--smtc-init":
 201         smtcinit = True
 202     elif o == "--smtc-top":
 203         smtctop = a.split(":")
 204         if len(smtctop) == 1:
 205             smtctop.append("")
 206         assert len(smtctop) == 2
 207         smtctop = tuple(smtctop)
 208     elif o == "--dump-all":
 209         dumpall = True
 210     elif o == "--presat":
 211         presat = True
 212     elif o == "--noinfo":
 213         noinfo = True
 214     elif o == "--noinit":
 215         noinit = True
 216     elif o == "--append":
 217         append_steps = int(a)
 218     elif o == "-i":
 219         tempind = True
 220     elif o == "-g":
 221         gentrace = True
 222     elif o == "-c":
 223         covermode = True
 224     elif o == "-m":
 225         topmod = a
 226     elif so.handle(o, a):
 227         pass
 228     else:
 229         usage()
 230
 231 if len(args) != 1:
 232     usage()
 233
 234 if sum([tempind, gentrace, covermode]) > 1:
 235     usage()
 236
 237 constr_final_start = None
 238 constr_asserts = defaultdict(list)
 239 constr_assumes = defaultdict(list)
 240 constr_write = list()
 241
 242 for fn in inconstr:
 243     current_states = None
 244     current_line = 0
 245
 246     with open(fn, "r") as f:
 247         for line in f:
 248             current_line += 1
 249
 250             if line.startswith("#"):
 251                 continue
 252
 253             tokens = line.split()
 254
 255             if len(tokens) == 0:
 256                 continue
 257
 258             if tokens[0] == "initial":
 259                 current_states = set()
 260                 if not tempind:
 261                     current_states.add(0)
 262                 continue
 263
 264             if tokens[0] == "final":
 265                 constr_final = True
 266                 if len(tokens) == 1:
 267                     current_states = set(["final-%d" % i for i in range(0, num_steps+1)])
 268                     constr_final_start = 0
 269                 elif len(tokens) == 2:
 270                     arg = abs(int(tokens[1]))
 271                     current_states = set(["final-%d" % i for i in range(arg, num_steps+1)])
 272                     constr_final_start = arg if constr_final_start is None else min(constr_final_start, arg)
 273                 else:
 274                     assert False
 275                 continue
 276
 277             if tokens[0] == "state":
 278                 current_states = set()
 279                 if not tempind:
 280                     for token in tokens[1:]:
 281                         tok = token.split(":")
 282                         if len(tok) == 1:
 283                             current_states.add(int(token))
 284                         elif len(tok) == 2:
 285                             lower = int(tok[0])
 286                             if tok[1] == "*":
 287                                 upper = num_steps
 288                             else:
 289                                 upper = int(tok[1])
 290                             for i in range(lower, upper+1):
 291                                 current_states.add(i)
 292                         else:
 293                             assert False
 294                 continue
 295
 296             if tokens[0] == "always":
 297                 if len(tokens) == 1:
 298                     current_states = set(range(0, num_steps+1))
 299                 elif len(tokens) == 2:
 300                     arg = abs(int(tokens[1]))
 301                     current_states = set(range(arg, num_steps+1))
 302                 else:
 303                     assert False
 304                 continue
 305
 306             if tokens[0] == "assert":
 307                 assert current_states is not None
 308
 309                 for state in current_states:
 310                     constr_asserts[state].append(("%s:%d" % (fn, current_line), " ".join(tokens[1:])))
 311
 312                 continue
 313
 314             if tokens[0] == "assume":
 315                 assert current_states is not None
 316
 317                 for state in current_states:
 318                     constr_assumes[state].append(("%s:%d" % (fn, current_line), " ".join(tokens[1:])))
 319
 320                 continue
 321
 322             if tokens[0] == "write":
 323                 constr_write.append(" ".join(tokens[1:]))
 324                 continue
 325
 326             if tokens[0] == "logic":
 327                 so.logic = " ".join(tokens[1:])
 328                 continue
 329
 330             assert False
 331
 332
 333 def get_constr_expr(db, state, final=False, getvalues=False):
 334     if final:
 335         if ("final-%d" % state) not in db:
 336             return ([], [], []) if getvalues else "true"
 337     else:
 338         if state not in db:
 339             return ([], [], []) if getvalues else "true"
 340
 341     netref_regex = re.compile(r'(^|[( ])\[(-?[0-9]+:|)([^\]]*|\S*)\](?=[ )]|$)')
 342
 343     def replace_netref(match):
 344         state_sel = match.group(2)
 345
 346         if state_sel == "":
 347             st = state
 348         elif state_sel[0] == "-":
 349             st = state + int(state_sel[:-1])
 350         else:
 351             st = int(state_sel[:-1])
 352
 353         expr = smt.net_expr(topmod, "s%d" % st, smt.get_path(topmod, match.group(3)))
 354
 355         return match.group(1) + expr
 356
 357     expr_list = list()
 358     for loc, expr in db[("final-%d" % state) if final else state]:
 359         actual_expr = netref_regex.sub(replace_netref, expr)
 360         if getvalues:
 361             expr_list.append((loc, expr, actual_expr))
 362         else:
 363             expr_list.append(actual_expr)
 364
 365     if getvalues:
 366         loc_list, expr_list, acual_expr_list = zip(*expr_list)
 367         value_list = smt.get_list(acual_expr_list)
 368         return loc_list, expr_list, value_list
 369
 370     if len(expr_list) == 0:
 371         return "true"
 372
 373     if len(expr_list) == 1:
 374         return expr_list[0]
 375
 376     return "(and %s)" % " ".join(expr_list)
 377
 378
 379 smt = SmtIo(opts=so)
 380
 381 if noinfo and vcdfile is None and vlogtbfile is None and outconstr is None:
 382     smt.produce_models = False
 383
 384 def print_msg(msg):
 385     print("%s %s" % (smt.timestamp(), msg))
 386     sys.stdout.flush()
 387
 388 print_msg("Solver: %s" % (so.solver))
 389
 390 with open(args[0], "r") as f:
 391     for line in f:
 392         smt.write(line)
 393
 394 for line in constr_write:
 395     smt.write(line)
 396
 397 if topmod is None:
 398     topmod = smt.topmod
 399
 400 assert topmod is not None
 401 assert topmod in smt.modinfo
 402
 403 if cexfile is not None:
 404     if not got_topt:
 405         assume_skipped = 0
 406         skip_steps = 0
 407         num_steps = 0
 408
 409     with open(cexfile, "r") as f:
 410         cex_regex = re.compile(r'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
 411         for entry in f.read().split():
 412             match = cex_regex.match(entry)
 413             assert match
 414
 415             name, bit, extra_name, step, val = match.group(1), match.group(2), match.group(3), match.group(4), match.group(5)
 416
 417             if extra_name != "":
 418                 continue
 419
 420             if name not in smt.modinfo[topmod].inputs:
 421                 continue
 422
 423             if bit is None:
 424                 bit = 0
 425             else:
 426                 bit = int(bit[1:-1])
 427
 428             step = int(step[1:])
 429             val = int(val)
 430
 431             if smt.modinfo[topmod].wsize[name] == 1:
 432                 assert bit == 0
 433                 smtexpr = "(= [%s] %s)" % (name, "true" if val else "false")
 434             else:
 435                 smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bit, bit, name, val)
 436
 437             # print("cex@%d: %s" % (step, smtexpr))
 438             constr_assumes[step].append((cexfile, smtexpr))
 439
 440             if not got_topt:
 441                 skip_steps = max(skip_steps, step)
 442                 num_steps = max(num_steps, step+1)
 443
 444 if aimfile is not None:
 445     input_map = dict()
 446     init_map = dict()
 447     latch_map = dict()
 448
 449     if not got_topt:
 450         assume_skipped = 0
 451         skip_steps = 0
 452         num_steps = 0
 453
 454     with open(aimfile, "r") as f:
 455         for entry in f.read().splitlines():
 456             entry = entry.split()
 457
 458             if entry[0] == "input":
 459                 input_map[int(entry[1])] = (entry[3], int(entry[2]))
 460                 continue
 461
 462             if entry[0] == "init":
 463                 init_map[int(entry[1])] = (entry[3], int(entry[2]))
 464                 continue
 465
 466             if entry[0] in ["latch", "invlatch"]:
 467                 latch_map[int(entry[1])] = (entry[3], int(entry[2]), entry[0] == "invlatch")
 468                 continue
 469
 470             if entry[0] in ["output", "wire"]:
 471                 continue
 472
 473             assert False
 474
 475     with open(aiwfile, "r") as f:
 476         got_state = False
 477         got_ffinit = False
 478         step = 0
 479
 480         if not aigheader:
 481             got_state = True
 482
 483         for entry in f.read().splitlines():
 484             if len(entry) == 0 or entry[0] in "bcjfu.":
 485                 continue
 486
 487             if not got_state:
 488                 got_state = True
 489                 assert entry == "1"
 490                 continue
 491
 492             if not got_ffinit:
 493                 got_ffinit = True
 494                 if len(init_map) == 0:
 495                     for i in range(len(entry)):
 496                         if entry[i] == "x":
 497                             continue
 498
 499                         if i in latch_map:
 500                             value = int(entry[i])
 501                             name = latch_map[i][0]
 502                             bitidx = latch_map[i][1]
 503                             invert = latch_map[i][2]
 504
 505                             if invert:
 506                                 value = 1 - value
 507
 508                             path = smt.get_path(topmod, name)
 509                             width = smt.net_width(topmod, path)
 510
 511                             if width == 1:
 512                                 assert bitidx == 0
 513                                 smtexpr = "(= [%s] %s)" % (name, "true" if value else "false")
 514                             else:
 515                                 smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value)
 516
 517                             constr_assumes[0].append((cexfile, smtexpr))
 518                 continue
 519
 520             for i in range(len(entry)):
 521                 if entry[i] == "x":
 522                     continue
 523
 524                 if (step == 0) and (i in init_map):
 525                     value = int(entry[i])
 526                     name = init_map[i][0]
 527                     bitidx = init_map[i][1]
 528
 529                     path = smt.get_path(topmod, name)
 530
 531                     if not smt.net_exists(topmod, path):
 532                         match = re.match(r"(.*)\[(\d+)\]$", path[-1])
 533                         if match:
 534                             path[-1] = match.group(1)
 535                             addr = int(match.group(2))
 536
 537                         if not match or not smt.mem_exists(topmod, path):
 538                             print_msg("Ignoring init value for unknown net: %s" % (name))
 539                             continue
 540
 541                         meminfo = smt.mem_info(topmod, path)
 542                         smtexpr = "(select [%s] #b%s)" % (".".join(path), bin(addr)[2:].zfill(meminfo[0]))
 543                         width = meminfo[1]
 544
 545                     else:
 546                         smtexpr = "[%s]" % name
 547                         width = smt.net_width(topmod, path)
 548
 549                     if width == 1:
 550                         assert bitidx == 0
 551                         smtexpr = "(= %s %s)" % (smtexpr, "true" if value else "false")
 552                     else:
 553                         smtexpr = "(= ((_ extract %d %d) %s) #b%d)" % (bitidx, bitidx, smtexpr, value)
 554
 555                     constr_assumes[0].append((cexfile, smtexpr))
 556
 557                 if i in input_map:
 558                     value = int(entry[i])
 559                     name = input_map[i][0]
 560                     bitidx = input_map[i][1]
 561
 562                     path = smt.get_path(topmod, name)
 563                     width = smt.net_width(topmod, path)
 564
 565                     if width == 1:
 566                         assert bitidx == 0
 567                         smtexpr = "(= [%s] %s)" % (name, "true" if value else "false")
 568                     else:
 569                         smtexpr = "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx, bitidx, name, value)
 570
 571                     constr_assumes[step].append((cexfile, smtexpr))
 572
 573             if not got_topt:
 574                 skip_steps = max(skip_steps, step)
 575                 num_steps = max(num_steps, step+1)
 576             step += 1
 577
 578 def write_vcd_trace(steps_start, steps_stop, index):
 579     filename = vcdfile.replace("%", index)
 580     print_msg("Writing trace to VCD file: %s" % (filename))
 581
 582     with open(filename, "w") as vcd_file:
 583         vcd = MkVcd(vcd_file)
 584         path_list = list()
 585
 586         for netpath in sorted(smt.hiernets(topmod)):
 587             hidden_net = False
 588             for n in netpath:
 589                 if n.startswith("$"):
 590                     hidden_net = True
 591             if not hidden_net:
 592                 edge = smt.net_clock(topmod, netpath)
 593                 if edge is None:
 594                     vcd.add_net([topmod] + netpath, smt.net_width(topmod, netpath))
 595                 else:
 596                     vcd.add_clock([topmod] + netpath, edge)
 597                 path_list.append(netpath)
 598
 599         mem_trace_data = dict()
 600         for mempath in sorted(smt.hiermems(topmod)):
 601             abits, width, rports, wports, asyncwr = smt.mem_info(topmod, mempath)
 602
 603             expr_id = list()
 604             expr_list = list()
 605             for i in range(steps_start, steps_stop):
 606                 for j in range(rports):
 607                     expr_id.append(('R', i-steps_start, j, 'A'))
 608                     expr_id.append(('R', i-steps_start, j, 'D'))
 609                     expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dA" % j))
 610                     expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "R%dD" % j))
 611                 for j in range(wports):
 612                     expr_id.append(('W', i-steps_start, j, 'A'))
 613                     expr_id.append(('W', i-steps_start, j, 'D'))
 614                     expr_id.append(('W', i-steps_start, j, 'M'))
 615                     expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dA" % j))
 616                     expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dD" % j))
 617                     expr_list.append(smt.mem_expr(topmod, "s%d" % i, mempath, "W%dM" % j))
 618
 619             rdata = list()
 620             wdata = list()
 621             addrs = set()
 622
 623             for eid, edat in zip(expr_id, smt.get_list(expr_list)):
 624                 t, i, j, f = eid
 625
 626                 if t == 'R':
 627                     c = rdata
 628                 elif t == 'W':
 629                     c = wdata
 630                 else:
 631                     assert False
 632
 633                 while len(c) <= i:
 634                     c.append(list())
 635                 c = c[i]
 636
 637                 while len(c) <= j:
 638                     c.append(dict())
 639                 c = c[j]
 640
 641                 c[f] = smt.bv2bin(edat)
 642
 643                 if f == 'A':
 644                     addrs.add(c[f])
 645
 646             for addr in addrs:
 647                 tdata = list()
 648                 data = ["x"] * width
 649                 gotread = False
 650
 651                 if len(wdata) == 0 and len(rdata) != 0:
 652                     wdata = [[]] * len(rdata)
 653
 654                 assert len(rdata) == len(wdata)
 655
 656                 for i in range(len(wdata)):
 657                     if not gotread:
 658                         for j_data in rdata[i]:
 659                             if j_data["A"] == addr:
 660                                 data = list(j_data["D"])
 661                                 gotread = True
 662                                 break
 663
 664                         if gotread:
 665                             buf = data[:]
 666                             for i in reversed(range(len(tdata))):
 667                                 for k in range(width):
 668                                     if tdata[i][k] == "x":
 669                                         tdata[i][k] = buf[k]
 670                                     else:
 671                                         buf[k] = tdata[i][k]
 672
 673                     if not asyncwr:
 674                         tdata.append(data[:])
 675
 676                     for j_data in wdata[i]:
 677                         if j_data["A"] != addr:
 678                             continue
 679
 680                         D = j_data["D"]
 681                         M = j_data["M"]
 682
 683                         for k in range(width):
 684                             if M[k] == "1":
 685                                 data[k] = D[k]
 686
 687                     if asyncwr:
 688                         tdata.append(data[:])
 689
 690                 assert len(tdata) == len(rdata)
 691
 692                 netpath = mempath[:]
 693                 netpath[-1] += "<%0*x>" % ((len(addr)+3) // 4, int(addr, 2))
 694                 vcd.add_net([topmod] + netpath, width)
 695
 696                 for i in range(steps_start, steps_stop):
 697                     if i not in mem_trace_data:
 698                         mem_trace_data[i] = list()
 699                     mem_trace_data[i].append((netpath, "".join(tdata[i-steps_start])))
 700
 701         for i in range(steps_start, steps_stop):
 702             vcd.set_time(i)
 703             value_list = smt.get_net_bin_list(topmod, path_list, "s%d" % i)
 704             for path, value in zip(path_list, value_list):
 705                 vcd.set_net([topmod] + path, value)
 706             if i in mem_trace_data:
 707                 for path, value in mem_trace_data[i]:
 708                     vcd.set_net([topmod] + path, value)
 709
 710         vcd.set_time(steps_stop)
 711
 712
 713 def write_vlogtb_trace(steps_start, steps_stop, index):
 714     filename = vlogtbfile.replace("%", index)
 715     print_msg("Writing trace to Verilog testbench: %s" % (filename))
 716
 717     vlogtb_topmod = topmod
 718     vlogtb_state = "s@@step_idx@@"
 719
 720     if vlogtbtop is not None:
 721         for item in vlogtbtop.split("."):
 722             if item in smt.modinfo[vlogtb_topmod].cells:
 723                 vlogtb_state = "(|%s_h %s| %s)" % (vlogtb_topmod, item, vlogtb_state)
 724                 vlogtb_topmod = smt.modinfo[vlogtb_topmod].cells[item]
 725             else:
 726                 print_msg("Vlog top module '%s' not found: no cell '%s' in module '%s'" % (vlogtbtop, item, vlogtb_topmod))
 727                 break
 728
 729     with open(filename, "w") as f:
 730         print("`ifndef VERILATOR", file=f)
 731         print("module testbench;", file=f)
 732         print("  reg [4095:0] vcdfile;", file=f)
 733         print("  reg clock;", file=f)
 734         print("`else", file=f)
 735         print("module testbench(input clock, output reg genclock);", file=f)
 736         print("  initial genclock = 1;", file=f)
 737         print("`endif", file=f)
 738
 739         print("  reg genclock = 1;", file=f)
 740         print("  reg [31:0] cycle = 0;", file=f)
 741
 742         primary_inputs = list()
 743         clock_inputs = set()
 744
 745         for name in smt.modinfo[vlogtb_topmod].inputs:
 746             if name in ["clk", "clock", "CLK", "CLOCK"]:
 747                 clock_inputs.add(name)
 748             width = smt.modinfo[vlogtb_topmod].wsize[name]
 749             primary_inputs.append((name, width))
 750
 751         for name, width in primary_inputs:
 752             if name in clock_inputs:
 753                 print("  wire [%d:0] PI_%s = clock;" % (width-1, name), file=f)
 754             else:
 755                 print("  reg [%d:0] PI_%s;" % (width-1, name), file=f)
 756
 757         print("  %s UUT (" % vlogtb_topmod, file=f)
 758         print(",\n".join("    .{name}(PI_{name})".format(name=name) for name, _ in primary_inputs), file=f)
 759         print("  );", file=f)
 760
 761         print("`ifndef VERILATOR", file=f)
 762         print("  initial begin", file=f)
 763         print("    if ($value$plusargs(\"vcd=%s\", vcdfile)) begin", file=f)
 764         print("      $dumpfile(vcdfile);", file=f)
 765         print("      $dumpvars(0, testbench);", file=f)
 766         print("    end", file=f)
 767         print("    #5 clock = 0;", file=f)
 768         print("    while (genclock) begin", file=f)
 769         print("      #5 clock = 0;", file=f)
 770         print("      #5 clock = 1;", file=f)
 771         print("    end", file=f)
 772         print("  end", file=f)
 773         print("`endif", file=f)
 774
 775         print("  initial begin", file=f)
 776
 777         regs = sorted(smt.hiernets(vlogtb_topmod, regs_only=True))
 778         regvals = smt.get_net_bin_list(vlogtb_topmod, regs, vlogtb_state.replace("@@step_idx@@", str(steps_start)))
 779
 780         print("`ifndef VERILATOR", file=f)
 781         print("    #1;", file=f)
 782         print("`endif", file=f)
 783         for reg, val in zip(regs, regvals):
 784             hidden_net = False
 785             for n in reg:
 786                 if n.startswith("$"):
 787                     hidden_net = True
 788             print("    %sUUT.%s = %d'b%s;" % ("// " if hidden_net else "", ".".join(reg), len(val), val), file=f)
 789
 790         anyconsts = sorted(smt.hieranyconsts(vlogtb_topmod))
 791         for info in anyconsts:
 792             if info[3] is not None:
 793                 modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(steps_start)), info[0])
 794                 value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
 795                 print("    UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
 796
 797         mems = sorted(smt.hiermems(vlogtb_topmod))
 798         for mempath in mems:
 799             abits, width, rports, wports, asyncwr = smt.mem_info(vlogtb_topmod, mempath)
 800
 801             addr_expr_list = list()
 802             data_expr_list = list()
 803             for i in range(steps_start, steps_stop):
 804                 for j in range(rports):
 805                     addr_expr_list.append(smt.mem_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j))
 806                     data_expr_list.append(smt.mem_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j))
 807
 808             addr_list = smt.get_list(addr_expr_list)
 809             data_list = smt.get_list(data_expr_list)
 810
 811             addr_data = dict()
 812             for addr, data in zip(addr_list, data_list):
 813                 addr = smt.bv2bin(addr)
 814                 data = smt.bv2bin(data)
 815                 if addr not in addr_data:
 816                     addr_data[addr] = data
 817
 818             for addr, data in addr_data.items():
 819                 print("    UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath), len(addr), addr, len(data), data), file=f)
 820
 821         print("", file=f)
 822         anyseqs = sorted(smt.hieranyseqs(vlogtb_topmod))
 823
 824         for i in range(steps_start, steps_stop):
 825             pi_names = [[name] for name, _ in primary_inputs if name not in clock_inputs]
 826             pi_values = smt.get_net_bin_list(vlogtb_topmod, pi_names, vlogtb_state.replace("@@step_idx@@", str(i)))
 827
 828             print("    // state %d" % i, file=f)
 829
 830             if i > 0:
 831                 print("    if (cycle == %d) begin" % (i-1), file=f)
 832
 833             for name, val in zip(pi_names, pi_values):
 834                 if i > 0:
 835                     print("      PI_%s <= %d'b%s;" % (".".join(name), len(val), val), file=f)
 836                 else:
 837                     print("    PI_%s = %d'b%s;" % (".".join(name), len(val), val), file=f)
 838
 839             for info in anyseqs:
 840                 if info[3] is not None:
 841                     modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), info[0])
 842                     value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
 843                     if i > 0:
 844                         print("      UUT.%s <= %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
 845                     else:
 846                         print("    UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
 847
 848             if i > 0:
 849                 print("    end", file=f)
 850                 print("", file=f)
 851
 852             if i == 0:
 853                 print("  end", file=f)
 854                 print("  always @(posedge clock) begin", file=f)
 855
 856         print("    genclock <= cycle < %d;" % (steps_stop-1), file=f)
 857         print("    cycle <= cycle + 1;", file=f)
 858         print("  end", file=f)
 859
 860         print("endmodule", file=f)
 861
 862
 863 def write_constr_trace(steps_start, steps_stop, index):
 864     filename = outconstr.replace("%", index)
 865     print_msg("Writing trace to constraints file: %s" % (filename))
 866
 867     constr_topmod = topmod
 868     constr_state = "s@@step_idx@@"
 869     constr_prefix = ""
 870
 871     if smtctop is not None:
 872         for item in smtctop[0].split("."):
 873             assert item in smt.modinfo[constr_topmod].cells
 874             constr_state = "(|%s_h %s| %s)" % (constr_topmod, item, constr_state)
 875             constr_topmod = smt.modinfo[constr_topmod].cells[item]
 876         if smtctop[1] != "":
 877             constr_prefix = smtctop[1] + "."
 878
 879     if smtcinit:
 880         steps_start = steps_stop - 1
 881
 882     with open(filename, "w") as f:
 883         primary_inputs = list()
 884
 885         for name in smt.modinfo[constr_topmod].inputs:
 886             width = smt.modinfo[constr_topmod].wsize[name]
 887             primary_inputs.append((name, width))
 888
 889         if steps_start == 0 or smtcinit:
 890             print("initial", file=f)
 891         else:
 892             print("state %d" % steps_start, file=f)
 893
 894         regnames = sorted(smt.hiernets(constr_topmod, regs_only=True))
 895         regvals = smt.get_net_list(constr_topmod, regnames, constr_state.replace("@@step_idx@@", str(steps_start)))
 896
 897         for name, val in zip(regnames, regvals):
 898             print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)
 899
 900         mems = sorted(smt.hiermems(constr_topmod))
 901         for mempath in mems:
 902             abits, width, rports, wports, asyncwr = smt.mem_info(constr_topmod, mempath)
 903
 904             addr_expr_list = list()
 905             data_expr_list = list()
 906             for i in range(steps_start, steps_stop):
 907                 for j in range(rports):
 908                     addr_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j))
 909                     data_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j))
 910
 911             addr_list = smt.get_list(addr_expr_list)
 912             data_list = smt.get_list(data_expr_list)
 913
 914             addr_data = dict()
 915             for addr, data in zip(addr_list, data_list):
 916                 if addr not in addr_data:
 917                     addr_data[addr] = data
 918
 919             for addr, data in addr_data.items():
 920                 print("assume (= (select [%s%s] %s) %s)" % (constr_prefix, ".".join(mempath), addr, data), file=f)
 921
 922         for k in range(steps_start, steps_stop):
 923             if not smtcinit:
 924                 print("", file=f)
 925                 print("state %d" % k, file=f)
 926
 927             pi_names = [[name] for name, _ in sorted(primary_inputs)]
 928             pi_values = smt.get_net_list(constr_topmod, pi_names, constr_state.replace("@@step_idx@@", str(k)))
 929
 930             for name, val in zip(pi_names, pi_values):
 931                 print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)
 932
 933
 934 def write_trace(steps_start, steps_stop, index):
 935     if vcdfile is not None:
 936         write_vcd_trace(steps_start, steps_stop, index)
 937
 938     if vlogtbfile is not None:
 939         write_vlogtb_trace(steps_start, steps_stop, index)
 940
 941     if outconstr is not None:
 942         write_constr_trace(steps_start, steps_stop, index)
 943
 944
 945 def print_failed_asserts_worker(mod, state, path, extrainfo):
 946     assert mod in smt.modinfo
 947     found_failed_assert = False
 948
 949     if smt.get("(|%s_a| %s)" % (mod, state)) in ["true", "#b1"]:
 950         return
 951
 952     for cellname, celltype in smt.modinfo[mod].cells.items():
 953         if print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname, extrainfo):
 954             found_failed_assert = True
 955
 956     for assertfun, assertinfo in smt.modinfo[mod].asserts.items():
 957         if smt.get("(|%s| %s)" % (assertfun, state)) in ["false", "#b0"]:
 958             print_msg("Assert failed in %s: %s%s" % (path, assertinfo, extrainfo))
 959             found_failed_assert = True
 960
 961     return found_failed_assert
 962
 963
 964 def print_failed_asserts(state, final=False, extrainfo=""):
 965     if noinfo: return
 966     loc_list, expr_list, value_list = get_constr_expr(constr_asserts, state, final=final, getvalues=True)
 967     found_failed_assert = False
 968
 969     for loc, expr, value in zip(loc_list, expr_list, value_list):
 970         if smt.bv2int(value) == 0:
 971             print_msg("Assert %s failed: %s%s" % (loc, expr, extrainfo))
 972             found_failed_assert = True
 973
 974     if not final:
 975         if print_failed_asserts_worker(topmod, "s%d" % state, topmod, extrainfo):
 976             found_failed_assert = True
 977
 978     return found_failed_assert
 979
 980
 981 def print_anyconsts_worker(mod, state, path):
 982     assert mod in smt.modinfo
 983
 984     for cellname, celltype in smt.modinfo[mod].cells.items():
 985         print_anyconsts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
 986
 987     for fun, info in smt.modinfo[mod].anyconsts.items():
 988         if info[1] is None:
 989             print_msg("Value for anyconst in %s (%s): %d" % (path, info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
 990         else:
 991             print_msg("Value for anyconst %s.%s (%s): %d" % (path, info[1], info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
 992
 993
 994 def print_anyconsts(state):
 995     if noinfo: return
 996     print_anyconsts_worker(topmod, "s%d" % state, topmod)
 997
 998
 999 def get_cover_list(mod, base):
1000     assert mod in smt.modinfo
1001
1002     cover_expr = list()
1003     cover_desc = list()
1004
1005     for expr, desc in smt.modinfo[mod].covers.items():
1006         cover_expr.append("(ite (|%s| %s) #b1 #b0)" % (expr, base))
1007         cover_desc.append(desc)
1008
1009     for cell, submod in smt.modinfo[mod].cells.items():
1010         e, d = get_cover_list(submod, "(|%s_h %s| %s)" % (mod, cell, base))
1011         cover_expr += e
1012         cover_desc += d
1013
1014     return cover_expr, cover_desc
1015
1016 states = list()
1017 asserts_antecedent_cache = [list()]
1018 asserts_consequent_cache = [list()]
1019 asserts_cache_dirty = False
1020
1021 def smt_state(step):
1022     smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod))
1023     states.append("s%d" % step)
1024
1025 def smt_assert(expr):
1026     if expr == "true":
1027         return
1028
1029     smt.write("(assert %s)" % expr)
1030
1031 def smt_assert_antecedent(expr):
1032     if expr == "true":
1033         return
1034
1035     smt.write("(assert %s)" % expr)
1036
1037     global asserts_cache_dirty
1038     asserts_cache_dirty = True
1039     asserts_antecedent_cache[-1].append(expr)
1040
1041 def smt_assert_consequent(expr):
1042     if expr == "true":
1043         return
1044
1045     smt.write("(assert %s)" % expr)
1046
1047     global asserts_cache_dirty
1048     asserts_cache_dirty = True
1049     asserts_consequent_cache[-1].append(expr)
1050
1051 def smt_forall_assert():
1052     if not smt.forall:
1053         return
1054
1055     global asserts_cache_dirty
1056     asserts_cache_dirty = False
1057
1058     def make_assert_expr(asserts_cache):
1059         expr = list()
1060         for lst in asserts_cache:
1061             expr += lst
1062
1063         assert len(expr) != 0
1064
1065         if len(expr) == 1:
1066             expr = expr[0]
1067         else:
1068             expr = "(and %s)" % (" ".join(expr))
1069         return expr
1070
1071     antecedent_expr = make_assert_expr(asserts_antecedent_cache)
1072     consequent_expr = make_assert_expr(asserts_consequent_cache)
1073
1074     states_db = set(states)
1075     used_states_db = set()
1076     new_antecedent_expr = list()
1077     new_consequent_expr = list()
1078     assert_expr = list()
1079
1080     def make_new_expr(new_expr, expr):
1081         cursor = 0
1082         while cursor < len(expr):
1083             l = 1
1084             if expr[cursor] in '|"':
1085                 while cursor+l+1 < len(expr) and expr[cursor] != expr[cursor+l]:
1086                     l += 1
1087                 l += 1
1088             elif expr[cursor] not in '() ':
1089                 while cursor+l < len(expr) and expr[cursor+l] not in '|"() ':
1090                     l += 1
1091
1092             word = expr[cursor:cursor+l]
1093             if word in states_db:
1094                 used_states_db.add(word)
1095                 word += "_"
1096
1097             new_expr.append(word)
1098             cursor += l
1099
1100     make_new_expr(new_antecedent_expr, antecedent_expr)
1101     make_new_expr(new_consequent_expr, consequent_expr)
1102
1103     new_antecedent_expr = ["".join(new_antecedent_expr)]
1104     new_consequent_expr = ["".join(new_consequent_expr)]
1105
1106     if states[0] in used_states_db:
1107         new_antecedent_expr.append("(|%s_ex_state_eq| %s %s_)" % (topmod, states[0], states[0]))
1108     for s in states:
1109         if s in used_states_db:
1110             new_antecedent_expr.append("(|%s_ex_input_eq| %s %s_)" % (topmod, s, s))
1111
1112     if len(new_antecedent_expr) == 0:
1113         new_antecedent_expr = "true"
1114     elif len(new_antecedent_expr) == 1:
1115         new_antecedent_expr = new_antecedent_expr[0]
1116     else:
1117         new_antecedent_expr = "(and %s)" % (" ".join(new_antecedent_expr))
1118
1119     if len(new_consequent_expr) == 0:
1120         new_consequent_expr = "true"
1121     elif len(new_consequent_expr) == 1:
1122         new_consequent_expr = new_consequent_expr[0]
1123     else:
1124         new_consequent_expr = "(and %s)" % (" ".join(new_consequent_expr))
1125
1126     assert_expr.append("(assert (forall (")
1127     first_state = True
1128     for s in states:
1129         if s in used_states_db:
1130             assert_expr.append("%s(%s_ |%s_s|)" % ("" if first_state else " ", s, topmod))
1131             first_state = False
1132     assert_expr.append(") (=> %s %s)))" % (new_antecedent_expr, new_consequent_expr))
1133
1134     smt.write("".join(assert_expr))
1135
1136 def smt_push():
1137     global asserts_cache_dirty
1138     asserts_cache_dirty = True
1139     asserts_antecedent_cache.append(list())
1140     asserts_consequent_cache.append(list())
1141     smt.write("(push 1)")
1142
1143 def smt_pop():
1144     global asserts_cache_dirty
1145     asserts_cache_dirty = True
1146     asserts_antecedent_cache.pop()
1147     asserts_consequent_cache.pop()
1148     smt.write("(pop 1)")
1149
1150 def smt_check_sat():
1151     if asserts_cache_dirty:
1152         smt_forall_assert()
1153     return smt.check_sat()
1154
1155 if tempind:
1156     retstatus = False
1157     skip_counter = step_size
1158     for step in range(num_steps, -1, -1):
1159         if smt.forall:
1160             print_msg("Temporal induction not supported for exists-forall problems.")
1161             break
1162
1163         smt_state(step)
1164         smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
1165         smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
1166         smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1167         smt_assert_consequent(get_constr_expr(constr_assumes, step))
1168
1169         if step == num_steps:
1170             smt_assert("(not (and (|%s_a| s%d) %s))" % (topmod, step, get_constr_expr(constr_asserts, step)))
1171
1172         else:
1173             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step, step+1))
1174             smt_assert("(|%s_a| s%d)" % (topmod, step))
1175             smt_assert(get_constr_expr(constr_asserts, step))
1176
1177         if step > num_steps-skip_steps:
1178             print_msg("Skipping induction in step %d.." % (step))
1179             continue
1180
1181         skip_counter += 1
1182         if skip_counter < step_size:
1183             print_msg("Skipping induction in step %d.." % (step))
1184             continue
1185
1186         skip_counter = 0
1187         print_msg("Trying induction in step %d.." % (step))
1188
1189         if smt_check_sat() == "sat":
1190             if step == 0:
1191                 print_msg("Temporal induction failed!")
1192                 print_anyconsts(num_steps)
1193                 print_failed_asserts(num_steps)
1194                 write_trace(step, num_steps+1, '%')
1195
1196             elif dumpall:
1197                 print_anyconsts(num_steps)
1198                 print_failed_asserts(num_steps)
1199                 write_trace(step, num_steps+1, "%d" % step)
1200
1201         else:
1202             print_msg("Temporal induction successful.")
1203             retstatus = True
1204             break
1205
1206 elif covermode:
1207     cover_expr, cover_desc = get_cover_list(topmod, "state")
1208     cover_mask = "1" * len(cover_desc)
1209
1210     if len(cover_expr) > 1:
1211         cover_expr = "(concat %s)" % " ".join(cover_expr)
1212     elif len(cover_expr) == 1:
1213         cover_expr = cover_expr[0]
1214     else:
1215         cover_expr = "#b0"
1216
1217     coveridx = 0
1218     smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr))
1219
1220     step = 0
1221     retstatus = False
1222     found_failed_assert = False
1223
1224     assert step_size == 1
1225
1226     while step < num_steps:
1227         smt_state(step)
1228         smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
1229         smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
1230         smt_assert_consequent(get_constr_expr(constr_assumes, step))
1231
1232         if step == 0:
1233             if noinit:
1234                 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1235             else:
1236                 smt_assert_antecedent("(|%s_i| s0)" % (topmod))
1237                 smt_assert_antecedent("(|%s_is| s0)" % (topmod))
1238
1239         else:
1240             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step))
1241             smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1242
1243         while "1" in cover_mask:
1244             print_msg("Checking cover reachability in step %d.." % (step))
1245             smt_push()
1246             smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx, step, "0" * len(cover_desc)))
1247
1248             if smt_check_sat() == "unsat":
1249                 smt_pop()
1250                 break
1251
1252             if append_steps > 0:
1253                 for i in range(step+1, step+1+append_steps):
1254                     print_msg("Appending additional step %d." % i)
1255                     smt_state(i)
1256                     smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
1257                     smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
1258                     smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
1259                     smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
1260                     smt_assert_consequent(get_constr_expr(constr_assumes, i))
1261                 print_msg("Re-solving with appended steps..")
1262                 if smt_check_sat() == "unsat":
1263                     print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
1264                     found_failed_assert = True
1265                     retstatus = False
1266                     break
1267
1268             reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
1269             assert len(reached_covers) == len(cover_desc)
1270
1271             new_cover_mask = []
1272
1273             for i in range(len(reached_covers)):
1274                 if reached_covers[i] == "0":
1275                     new_cover_mask.append(cover_mask[i])
1276                     continue
1277
1278                 print_msg("Reached cover statement at %s in step %d." % (cover_desc[i], step))
1279                 new_cover_mask.append("0")
1280
1281             cover_mask = "".join(new_cover_mask)
1282
1283             for i in range(step+1+append_steps):
1284                 if print_failed_asserts(i, extrainfo=" (step %d)" % i):
1285                     found_failed_assert = True
1286
1287             write_trace(0, step+1+append_steps, "%d" % coveridx)
1288
1289             if found_failed_assert:
1290                 break
1291
1292             coveridx += 1
1293             smt_pop()
1294             smt.write("(define-fun covers_%d ((state |%s_s|)) (_ BitVec %d) (bvand (covers_%d state) #b%s))" % (coveridx, topmod, len(cover_desc), coveridx-1, cover_mask))
1295
1296         if found_failed_assert:
1297             break
1298
1299         if "1" not in cover_mask:
1300             retstatus = True
1301             break
1302
1303         step += 1
1304
1305     if "1" in cover_mask:
1306         for i in range(len(cover_mask)):
1307             if cover_mask[i] == "1":
1308                 print_msg("Unreached cover statement at %s." % cover_desc[i])
1309
1310 else:  # not tempind, covermode
1311     step = 0
1312     retstatus = True
1313     while step < num_steps:
1314         smt_state(step)
1315         smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
1316         smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
1317         smt_assert_consequent(get_constr_expr(constr_assumes, step))
1318
1319         if step == 0:
1320             if noinit:
1321                 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1322             else:
1323                 smt_assert_antecedent("(|%s_i| s0)" % (topmod))
1324                 smt_assert_antecedent("(|%s_is| s0)" % (topmod))
1325
1326         else:
1327             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step))
1328             smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1329
1330         if step < skip_steps:
1331             if assume_skipped is not None and step >= assume_skipped:
1332                 print_msg("Skipping step %d (and assuming pass).." % (step))
1333                 smt_assert("(|%s_a| s%d)" % (topmod, step))
1334                 smt_assert(get_constr_expr(constr_asserts, step))
1335             else:
1336                 print_msg("Skipping step %d.." % (step))
1337             step += 1
1338             continue
1339
1340         last_check_step = step
1341         for i in range(1, step_size):
1342             if step+i < num_steps:
1343                 smt_state(step+i)
1344                 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step+i))
1345                 smt_assert_consequent("(|%s_u| s%d)" % (topmod, step+i))
1346                 smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step+i))
1347                 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step+i-1, step+i))
1348                 smt_assert_consequent(get_constr_expr(constr_assumes, step+i))
1349                 last_check_step = step+i
1350
1351         if not gentrace:
1352             if presat:
1353                 if last_check_step == step:
1354                     print_msg("Checking assumptions in step %d.." % (step))
1355                 else:
1356                     print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step))
1357
1358                 if smt_check_sat() == "unsat":
1359                     print("%s Warmup failed!" % smt.timestamp())
1360                     retstatus = False
1361                     break
1362
1363             if not final_only:
1364                 if last_check_step == step:
1365                     print_msg("Checking assertions in step %d.." % (step))
1366                 else:
1367                     print_msg("Checking assertions in steps %d to %d.." % (step, last_check_step))
1368                 smt_push()
1369
1370                 smt_assert("(not (and %s))" % " ".join(["(|%s_a| s%d)" % (topmod, i) for i in range(step, last_check_step+1)] +
1371                         [get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)]))
1372
1373                 if smt_check_sat() == "sat":
1374                     print("%s BMC failed!" % smt.timestamp())
1375                     if append_steps > 0:
1376                         for i in range(last_check_step+1, last_check_step+1+append_steps):
1377                             print_msg("Appending additional step %d." % i)
1378                             smt_state(i)
1379                             smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
1380                             smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
1381                             smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
1382                             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
1383                             smt_assert_consequent(get_constr_expr(constr_assumes, i))
1384                     print_msg("Re-solving with appended steps..")
1385                     if smt_check_sat() == "unsat":
1386                         print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
1387                         retstatus = False
1388                         break
1389                     print_anyconsts(step)
1390                     for i in range(step, last_check_step+1):
1391                         print_failed_asserts(i)
1392                     write_trace(0, last_check_step+1+append_steps, '%')
1393                     retstatus = False
1394                     break
1395
1396                 smt_pop()
1397
1398             if (constr_final_start is not None) or (last_check_step+1 != num_steps):
1399                 for i in range(step, last_check_step+1):
1400                     smt_assert("(|%s_a| s%d)" % (topmod, i))
1401                     smt_assert(get_constr_expr(constr_asserts, i))
1402
1403             if constr_final_start is not None:
1404                 for i in range(step, last_check_step+1):
1405                     if i < constr_final_start:
1406                         continue
1407
1408                     print_msg("Checking final constraints in step %d.." % (i))
1409                     smt_push()
1410
1411                     smt_assert_consequent(get_constr_expr(constr_assumes, i, final=True))
1412                     smt_assert("(not %s)" % get_constr_expr(constr_asserts, i, final=True))
1413
1414                     if smt_check_sat() == "sat":
1415                         print("%s BMC failed!" % smt.timestamp())
1416                         print_anyconsts(i)
1417                         print_failed_asserts(i, final=True)
1418                         write_trace(0, i+1, '%')
1419                         retstatus = False
1420                         break
1421
1422                     smt_pop()
1423                 if not retstatus:
1424                     break
1425
1426         else:  # gentrace
1427             for i in range(step, last_check_step+1):
1428                 smt_assert("(|%s_a| s%d)" % (topmod, i))
1429                 smt_assert(get_constr_expr(constr_asserts, i))
1430
1431             print_msg("Solving for step %d.." % (last_check_step))
1432             if smt_check_sat() != "sat":
1433                 print("%s No solution found!" % smt.timestamp())
1434                 retstatus = False
1435                 break
1436
1437             elif dumpall:
1438                 print_anyconsts(0)
1439                 write_trace(0, last_check_step+1, "%d" % step)
1440
1441         step += step_size
1442
1443     if gentrace and retstatus:
1444         print_anyconsts(0)
1445         write_trace(0, num_steps, '%')
1446
1447
1448 smt.write("(exit)")
1449 smt.wait()
1450
1451 print_msg("Status: %s" % ("PASSED" if retstatus else "FAILED (!)"))
1452 sys.exit(0 if retstatus else 1)