projects / yosys.git / blob
? search:


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