backends/smt2/smtbmc.py

   1 #!/usr/bin/env python3
   2 #
   3 # yosys -- Yosys Open SYnthesis Suite
   4 #
   5 # Copyright (C) 2012  Clifford Wolf <clifford@clifford.at>
   6 #
   7 # Permission to use, copy, modify, and/or distribute this software for any
   8 # purpose with or without fee is hereby granted, provided that the above
   9 # copyright notice and this permission notice appear in all copies.
  10 #
  11 # THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
  12 # WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
  13 # MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
  14 # ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
  15 # WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
  16 # ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
  17 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
  18 #
  19
  20 import os, sys, getopt, re
  21 ##yosys-sys-path##
  22 from smtio import SmtIo, SmtOpts, MkVcd
  23 from collections import defaultdict
  24
  25 got_topt = False
  26 skip_steps = 0
  27 step_size = 1
  28 num_steps = 20
  29 append_steps = 0
  30 vcdfile = None
  31 cexfile = None
  32 aimfile = None
  33 aiwfile = None
  34 aigheader = True
  35 btorwitfile = None
  36 vlogtbfile = None
  37 vlogtbtop = None
  38 inconstr = list()
  39 outconstr = None
  40 gentrace = False
  41 covermode = False
  42 tempind = False
  43 dumpall = False
  44 assume_skipped = None
  45 final_only = False
  46 topmod = None
  47 noinfo = False
  48 presat = False
  49 smtcinit = False
  50 smtctop = None
  51 noinit = False
  52 binarymode = False
  53 so = SmtOpts()
  54
  55
  56 def usage():
  57     print(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 i in reversed(range(len(tdata))):
 775                                 for k in range(width):
 776                                     if tdata[i][k] == "x":
 777                                         tdata[i][k] = buf[k]
 778                                     else:
 779                                         buf[k] = tdata[i][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
 821 def write_vlogtb_trace(steps_start, steps_stop, index):
 822     filename = vlogtbfile.replace("%", index)
 823     print_msg("Writing trace to Verilog testbench: %s" % (filename))
 824
 825     vlogtb_topmod = topmod
 826     vlogtb_state = "s@@step_idx@@"
 827
 828     if vlogtbtop is not None:
 829         for item in vlogtbtop.split("."):
 830             if item in smt.modinfo[vlogtb_topmod].cells:
 831                 vlogtb_state = "(|%s_h %s| %s)" % (vlogtb_topmod, item, vlogtb_state)
 832                 vlogtb_topmod = smt.modinfo[vlogtb_topmod].cells[item]
 833             else:
 834                 print_msg("Vlog top module '%s' not found: no cell '%s' in module '%s'" % (vlogtbtop, item, vlogtb_topmod))
 835                 break
 836
 837     with open(filename, "w") as f:
 838         print("`ifndef VERILATOR", file=f)
 839         print("module testbench;", file=f)
 840         print("  reg [4095:0] vcdfile;", file=f)
 841         print("  reg clock;", file=f)
 842         print("`else", file=f)
 843         print("module testbench(input clock, output reg genclock);", file=f)
 844         print("  initial genclock = 1;", file=f)
 845         print("`endif", file=f)
 846
 847         print("  reg genclock = 1;", file=f)
 848         print("  reg [31:0] cycle = 0;", file=f)
 849
 850         primary_inputs = list()
 851         clock_inputs = set()
 852
 853         for name in smt.modinfo[vlogtb_topmod].inputs:
 854             if name in ["clk", "clock", "CLK", "CLOCK"]:
 855                 clock_inputs.add(name)
 856             width = smt.modinfo[vlogtb_topmod].wsize[name]
 857             primary_inputs.append((name, width))
 858
 859         for name, width in primary_inputs:
 860             if name in clock_inputs:
 861                 print("  wire [%d:0] PI_%s = clock;" % (width-1, name), file=f)
 862             else:
 863                 print("  reg [%d:0] PI_%s;" % (width-1, name), file=f)
 864
 865         print("  %s UUT (" % vlogtb_topmod, file=f)
 866         print(",\n".join("    .{name}(PI_{name})".format(name=name) for name, _ in primary_inputs), file=f)
 867         print("  );", file=f)
 868
 869         print("`ifndef VERILATOR", file=f)
 870         print("  initial begin", file=f)
 871         print("    if ($value$plusargs(\"vcd=%s\", vcdfile)) begin", file=f)
 872         print("      $dumpfile(vcdfile);", file=f)
 873         print("      $dumpvars(0, testbench);", file=f)
 874         print("    end", file=f)
 875         print("    #5 clock = 0;", file=f)
 876         print("    while (genclock) begin", file=f)
 877         print("      #5 clock = 0;", file=f)
 878         print("      #5 clock = 1;", file=f)
 879         print("    end", file=f)
 880         print("  end", file=f)
 881         print("`endif", file=f)
 882
 883         print("  initial begin", file=f)
 884
 885         regs = sorted(smt.hiernets(vlogtb_topmod, regs_only=True))
 886         regvals = smt.get_net_bin_list(vlogtb_topmod, regs, vlogtb_state.replace("@@step_idx@@", str(steps_start)))
 887
 888         print("`ifndef VERILATOR", file=f)
 889         print("    #1;", file=f)
 890         print("`endif", file=f)
 891         for reg, val in zip(regs, regvals):
 892             hidden_net = False
 893             for n in reg:
 894                 if n.startswith("$"):
 895                     hidden_net = True
 896             print("    %sUUT.%s = %d'b%s;" % ("// " if hidden_net else "", ".".join(reg), len(val), val), file=f)
 897
 898         anyconsts = sorted(smt.hieranyconsts(vlogtb_topmod))
 899         for info in anyconsts:
 900             if info[3] is not None:
 901                 modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(steps_start)), info[0])
 902                 value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
 903                 print("    UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
 904
 905         mems = sorted(smt.hiermems(vlogtb_topmod))
 906         for mempath in mems:
 907             abits, width, rports, wports, asyncwr = smt.mem_info(vlogtb_topmod, mempath)
 908
 909             addr_expr_list = list()
 910             data_expr_list = list()
 911             for i in range(steps_start, steps_stop):
 912                 for j in range(rports):
 913                     addr_expr_list.append(smt.mem_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j))
 914                     data_expr_list.append(smt.mem_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j))
 915
 916             addr_list = smt.get_list(addr_expr_list)
 917             data_list = smt.get_list(data_expr_list)
 918
 919             addr_data = dict()
 920             for addr, data in zip(addr_list, data_list):
 921                 addr = smt.bv2bin(addr)
 922                 data = smt.bv2bin(data)
 923                 if addr not in addr_data:
 924                     addr_data[addr] = data
 925
 926             for addr, data in addr_data.items():
 927                 print("    UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath), len(addr), addr, len(data), data), file=f)
 928
 929         print("", file=f)
 930         anyseqs = sorted(smt.hieranyseqs(vlogtb_topmod))
 931
 932         for i in range(steps_start, steps_stop):
 933             pi_names = [[name] for name, _ in primary_inputs if name not in clock_inputs]
 934             pi_values = smt.get_net_bin_list(vlogtb_topmod, pi_names, vlogtb_state.replace("@@step_idx@@", str(i)))
 935
 936             print("    // state %d" % i, file=f)
 937
 938             if i > 0:
 939                 print("    if (cycle == %d) begin" % (i-1), file=f)
 940
 941             for name, val in zip(pi_names, pi_values):
 942                 if i > 0:
 943                     print("      PI_%s <= %d'b%s;" % (".".join(name), len(val), val), file=f)
 944                 else:
 945                     print("    PI_%s = %d'b%s;" % (".".join(name), len(val), val), file=f)
 946
 947             for info in anyseqs:
 948                 if info[3] is not None:
 949                     modstate = smt.net_expr(vlogtb_topmod, vlogtb_state.replace("@@step_idx@@", str(i)), info[0])
 950                     value = smt.bv2bin(smt.get("(|%s| %s)" % (info[1], modstate)))
 951                     if i > 0:
 952                         print("      UUT.%s <= %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
 953                     else:
 954                         print("    UUT.%s = %d'b%s;" % (".".join(info[0] + [info[3]]), len(value), value), file=f);
 955
 956             if i > 0:
 957                 print("    end", file=f)
 958                 print("", file=f)
 959
 960             if i == 0:
 961                 print("  end", file=f)
 962                 print("  always @(posedge clock) begin", file=f)
 963
 964         print("    genclock <= cycle < %d;" % (steps_stop-1), file=f)
 965         print("    cycle <= cycle + 1;", file=f)
 966         print("  end", file=f)
 967
 968         print("endmodule", file=f)
 969
 970
 971 def write_constr_trace(steps_start, steps_stop, index):
 972     filename = outconstr.replace("%", index)
 973     print_msg("Writing trace to constraints file: %s" % (filename))
 974
 975     constr_topmod = topmod
 976     constr_state = "s@@step_idx@@"
 977     constr_prefix = ""
 978
 979     if smtctop is not None:
 980         for item in smtctop[0].split("."):
 981             assert item in smt.modinfo[constr_topmod].cells
 982             constr_state = "(|%s_h %s| %s)" % (constr_topmod, item, constr_state)
 983             constr_topmod = smt.modinfo[constr_topmod].cells[item]
 984         if smtctop[1] != "":
 985             constr_prefix = smtctop[1] + "."
 986
 987     if smtcinit:
 988         steps_start = steps_stop - 1
 989
 990     with open(filename, "w") as f:
 991         primary_inputs = list()
 992
 993         for name in smt.modinfo[constr_topmod].inputs:
 994             width = smt.modinfo[constr_topmod].wsize[name]
 995             primary_inputs.append((name, width))
 996
 997         if steps_start == 0 or smtcinit:
 998             print("initial", file=f)
 999         else:
1000             print("state %d" % steps_start, file=f)
1001
1002         regnames = sorted(smt.hiernets(constr_topmod, regs_only=True))
1003         regvals = smt.get_net_list(constr_topmod, regnames, constr_state.replace("@@step_idx@@", str(steps_start)))
1004
1005         for name, val in zip(regnames, regvals):
1006             print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)
1007
1008         mems = sorted(smt.hiermems(constr_topmod))
1009         for mempath in mems:
1010             abits, width, rports, wports, asyncwr = smt.mem_info(constr_topmod, mempath)
1011
1012             addr_expr_list = list()
1013             data_expr_list = list()
1014             for i in range(steps_start, steps_stop):
1015                 for j in range(rports):
1016                     addr_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dA" % j))
1017                     data_expr_list.append(smt.mem_expr(constr_topmod, constr_state.replace("@@step_idx@@", str(i)), mempath, "R%dD" % j))
1018
1019             addr_list = smt.get_list(addr_expr_list)
1020             data_list = smt.get_list(data_expr_list)
1021
1022             addr_data = dict()
1023             for addr, data in zip(addr_list, data_list):
1024                 if addr not in addr_data:
1025                     addr_data[addr] = data
1026
1027             for addr, data in addr_data.items():
1028                 print("assume (= (select [%s%s] %s) %s)" % (constr_prefix, ".".join(mempath), addr, data), file=f)
1029
1030         for k in range(steps_start, steps_stop):
1031             if not smtcinit:
1032                 print("", file=f)
1033                 print("state %d" % k, file=f)
1034
1035             pi_names = [[name] for name, _ in sorted(primary_inputs)]
1036             pi_values = smt.get_net_list(constr_topmod, pi_names, constr_state.replace("@@step_idx@@", str(k)))
1037
1038             for name, val in zip(pi_names, pi_values):
1039                 print("assume (= [%s%s] %s)" % (constr_prefix, ".".join(name), val), file=f)
1040
1041
1042 def write_trace(steps_start, steps_stop, index):
1043     if vcdfile is not None:
1044         write_vcd_trace(steps_start, steps_stop, index)
1045
1046     if vlogtbfile is not None:
1047         write_vlogtb_trace(steps_start, steps_stop, index)
1048
1049     if outconstr is not None:
1050         write_constr_trace(steps_start, steps_stop, index)
1051
1052
1053 def print_failed_asserts_worker(mod, state, path, extrainfo):
1054     assert mod in smt.modinfo
1055     found_failed_assert = False
1056
1057     if smt.get("(|%s_a| %s)" % (mod, state)) in ["true", "#b1"]:
1058         return
1059
1060     for cellname, celltype in smt.modinfo[mod].cells.items():
1061         if print_failed_asserts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname, extrainfo):
1062             found_failed_assert = True
1063
1064     for assertfun, assertinfo in smt.modinfo[mod].asserts.items():
1065         if smt.get("(|%s| %s)" % (assertfun, state)) in ["false", "#b0"]:
1066             print_msg("Assert failed in %s: %s%s" % (path, assertinfo, extrainfo))
1067             found_failed_assert = True
1068
1069     return found_failed_assert
1070
1071
1072 def print_failed_asserts(state, final=False, extrainfo=""):
1073     if noinfo: return
1074     loc_list, expr_list, value_list = get_constr_expr(constr_asserts, state, final=final, getvalues=True)
1075     found_failed_assert = False
1076
1077     for loc, expr, value in zip(loc_list, expr_list, value_list):
1078         if smt.bv2int(value) == 0:
1079             print_msg("Assert %s failed: %s%s" % (loc, expr, extrainfo))
1080             found_failed_assert = True
1081
1082     if not final:
1083         if print_failed_asserts_worker(topmod, "s%d" % state, topmod, extrainfo):
1084             found_failed_assert = True
1085
1086     return found_failed_assert
1087
1088
1089 def print_anyconsts_worker(mod, state, path):
1090     assert mod in smt.modinfo
1091
1092     for cellname, celltype in smt.modinfo[mod].cells.items():
1093         print_anyconsts_worker(celltype, "(|%s_h %s| %s)" % (mod, cellname, state), path + "." + cellname)
1094
1095     for fun, info in smt.modinfo[mod].anyconsts.items():
1096         if info[1] is None:
1097             if not binarymode:
1098                 print_msg("Value for anyconst in %s (%s): %d" % (path, info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
1099             else:
1100                 print_msg("Value for anyconst in %s (%s): %s" % (path, info[0], smt.bv2bin(smt.get("(|%s| %s)" % (fun, state)))))
1101         else:
1102             if not binarymode:
1103                 print_msg("Value for anyconst %s.%s (%s): %d" % (path, info[1], info[0], smt.bv2int(smt.get("(|%s| %s)" % (fun, state)))))
1104             else:
1105                 print_msg("Value for anyconst %s.%s (%s): %s" % (path, info[1], info[0], smt.bv2bin(smt.get("(|%s| %s)" % (fun, state)))))
1106
1107
1108 def print_anyconsts(state):
1109     if noinfo: return
1110     print_anyconsts_worker(topmod, "s%d" % state, topmod)
1111
1112
1113 def get_cover_list(mod, base):
1114     assert mod in smt.modinfo
1115
1116     cover_expr = list()
1117     cover_desc = list()
1118
1119     for expr, desc in smt.modinfo[mod].covers.items():
1120         cover_expr.append("(ite (|%s| %s) #b1 #b0)" % (expr, base))
1121         cover_desc.append(desc)
1122
1123     for cell, submod in smt.modinfo[mod].cells.items():
1124         e, d = get_cover_list(submod, "(|%s_h %s| %s)" % (mod, cell, base))
1125         cover_expr += e
1126         cover_desc += d
1127
1128     return cover_expr, cover_desc
1129
1130 states = list()
1131 asserts_antecedent_cache = [list()]
1132 asserts_consequent_cache = [list()]
1133 asserts_cache_dirty = False
1134
1135 def smt_state(step):
1136     smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod))
1137     states.append("s%d" % step)
1138
1139 def smt_assert(expr):
1140     if expr == "true":
1141         return
1142
1143     smt.write("(assert %s)" % expr)
1144
1145 def smt_assert_antecedent(expr):
1146     if expr == "true":
1147         return
1148
1149     smt.write("(assert %s)" % expr)
1150
1151     global asserts_cache_dirty
1152     asserts_cache_dirty = True
1153     asserts_antecedent_cache[-1].append(expr)
1154
1155 def smt_assert_consequent(expr):
1156     if expr == "true":
1157         return
1158
1159     smt.write("(assert %s)" % expr)
1160
1161     global asserts_cache_dirty
1162     asserts_cache_dirty = True
1163     asserts_consequent_cache[-1].append(expr)
1164
1165 def smt_forall_assert():
1166     if not smt.forall:
1167         return
1168
1169     global asserts_cache_dirty
1170     asserts_cache_dirty = False
1171
1172     assert (len(smt.modinfo[topmod].maximize) + len(smt.modinfo[topmod].minimize) <= 1)
1173
1174     def make_assert_expr(asserts_cache):
1175         expr = list()
1176         for lst in asserts_cache:
1177             expr += lst
1178
1179         assert len(expr) != 0
1180
1181         if len(expr) == 1:
1182             expr = expr[0]
1183         else:
1184             expr = "(and %s)" % (" ".join(expr))
1185         return expr
1186
1187     antecedent_expr = make_assert_expr(asserts_antecedent_cache)
1188     consequent_expr = make_assert_expr(asserts_consequent_cache)
1189
1190     states_db = set(states)
1191     used_states_db = set()
1192     new_antecedent_expr = list()
1193     new_consequent_expr = list()
1194     assert_expr = list()
1195
1196     def make_new_expr(new_expr, expr):
1197         cursor = 0
1198         while cursor < len(expr):
1199             l = 1
1200             if expr[cursor] in '|"':
1201                 while cursor+l+1 < len(expr) and expr[cursor] != expr[cursor+l]:
1202                     l += 1
1203                 l += 1
1204             elif expr[cursor] not in '() ':
1205                 while cursor+l < len(expr) and expr[cursor+l] not in '|"() ':
1206                     l += 1
1207
1208             word = expr[cursor:cursor+l]
1209             if word in states_db:
1210                 used_states_db.add(word)
1211                 word += "_"
1212
1213             new_expr.append(word)
1214             cursor += l
1215
1216     make_new_expr(new_antecedent_expr, antecedent_expr)
1217     make_new_expr(new_consequent_expr, consequent_expr)
1218
1219     new_antecedent_expr = ["".join(new_antecedent_expr)]
1220     new_consequent_expr = ["".join(new_consequent_expr)]
1221
1222     if states[0] in used_states_db:
1223         new_antecedent_expr.append("(|%s_ex_state_eq| %s %s_)" % (topmod, states[0], states[0]))
1224     for s in states:
1225         if s in used_states_db:
1226             new_antecedent_expr.append("(|%s_ex_input_eq| %s %s_)" % (topmod, s, s))
1227
1228     if len(new_antecedent_expr) == 0:
1229         new_antecedent_expr = "true"
1230     elif len(new_antecedent_expr) == 1:
1231         new_antecedent_expr = new_antecedent_expr[0]
1232     else:
1233         new_antecedent_expr = "(and %s)" % (" ".join(new_antecedent_expr))
1234
1235     if len(new_consequent_expr) == 0:
1236         new_consequent_expr = "true"
1237     elif len(new_consequent_expr) == 1:
1238         new_consequent_expr = new_consequent_expr[0]
1239     else:
1240         new_consequent_expr = "(and %s)" % (" ".join(new_consequent_expr))
1241
1242     assert_expr.append("(assert (forall (")
1243     first_state = True
1244     for s in states:
1245         if s in used_states_db:
1246             assert_expr.append("%s(%s_ |%s_s|)" % ("" if first_state else " ", s, topmod))
1247             first_state = False
1248     assert_expr.append(") (=> %s %s)))" % (new_antecedent_expr, new_consequent_expr))
1249
1250     smt.write("".join(assert_expr))
1251
1252     if len(smt.modinfo[topmod].maximize) > 0:
1253         for s in states:
1254             if s in used_states_db:
1255                 smt.write("(maximize (|%s| %s))\n" % (smt.modinfo[topmod].maximize.copy().pop(), s))
1256                 break
1257
1258     if len(smt.modinfo[topmod].minimize) > 0:
1259         for s in states:
1260             if s in used_states_db:
1261                 smt.write("(minimize (|%s| %s))\n" % (smt.modinfo[topmod].minimize.copy().pop(), s))
1262                 break
1263
1264 def smt_push():
1265     global asserts_cache_dirty
1266     asserts_cache_dirty = True
1267     asserts_antecedent_cache.append(list())
1268     asserts_consequent_cache.append(list())
1269     smt.write("(push 1)")
1270
1271 def smt_pop():
1272     global asserts_cache_dirty
1273     asserts_cache_dirty = True
1274     asserts_antecedent_cache.pop()
1275     asserts_consequent_cache.pop()
1276     smt.write("(pop 1)")
1277
1278 def smt_check_sat():
1279     if asserts_cache_dirty:
1280         smt_forall_assert()
1281     return smt.check_sat()
1282
1283 if tempind:
1284     retstatus = "FAILED"
1285     skip_counter = step_size
1286     for step in range(num_steps, -1, -1):
1287         if smt.forall:
1288             print_msg("Temporal induction not supported for exists-forall problems.")
1289             break
1290
1291         smt_state(step)
1292         smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
1293         smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
1294         smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1295         smt_assert_consequent(get_constr_expr(constr_assumes, step))
1296
1297         if step == num_steps:
1298             smt_assert("(not (and (|%s_a| s%d) %s))" % (topmod, step, get_constr_expr(constr_asserts, step)))
1299
1300         else:
1301             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step, step+1))
1302             smt_assert("(|%s_a| s%d)" % (topmod, step))
1303             smt_assert(get_constr_expr(constr_asserts, step))
1304
1305         if step > num_steps-skip_steps:
1306             print_msg("Skipping induction in step %d.." % (step))
1307             continue
1308
1309         skip_counter += 1
1310         if skip_counter < step_size:
1311             print_msg("Skipping induction in step %d.." % (step))
1312             continue
1313
1314         skip_counter = 0
1315         print_msg("Trying induction in step %d.." % (step))
1316
1317         if smt_check_sat() == "sat":
1318             if step == 0:
1319                 print_msg("Temporal induction failed!")
1320                 print_anyconsts(num_steps)
1321                 print_failed_asserts(num_steps)
1322                 write_trace(step, num_steps+1, '%')
1323
1324             elif dumpall:
1325                 print_anyconsts(num_steps)
1326                 print_failed_asserts(num_steps)
1327                 write_trace(step, num_steps+1, "%d" % step)
1328
1329         else:
1330             print_msg("Temporal induction successful.")
1331             retstatus = "PASSED"
1332             break
1333
1334 elif covermode:
1335     cover_expr, cover_desc = get_cover_list(topmod, "state")
1336     cover_mask = "1" * len(cover_desc)
1337
1338     if len(cover_expr) > 1:
1339         cover_expr = "(concat %s)" % " ".join(cover_expr)
1340     elif len(cover_expr) == 1:
1341         cover_expr = cover_expr[0]
1342     else:
1343         cover_expr = "#b0"
1344
1345     coveridx = 0
1346     smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr))
1347
1348     step = 0
1349     retstatus = "FAILED"
1350     found_failed_assert = False
1351
1352     assert step_size == 1
1353
1354     while step < num_steps:
1355         smt_state(step)
1356         smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
1357         smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
1358         smt_assert_consequent(get_constr_expr(constr_assumes, step))
1359
1360         if step == 0:
1361             if noinit:
1362                 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1363             else:
1364                 smt_assert_antecedent("(|%s_i| s0)" % (topmod))
1365                 smt_assert_antecedent("(|%s_is| s0)" % (topmod))
1366
1367         else:
1368             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step))
1369             smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1370
1371         while "1" in cover_mask:
1372             print_msg("Checking cover reachability in step %d.." % (step))
1373             smt_push()
1374             smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx, step, "0" * len(cover_desc)))
1375
1376             if smt_check_sat() == "unsat":
1377                 smt_pop()
1378                 break
1379
1380             if append_steps > 0:
1381                 for i in range(step+1, step+1+append_steps):
1382                     print_msg("Appending additional step %d." % i)
1383                     smt_state(i)
1384                     smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
1385                     smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
1386                     smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
1387                     smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
1388                     smt_assert_consequent(get_constr_expr(constr_assumes, i))
1389                 print_msg("Re-solving with appended steps..")
1390                 if smt_check_sat() == "unsat":
1391                     print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
1392                     found_failed_assert = True
1393                     retstatus = "FAILED"
1394                     break
1395
1396             reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
1397             assert len(reached_covers) == len(cover_desc)
1398
1399             new_cover_mask = []
1400
1401             for i in range(len(reached_covers)):
1402                 if reached_covers[i] == "0":
1403                     new_cover_mask.append(cover_mask[i])
1404                     continue
1405
1406                 print_msg("Reached cover statement at %s in step %d." % (cover_desc[i], step))
1407                 new_cover_mask.append("0")
1408
1409             cover_mask = "".join(new_cover_mask)
1410
1411             for i in range(step+1+append_steps):
1412                 if print_failed_asserts(i, extrainfo=" (step %d)" % i):
1413                     found_failed_assert = True
1414
1415             write_trace(0, step+1+append_steps, "%d" % coveridx)
1416
1417             if found_failed_assert:
1418                 break
1419
1420             coveridx += 1
1421             smt_pop()
1422             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))
1423
1424         if found_failed_assert:
1425             break
1426
1427         if "1" not in cover_mask:
1428             retstatus = "PASSED"
1429             break
1430
1431         step += 1
1432
1433     if "1" in cover_mask:
1434         for i in range(len(cover_mask)):
1435             if cover_mask[i] == "1":
1436                 print_msg("Unreached cover statement at %s." % cover_desc[i])
1437
1438 else:  # not tempind, covermode
1439     step = 0
1440     retstatus = "PASSED"
1441     while step < num_steps:
1442         smt_state(step)
1443         smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
1444         smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
1445         smt_assert_consequent(get_constr_expr(constr_assumes, step))
1446
1447         if step == 0:
1448             if noinit:
1449                 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1450             else:
1451                 smt_assert_antecedent("(|%s_i| s0)" % (topmod))
1452                 smt_assert_antecedent("(|%s_is| s0)" % (topmod))
1453
1454         else:
1455             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step))
1456             smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1457
1458         if step < skip_steps:
1459             if assume_skipped is not None and step >= assume_skipped:
1460                 print_msg("Skipping step %d (and assuming pass).." % (step))
1461                 smt_assert("(|%s_a| s%d)" % (topmod, step))
1462                 smt_assert(get_constr_expr(constr_asserts, step))
1463             else:
1464                 print_msg("Skipping step %d.." % (step))
1465             step += 1
1466             continue
1467
1468         last_check_step = step
1469         for i in range(1, step_size):
1470             if step+i < num_steps:
1471                 smt_state(step+i)
1472                 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step+i))
1473                 smt_assert_consequent("(|%s_u| s%d)" % (topmod, step+i))
1474                 smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step+i))
1475                 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step+i-1, step+i))
1476                 smt_assert_consequent(get_constr_expr(constr_assumes, step+i))
1477                 last_check_step = step+i
1478
1479         if not gentrace:
1480             if presat:
1481                 if last_check_step == step:
1482                     print_msg("Checking assumptions in step %d.." % (step))
1483                 else:
1484                     print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step))
1485
1486                 if smt_check_sat() == "unsat":
1487                     print("%s Assumptions are unsatisfiable!" % smt.timestamp())
1488                     retstatus = "PREUNSAT"
1489                     break
1490
1491             if not final_only:
1492                 if last_check_step == step:
1493                     print_msg("Checking assertions in step %d.." % (step))
1494                 else:
1495                     print_msg("Checking assertions in steps %d to %d.." % (step, last_check_step))
1496                 smt_push()
1497
1498                 smt_assert("(not (and %s))" % " ".join(["(|%s_a| s%d)" % (topmod, i) for i in range(step, last_check_step+1)] +
1499                         [get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)]))
1500
1501                 if smt_check_sat() == "sat":
1502                     print("%s BMC failed!" % smt.timestamp())
1503                     if append_steps > 0:
1504                         for i in range(last_check_step+1, last_check_step+1+append_steps):
1505                             print_msg("Appending additional step %d." % i)
1506                             smt_state(i)
1507                             smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
1508                             smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
1509                             smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
1510                             smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
1511                             smt_assert_consequent(get_constr_expr(constr_assumes, i))
1512                         print_msg("Re-solving with appended steps..")
1513                         if smt_check_sat() == "unsat":
1514                             print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
1515                             retstatus = "FAILED"
1516                             break
1517                     print_anyconsts(step)
1518                     for i in range(step, last_check_step+1):
1519                         print_failed_asserts(i)
1520                     write_trace(0, last_check_step+1+append_steps, '%')
1521                     retstatus = "FAILED"
1522                     break
1523
1524                 smt_pop()
1525
1526             if (constr_final_start is not None) or (last_check_step+1 != num_steps):
1527                 for i in range(step, last_check_step+1):
1528                     smt_assert("(|%s_a| s%d)" % (topmod, i))
1529                     smt_assert(get_constr_expr(constr_asserts, i))
1530
1531             if constr_final_start is not None:
1532                 for i in range(step, last_check_step+1):
1533                     if i < constr_final_start:
1534                         continue
1535
1536                     print_msg("Checking final constraints in step %d.." % (i))
1537                     smt_push()
1538
1539                     smt_assert_consequent(get_constr_expr(constr_assumes, i, final=True))
1540                     smt_assert("(not %s)" % get_constr_expr(constr_asserts, i, final=True))
1541
1542                     if smt_check_sat() == "sat":
1543                         print("%s BMC failed!" % smt.timestamp())
1544                         print_anyconsts(i)
1545                         print_failed_asserts(i, final=True)
1546                         write_trace(0, i+1, '%')
1547                         retstatus = "FAILED"
1548                         break
1549
1550                     smt_pop()
1551                 if not retstatus:
1552                     break
1553
1554         else:  # gentrace
1555             for i in range(step, last_check_step+1):
1556                 smt_assert("(|%s_a| s%d)" % (topmod, i))
1557                 smt_assert(get_constr_expr(constr_asserts, i))
1558
1559             print_msg("Solving for step %d.." % (last_check_step))
1560             if smt_check_sat() != "sat":
1561                 print("%s No solution found!" % smt.timestamp())
1562                 retstatus = "FAILED"
1563                 break
1564
1565             elif dumpall:
1566                 print_anyconsts(0)
1567                 write_trace(0, last_check_step+1, "%d" % step)
1568
1569         step += step_size
1570
1571     if gentrace and retstatus:
1572         print_anyconsts(0)
1573         write_trace(0, num_steps, '%')
1574
1575
1576 smt.write("(exit)")
1577 smt.wait()
1578
1579 print_msg("Status: %s" % retstatus)
1580 sys.exit(0 if retstatus == "PASSED" else 1)