backends/smt2/smtbmc.py

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