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             assert 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
 726     with open(filename, "w") as f:
 727         print("`ifndef VERILATOR", file=f)
 728         print("module testbench;", file=f)
 729         print("  reg [4095:0] vcdfile;", file=f)
 730         print("  reg clock;", file=f)
 731         print("`else", file=f)
 732         print("module testbench(input clock, output reg genclock);", file=f)
 733         print("  initial genclock = 1;", file=f)
 734         print("`endif", file=f)
 735
 736         print("  reg genclock = 1;", file=f)
 737         print("  reg [31:0] cycle = 0;", file=f)
 738
 739         primary_inputs = list()
 740         clock_inputs = set()
 741
 742         for name in smt.modinfo[vlogtb_topmod].inputs:
 743             if name in ["clk", "clock", "CLK", "CLOCK"]:
 744                 clock_inputs.add(name)
 745             width = smt.modinfo[vlogtb_topmod].wsize[name]
 746             primary_inputs.append((name, width))
 747
 748         for name, width in primary_inputs:
 749             if name in clock_inputs:
 750                 print("  wire [%d:0] PI_%s = clock;" % (width-1, name), file=f)
 751             else:
 752                 print("  reg [%d:0] PI_%s;" % (width-1, name), file=f)
 753
 754         print("  %s UUT (" % vlogtb_topmod, file=f)
 755         print(",\n".join("    .{name}(PI_{name})".format(name=name) for name, _ in primary_inputs), file=f)
 756         print("  );", file=f)
 757
 758         print("`ifndef VERILATOR", file=f)
 759         print("  initial begin", file=f)
 760         print("    if ($value$plusargs(\"vcd=%s\", vcdfile)) begin", file=f)
 761         print("      $dumpfile(vcdfile);", file=f)
 762         print("      $dumpvars(0, testbench);", file=f)
 763         print("    end", file=f)
 764         print("    #5 clock = 0;", file=f)
 765         print("    while (genclock) begin", file=f)
 766         print("      #5 clock = 0;", file=f)
 767         print("      #5 clock = 1;", file=f)
 768         print("    end", file=f)
 769         print("  end", file=f)
 770         print("`endif", file=f)
 771
 772         print("  initial begin", file=f)
 773
 774         regs = sorted(smt.hiernets(vlogtb_topmod, regs_only=True))
 775         regvals = smt.get_net_bin_list(vlogtb_topmod, regs, vlogtb_state.replace("@@step_idx@@", str(steps_start)))
 776
 777         print("`ifndef VERILATOR", file=f)
 778         print("    #1;", file=f)
 779         print("`endif", file=f)
 780         for reg, val in zip(regs, regvals):
 781             hidden_net = False
 782             for n in reg:
 783                 if n.startswith("$"):
 784                     hidden_net = True
 785             print("    %sUUT.%s = %d'b%s;" % ("// " if hidden_net else "", ".".join(reg), len(val), val), file=f)
 786
 787         anyconsts = sorted(smt.hieranyconsts(vlogtb_topmod))
 788         for info in anyconsts:
 789             if info[3] is not None:
 790                 modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(steps_start)), info[0])
 791                 value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
 792                 print("    UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
 793
 794         mems = sorted(smt.hiermems(vlogtb_topmod))
 795         for mempath in mems:
 796             abits, width, rports, wports, asyncwr = smt.mem_info(vlogtb_topmod, mempath)
 797
 798             addr_expr_list = list()
 799             data_expr_list = list()
 800             for i in range(steps_start, steps_stop):
 801                 for j in range(rports):
 802                     addr_expr_list.append(smt.mem_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j))
 803                     data_expr_list.append(smt.mem_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j))
 804
 805             addr_list = smt.get_list(addr_expr_list)
 806             data_list = smt.get_list(data_expr_list)
 807
 808             addr_data = dict()
 809             for addr, data in zip(addr_list, data_list):
 810                 addr = smt.bv2bin(addr)
 811                 data = smt.bv2bin(data)
 812                 if addr not in addr_data:
 813                     addr_data[addr] = data
 814
 815             for addr, data in addr_data.items():
 816                 print("    UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath), len(addr), addr, len(data), data), file=f)
 817
 818         print("", file=f)
 819         anyseqs = sorted(smt.hieranyseqs(vlogtb_topmod))
 820
 821         for i in range(steps_start, steps_stop):
 822             pi_names = [[name] for name, _ in primary_inputs if name not in clock_inputs]
 823             pi_values = smt.get_net_bin_list(vlogtb_topmod, pi_names, vlogtb_state.replace("@@step_idx@@", str(i)))
 824
 825             print("    // state %d" % i, file=f)
 826
 827             if i > 0:
 828                 print("    if (cycle == %d) begin" % (i-1), file=f)
 829
 830             for name, val in zip(pi_names, pi_values):
 831                 if i > 0:
 832                     print("      PI_%s <= %d'b%s;" % (".".join(name), len(val), val), file=f)
 833                 else:
 834                     print("    PI_%s = %d'b%s;" % (".".join(name), len(val), val), file=f)
 835
 836             for info in anyseqs:
 837                 if info[3] is not None:
 838                     modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), info[0])
 839                     value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
 840                     if i > 0:
 841                         print("      UUT.%s <= %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
 842                     else:
 843                         print("    UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
 844
 845             if i > 0:
 846                 print("    end", file=f)
 847                 print("", file=f)
 848
 849             if i == 0:
 850                 print("  end", file=f)
 851                 print("  always @(posedge clock) begin", file=f)
 852
 853         print("    genclock <= cycle < %d;" % (steps_stop-1), file=f)
 854         print("    cycle <= cycle + 1;", file=f)
 855         print("  end", file=f)
 856
 857         print("endmodule", file=f)
 858
 859
 860 def write_constr_trace(steps_start, steps_stop, index):
 861     filename = outconstr.replace("%", index)
 862     print_msg("Writing trace to constraints file: %s" % (filename))
 863
 864     constr_topmod = topmod
 865     constr_state = "s@@step_idx@@"
 866     constr_prefix = ""
 867
 868     if smtctop is not None:
 869         for item in smtctop[0].split("."):
 870             assert item in smt.modinfo[constr_topmod].cells
 871             constr_state = "(|%s_h %s| %s)" % (constr_topmod, item, constr_state)
 872             constr_topmod = smt.modinfo[constr_topmod].cells[item]
 873         if smtctop[1] != "":
 874             constr_prefix = smtctop[1] + "."
 875
 876     if smtcinit:
 877         steps_start = steps_stop - 1
 878
 879     with open(filename, "w") as f:
 880         primary_inputs = list()
 881
 882         for name in smt.modinfo[constr_topmod].inputs:
 883             width = smt.modinfo[constr_topmod].wsize[name]
 884             primary_inputs.append((name, width))
 885
 886         if steps_start == 0 or smtcinit:
 887             print("initial", file=f)
 888         else:
 889             print("state %d" % steps_start, file=f)
 890
 891         regnames = sorted(smt.hiernets(constr_topmod, regs_only=True))
 892         regvals = smt.get_net_list(constr_topmod, regnames, constr_state.replace("@@step_idx@@", str(steps_start)))
 893
 894         for name, val in zip(regnames, regvals):
 895             print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)
 896
 897         mems = sorted(smt.hiermems(constr_topmod))
 898         for mempath in mems:
 899             abits, width, rports, wports, asyncwr = smt.mem_info(constr_topmod, mempath)
 900
 901             addr_expr_list = list()
 902             data_expr_list = list()
 903             for i in range(steps_start, steps_stop):
 904                 for j in range(rports):
 905                     addr_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j))
 906                     data_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j))
 907
 908             addr_list = smt.get_list(addr_expr_list)
 909             data_list = smt.get_list(data_expr_list)
 910
 911             addr_data = dict()
 912             for addr, data in zip(addr_list, data_list):
 913                 if addr not in addr_data:
 914                     addr_data[addr] = data
 915
 916             for addr, data in addr_data.items():
 917                 print("assume (= (select [%s%s] %s) %s)" % (constr_prefix, ".".join(mempath), addr, data), file=f)
 918
 919         for k in range(steps_start, steps_stop):
 920             if not smtcinit:
 921                 print("", file=f)
 922                 print("state %d" % k, file=f)
 923
 924             pi_names = [[name] for name, _ in sorted(primary_inputs)]
 925             pi_values = smt.get_net_list(constr_topmod, pi_names, constr_state.replace("@@step_idx@@", str(k)))
 926
 927             for name, val in zip(pi_names, pi_values):
 928                 print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)
 929
 930
 931 def write_trace(steps_start, steps_stop, index):
 932     if vcdfile is not None:
 933         write_vcd_trace(steps_start, steps_stop, index)
 934
 935     if vlogtbfile is not None:
 936         write_vlogtb_trace(steps_start, steps_stop, index)
 937
 938     if outconstr is not None:
 939         write_constr_trace(steps_start, steps_stop, index)
 940
 941
 942 def print_failed_asserts_worker(mod, state, path, extrainfo):
 943     assert mod in smt.modinfo
 944     found_failed_assert = False
 945
 946     if smt.get("(|%s_a| %s)" % (mod, state)) in ["true", "#b1"]:
 947         return
 948
 949     for cellname, celltype in smt.modinfo[mod].cells.items():
 950         if print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname, extrainfo):
 951             found_failed_assert = True
 952
 953     for assertfun, assertinfo in smt.modinfo[mod].asserts.items():
 954         if smt.get("(|%s| %s)" % (assertfun, state)) in ["false", "#b0"]:
 955             print_msg("Assert failed in %s: %s%s" % (path, assertinfo, extrainfo))
 956             found_failed_assert = True
 957
 958     return found_failed_assert
 959
 960
 961 def print_failed_asserts(state, final=False, extrainfo=""):
 962     if noinfo: return
 963     loc_list, expr_list, value_list = get_constr_expr(constr_asserts, state, final=final, getvalues=True)
 964     found_failed_assert = False
 965
 966     for loc, expr, value in zip(loc_list, expr_list, value_list):
 967         if smt.bv2int(value) == 0:
 968             print_msg("Assert %s failed: %s%s" % (loc, expr, extrainfo))
 969             found_failed_assert = True
 970
 971     if not final:
 972         if print_failed_asserts_worker(topmod, "s%d" % state, topmod, extrainfo):
 973             found_failed_assert = True
 974
 975     return found_failed_assert
 976
 977
 978 def print_anyconsts_worker(mod, state, path):
 979     assert mod in smt.modinfo
 980
 981     for cellname, celltype in smt.modinfo[mod].cells.items():
 982         print_anyconsts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
 983
 984     for fun, info in smt.modinfo[mod].anyconsts.items():
 985         if info[1] is None:
 986             print_msg("Value for anyconst in %s (%s): %d" % (path, info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
 987         else:
 988             print_msg("Value for anyconst %s.%s (%s): %d" % (path, info[1], info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
 989
 990
 991 def print_anyconsts(state):
 992     if noinfo: return
 993     print_anyconsts_worker(topmod, "s%d" % state, topmod)
 994
 995
 996 def get_cover_list(mod, base):
 997     assert mod in smt.modinfo
 998
 999     cover_expr = list()
1000     cover_desc = list()
1001
1002     for expr, desc in smt.modinfo[mod].covers.items():
1003         cover_expr.append("(ite (|%s| %s) #b1 #b0)" % (expr, base))
1004         cover_desc.append(desc)
1005
1006     for cell, submod in smt.modinfo[mod].cells.items():
1007         e, d = get_cover_list(submod, "(|%s_h %s| %s)" % (mod, cell, base))
1008         cover_expr += e
1009         cover_desc += d
1010
1011     return cover_expr, cover_desc
1012
1013 states = list()
1014 asserts_antecedent_cache = [list()]
1015 asserts_consequent_cache = [list()]
1016 asserts_cache_dirty = False
1017
1018 def smt_state(step):
1019     smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod))
1020     states.append("s%d" % step)
1021
1022 def smt_assert(expr):
1023     if expr == "true":
1024         return
1025
1026     smt.write("(assert %s)" % expr)
1027
1028 def smt_assert_antecedent(expr):
1029     if expr == "true":
1030         return
1031
1032     smt.write("(assert %s)" % expr)
1033
1034     global asserts_cache_dirty
1035     asserts_cache_dirty = True
1036     asserts_antecedent_cache[-1].append(expr)
1037
1038 def smt_assert_consequent(expr):
1039     if expr == "true":
1040         return
1041
1042     smt.write("(assert %s)" % expr)
1043
1044     global asserts_cache_dirty
1045     asserts_cache_dirty = True
1046     asserts_consequent_cache[-1].append(expr)
1047
1048 def smt_forall_assert():
1049     if not smt.forall:
1050         return
1051
1052     global asserts_cache_dirty
1053     asserts_cache_dirty = False
1054
1055     def make_assert_expr(asserts_cache):
1056         expr = list()
1057         for lst in asserts_cache:
1058             expr += lst
1059
1060         assert len(expr) != 0
1061
1062         if len(expr) == 1:
1063             expr = expr[0]
1064         else:
1065             expr = "(and %s)" % (" ".join(expr))
1066         return expr
1067
1068     antecedent_expr = make_assert_expr(asserts_antecedent_cache)
1069     consequent_expr = make_assert_expr(asserts_consequent_cache)
1070
1071     states_db = set(states)
1072     used_states_db = set()
1073     new_antecedent_expr = list()
1074     new_consequent_expr = list()
1075     assert_expr = list()
1076
1077     def make_new_expr(new_expr, expr):
1078         cursor = 0
1079         while cursor < len(expr):
1080             l = 1
1081             if expr[cursor] in '|"':
1082                 while cursor+l+1 < len(expr) and expr[cursor] != expr[cursor+l]:
1083                     l += 1
1084                 l += 1
1085             elif expr[cursor] not in '() ':
1086                 while cursor+l < len(expr) and expr[cursor+l] not in '|"() ':
1087                     l += 1
1088
1089             word = expr[cursor:cursor+l]
1090             if word in states_db:
1091                 used_states_db.add(word)
1092                 word += "_"
1093
1094             new_expr.append(word)
1095             cursor += l
1096
1097     make_new_expr(new_antecedent_expr, antecedent_expr)
1098     make_new_expr(new_consequent_expr, consequent_expr)
1099
1100     new_antecedent_expr = ["".join(new_antecedent_expr)]
1101     new_consequent_expr = ["".join(new_consequent_expr)]
1102
1103     if states[0] in used_states_db:
1104         new_antecedent_expr.append("(|%s_ex_state_eq| %s %s_)" % (topmod, states[0], states[0]))
1105     for s in states:
1106         if s in used_states_db:
1107             new_antecedent_expr.append("(|%s_ex_input_eq| %s %s_)" % (topmod, s, s))
1108
1109     if len(new_antecedent_expr) == 0:
1110         new_antecedent_expr = "true"
1111     elif len(new_antecedent_expr) == 1:
1112         new_antecedent_expr = new_antecedent_expr[0]
1113     else:
1114         new_antecedent_expr = "(and %s)" % (" ".join(new_antecedent_expr))
1115
1116     if len(new_consequent_expr) == 0:
1117         new_consequent_expr = "true"
1118     elif len(new_consequent_expr) == 1:
1119         new_consequent_expr = new_consequent_expr[0]
1120     else:
1121         new_consequent_expr = "(and %s)" % (" ".join(new_consequent_expr))
1122
1123     assert_expr.append("(assert (forall (")
1124     first_state = True
1125     for s in states:
1126         if s in used_states_db:
1127             assert_expr.append("%s(%s_ |%s_s|)" % ("" if first_state else " ", s, topmod))
1128             first_state = False
1129     assert_expr.append(") (=> %s %s)))" % (new_antecedent_expr, new_consequent_expr))
1130
1131     smt.write("".join(assert_expr))
1132
1133 def smt_push():
1134     global asserts_cache_dirty
1135     asserts_cache_dirty = True
1136     asserts_antecedent_cache.append(list())
1137     asserts_consequent_cache.append(list())
1138     smt.write("(push 1)")
1139
1140 def smt_pop():
1141     global asserts_cache_dirty
1142     asserts_cache_dirty = True
1143     asserts_antecedent_cache.pop()
1144     asserts_consequent_cache.pop()
1145     smt.write("(pop 1)")
1146
1147 def smt_check_sat():
1148     if asserts_cache_dirty:
1149         smt_forall_assert()
1150     return smt.check_sat()
1151
1152 if tempind:
1153     retstatus = False
1154     skip_counter = step_size
1155     for step in range(num_steps, -1, -1):
1156         if smt.forall:
1157             print_msg("Temporal induction not supported for exists-forall problems.")
1158             break
1159
1160         smt_state(step)
1161         smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
1162         smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
1163         smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1164         smt_assert_consequent(get_constr_expr(constr_assumes, step))
1165
1166         if step == num_steps:
1167             smt_assert("(not (and (|%s_a| s%d) %s))" % (topmod, step, get_constr_expr(constr_asserts, step)))
1168
1169         else:
1170             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step, step+1))
1171             smt_assert("(|%s_a| s%d)" % (topmod, step))
1172             smt_assert(get_constr_expr(constr_asserts, step))
1173
1174         if step > num_steps-skip_steps:
1175             print_msg("Skipping induction in step %d.." % (step))
1176             continue
1177
1178         skip_counter += 1
1179         if skip_counter < step_size:
1180             print_msg("Skipping induction in step %d.." % (step))
1181             continue
1182
1183         skip_counter = 0
1184         print_msg("Trying induction in step %d.." % (step))
1185
1186         if smt_check_sat() == "sat":
1187             if step == 0:
1188                 print_msg("Temporal induction failed!")
1189                 print_anyconsts(num_steps)
1190                 print_failed_asserts(num_steps)
1191                 write_trace(step, num_steps+1, '%')
1192
1193             elif dumpall:
1194                 print_anyconsts(num_steps)
1195                 print_failed_asserts(num_steps)
1196                 write_trace(step, num_steps+1, "%d" % step)
1197
1198         else:
1199             print_msg("Temporal induction successful.")
1200             retstatus = True
1201             break
1202
1203 elif covermode:
1204     cover_expr, cover_desc = get_cover_list(topmod, "state")
1205     cover_mask = "1" * len(cover_desc)
1206
1207     if len(cover_expr) > 1:
1208         cover_expr = "(concat %s)" % " ".join(cover_expr)
1209     elif len(cover_expr) == 1:
1210         cover_expr = cover_expr[0]
1211     else:
1212         cover_expr = "#b0"
1213
1214     coveridx = 0
1215     smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr))
1216
1217     step = 0
1218     retstatus = False
1219     found_failed_assert = False
1220
1221     assert step_size == 1
1222
1223     while step < num_steps:
1224         smt_state(step)
1225         smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
1226         smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
1227         smt_assert_consequent(get_constr_expr(constr_assumes, step))
1228
1229         if step == 0:
1230             if noinit:
1231                 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1232             else:
1233                 smt_assert_antecedent("(|%s_i| s0)" % (topmod))
1234                 smt_assert_antecedent("(|%s_is| s0)" % (topmod))
1235
1236         else:
1237             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step))
1238             smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1239
1240         while "1" in cover_mask:
1241             print_msg("Checking cover reachability in step %d.." % (step))
1242             smt_push()
1243             smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx, step, "0" * len(cover_desc)))
1244
1245             if smt_check_sat() == "unsat":
1246                 smt_pop()
1247                 break
1248
1249             if append_steps > 0:
1250                 for i in range(step+1, step+1+append_steps):
1251                     print_msg("Appending additional step %d." % i)
1252                     smt_state(i)
1253                     smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
1254                     smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
1255                     smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
1256                     smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
1257                     smt_assert_consequent(get_constr_expr(constr_assumes, i))
1258                 print_msg("Re-solving with appended steps..")
1259                 assert smt_check_sat() == "sat"
1260
1261             reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
1262             assert len(reached_covers) == len(cover_desc)
1263
1264             new_cover_mask = []
1265
1266             for i in range(len(reached_covers)):
1267                 if reached_covers[i] == "0":
1268                     new_cover_mask.append(cover_mask[i])
1269                     continue
1270
1271                 print_msg("Reached cover statement at %s in step %d." % (cover_desc[i], step))
1272                 new_cover_mask.append("0")
1273
1274             cover_mask = "".join(new_cover_mask)
1275
1276             for i in range(step+1+append_steps):
1277                 if print_failed_asserts(i, extrainfo=" (step %d)" % i):
1278                     found_failed_assert = True
1279
1280             write_trace(0, step+1+append_steps, "%d" % coveridx)
1281
1282             if found_failed_assert:
1283                 break
1284
1285             coveridx += 1
1286             smt_pop()
1287             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))
1288
1289         if found_failed_assert:
1290             break
1291
1292         if "1" not in cover_mask:
1293             retstatus = True
1294             break
1295
1296         step += 1
1297
1298     if "1" in cover_mask:
1299         for i in range(len(cover_mask)):
1300             if cover_mask[i] == "1":
1301                 print_msg("Unreached cover statement at %s." % cover_desc[i])
1302
1303 else:  # not tempind, covermode
1304     step = 0
1305     retstatus = True
1306     while step < num_steps:
1307         smt_state(step)
1308         smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
1309         smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
1310         smt_assert_consequent(get_constr_expr(constr_assumes, step))
1311
1312         if step == 0:
1313             if noinit:
1314                 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1315             else:
1316                 smt_assert_antecedent("(|%s_i| s0)" % (topmod))
1317                 smt_assert_antecedent("(|%s_is| s0)" % (topmod))
1318
1319         else:
1320             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step))
1321             smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1322
1323         if step < skip_steps:
1324             if assume_skipped is not None and step >= assume_skipped:
1325                 print_msg("Skipping step %d (and assuming pass).." % (step))
1326                 smt_assert("(|%s_a| s%d)" % (topmod, step))
1327                 smt_assert(get_constr_expr(constr_asserts, step))
1328             else:
1329                 print_msg("Skipping step %d.." % (step))
1330             step += 1
1331             continue
1332
1333         last_check_step = step
1334         for i in range(1, step_size):
1335             if step+i < num_steps:
1336                 smt_state(step+i)
1337                 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step+i))
1338                 smt_assert_consequent("(|%s_u| s%d)" % (topmod, step+i))
1339                 smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step+i))
1340                 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step+i-1, step+i))
1341                 smt_assert_consequent(get_constr_expr(constr_assumes, step+i))
1342                 last_check_step = step+i
1343
1344         if not gentrace:
1345             if presat:
1346                 if last_check_step == step:
1347                     print_msg("Checking assumptions in step %d.." % (step))
1348                 else:
1349                     print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step))
1350
1351                 if smt_check_sat() == "unsat":
1352                     print("%s Warmup failed!" % smt.timestamp())
1353                     retstatus = False
1354                     break
1355
1356             if not final_only:
1357                 if last_check_step == step:
1358                     print_msg("Checking assertions in step %d.." % (step))
1359                 else:
1360                     print_msg("Checking assertions in steps %d to %d.." % (step, last_check_step))
1361                 smt_push()
1362
1363                 smt_assert("(not (and %s))" % " ".join(["(|%s_a| s%d)" % (topmod, i) for i in range(step, last_check_step+1)] +
1364                         [get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)]))
1365
1366                 if smt_check_sat() == "sat":
1367                     print("%s BMC failed!" % smt.timestamp())
1368                     if append_steps > 0:
1369                         for i in range(last_check_step+1, last_check_step+1+append_steps):
1370                             print_msg("Appending additional step %d." % i)
1371                             smt_state(i)
1372                             smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
1373                             smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
1374                             smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
1375                             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
1376                             smt_assert_consequent(get_constr_expr(constr_assumes, i))
1377                             assert smt_check_sat() == "sat"
1378                     print_anyconsts(step)
1379                     for i in range(step, last_check_step+1):
1380                         print_failed_asserts(i)
1381                     write_trace(0, last_check_step+1+append_steps, '%')
1382                     retstatus = False
1383                     break
1384
1385                 smt_pop()
1386
1387             if (constr_final_start is not None) or (last_check_step+1 != num_steps):
1388                 for i in range(step, last_check_step+1):
1389                     smt_assert("(|%s_a| s%d)" % (topmod, i))
1390                     smt_assert(get_constr_expr(constr_asserts, i))
1391
1392             if constr_final_start is not None:
1393                 for i in range(step, last_check_step+1):
1394                     if i < constr_final_start:
1395                         continue
1396
1397                     print_msg("Checking final constraints in step %d.." % (i))
1398                     smt_push()
1399
1400                     smt_assert_consequent(get_constr_expr(constr_assumes, i, final=True))
1401                     smt_assert("(not %s)" % get_constr_expr(constr_asserts, i, final=True))
1402
1403                     if smt_check_sat() == "sat":
1404                         print("%s BMC failed!" % smt.timestamp())
1405                         print_anyconsts(i)
1406                         print_failed_asserts(i, final=True)
1407                         write_trace(0, i+1, '%')
1408                         retstatus = False
1409                         break
1410
1411                     smt_pop()
1412                 if not retstatus:
1413                     break
1414
1415         else:  # gentrace
1416             for i in range(step, last_check_step+1):
1417                 smt_assert("(|%s_a| s%d)" % (topmod, i))
1418                 smt_assert(get_constr_expr(constr_asserts, i))
1419
1420             print_msg("Solving for step %d.." % (last_check_step))
1421             if smt_check_sat() != "sat":
1422                 print("%s No solution found!" % smt.timestamp())
1423                 retstatus = False
1424                 break
1425
1426             elif dumpall:
1427                 print_anyconsts(0)
1428                 write_trace(0, last_check_step+1, "%d" % step)
1429
1430         step += step_size
1431
1432     if gentrace and retstatus:
1433         print_anyconsts(0)
1434         write_trace(0, num_steps, '%')
1435
1436
1437 smt.write("(exit)")
1438 smt.wait()
1439
1440 print_msg("Status: %s" % ("PASSED" if retstatus else "FAILED (!)"))
1441 sys.exit(0 if retstatus else 1)