1#!/usr/local/bin/python3.8 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 20import os, sys, getopt, re 21##yosys-sys-path## 22from smtio import SmtIo, SmtOpts, MkVcd 23from collections import defaultdict 24 25got_topt = False 26skip_steps = 0 27step_size = 1 28num_steps = 20 29append_steps = 0 30vcdfile = None 31cexfile = None 32aimfile = None 33aiwfile = None 34aigheader = True 35btorwitfile = None 36vlogtbfile = None 37vlogtbtop = None 38inconstr = list() 39outconstr = None 40gentrace = False 41covermode = False 42tempind = False 43dumpall = False 44assume_skipped = None 45final_only = False 46topmod = None 47noinfo = False 48presat = False 49smtcinit = False 50smtctop = None 51noinit = False 52binarymode = False 53so = SmtOpts() 54 55 56def 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 160try: 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"]) 165except: 166 usage() 167 168for 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 242if len(args) != 1: 243 usage() 244 245if sum([tempind, gentrace, covermode]) > 1: 246 usage() 247 248constr_final_start = None 249constr_asserts = defaultdict(list) 250constr_assumes = defaultdict(list) 251constr_write = list() 252 253for 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 344def 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 390smt = SmtIo(opts=so) 391 392if noinfo and vcdfile is None and vlogtbfile is None and outconstr is None: 393 smt.produce_models = False 394 395def print_msg(msg): 396 print("%s %s" % (smt.timestamp(), msg)) 397 sys.stdout.flush() 398 399print_msg("Solver: %s" % (so.solver)) 400 401with open(args[0], "r") as f: 402 for line in f: 403 smt.write(line) 404 405for line in constr_write: 406 smt.write(line) 407 408if topmod is None: 409 topmod = smt.topmod 410 411assert topmod is not None 412assert topmod in smt.modinfo 413 414if 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 455if 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 589if 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 686def 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 820def 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 828def 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 839def 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 989def 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 1060def 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 1071def 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 1090def 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 1107def 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 1126def print_anyconsts(state): 1127 if noinfo: return 1128 print_anyconsts_worker(topmod, "s%d" % state, topmod) 1129 1130 1131def 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 1148states = list() 1149asserts_antecedent_cache = [list()] 1150asserts_consequent_cache = [list()] 1151asserts_cache_dirty = False 1152 1153def smt_state(step): 1154 smt.write("(declare-fun s%d () |%s_s|)" % (step, topmod)) 1155 states.append("s%d" % step) 1156 1157def smt_assert(expr): 1158 if expr == "true": 1159 return 1160 1161 smt.write("(assert %s)" % expr) 1162 1163def 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 1173def 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 1183def 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 1282def 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 1289def 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 1296def smt_check_sat(expected=["sat", "unsat"]): 1297 if asserts_cache_dirty: 1298 smt_forall_assert() 1299 return smt.check_sat(expected=expected) 1300 1301if 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 1352elif 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 1456else: # 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 1595smt.write("(exit)") 1596smt.wait() 1597 1598print_msg("Status: %s" % retstatus) 1599sys.exit(0 if retstatus == "PASSED" else 1) 1600