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