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