projects / yosys.git / blob
? search:


3d6d3e1b39d93217e543c51c71ded4a83eac2616
[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 def make_assert_expr(asserts_cache):
1162 expr = list()
1163 for lst in asserts_cache:
1164 expr += lst
1165
1166 assert len(expr) != 0
1167
1168 if len(expr) == 1:
1169 expr = expr[0]
1170 else:
1171 expr = "(and %s)" % (" ".join(expr))
1172 return expr
1173
1174 antecedent_expr = make_assert_expr(asserts_antecedent_cache)
1175 consequent_expr = make_assert_expr(asserts_consequent_cache)
1176
1177 states_db = set(states)
1178 used_states_db = set()
1179 new_antecedent_expr = list()
1180 new_consequent_expr = list()
1181 assert_expr = list()
1182
1183 def make_new_expr(new_expr, expr):
1184 cursor = 0
1185 while cursor < len(expr):
1186 l = 1
1187 if expr[cursor] in '|"':
1188 while cursor+l+1 < len(expr) and expr[cursor] != expr[cursor+l]:
1189 l += 1
1190 l += 1
1191 elif expr[cursor] not in '() ':
1192 while cursor+l < len(expr) and expr[cursor+l] not in '|"() ':
1193 l += 1
1194
1195 word = expr[cursor:cursor+l]
1196 if word in states_db:
1197 used_states_db.add(word)
1198 word += "_"
1199
1200 new_expr.append(word)
1201 cursor += l
1202
1203 make_new_expr(new_antecedent_expr, antecedent_expr)
1204 make_new_expr(new_consequent_expr, consequent_expr)
1205
1206 new_antecedent_expr = ["".join(new_antecedent_expr)]
1207 new_consequent_expr = ["".join(new_consequent_expr)]
1208
1209 if states[0] in used_states_db:
1210 new_antecedent_expr.append("(|%s_ex_state_eq| %s %s_)" % (topmod, states[0], states[0]))
1211 for s in states:
1212 if s in used_states_db:
1213 new_antecedent_expr.append("(|%s_ex_input_eq| %s %s_)" % (topmod, s, s))
1214
1215 if len(new_antecedent_expr) == 0:
1216 new_antecedent_expr = "true"
1217 elif len(new_antecedent_expr) == 1:
1218 new_antecedent_expr = new_antecedent_expr[0]
1219 else:
1220 new_antecedent_expr = "(and %s)" % (" ".join(new_antecedent_expr))
1221
1222 if len(new_consequent_expr) == 0:
1223 new_consequent_expr = "true"
1224 elif len(new_consequent_expr) == 1:
1225 new_consequent_expr = new_consequent_expr[0]
1226 else:
1227 new_consequent_expr = "(and %s)" % (" ".join(new_consequent_expr))
1228
1229 assert_expr.append("(assert (forall (")
1230 first_state = True
1231 for s in states:
1232 if s in used_states_db:
1233 assert_expr.append("%s(%s_ |%s_s|)" % ("" if first_state else " ", s, topmod))
1234 first_state = False
1235 assert_expr.append(") (=> %s %s)))" % (new_antecedent_expr, new_consequent_expr))
1236
1237 smt.write("".join(assert_expr))
1238
1239 def smt_push():
1240 global asserts_cache_dirty
1241 asserts_cache_dirty = True
1242 asserts_antecedent_cache.append(list())
1243 asserts_consequent_cache.append(list())
1244 smt.write("(push 1)")
1245
1246 def smt_pop():
1247 global asserts_cache_dirty
1248 asserts_cache_dirty = True
1249 asserts_antecedent_cache.pop()
1250 asserts_consequent_cache.pop()
1251 smt.write("(pop 1)")
1252
1253 def smt_check_sat():
1254 if asserts_cache_dirty:
1255 smt_forall_assert()
1256 return smt.check_sat()
1257
1258 if tempind:
1259 retstatus = "FAILED"
1260 skip_counter = step_size
1261 for step in range(num_steps, -1, -1):
1262 if smt.forall:
1263 print_msg("Temporal induction not supported for exists-forall problems.")
1264 break
1265
1266 smt_state(step)
1267 smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
1268 smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
1269 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1270 smt_assert_consequent(get_constr_expr(constr_assumes, step))
1271
1272 if step == num_steps:
1273 smt_assert("(not (and (|%s_a| s%d) %s))" % (topmod, step, get_constr_expr(constr_asserts, step)))
1274
1275 else:
1276 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step, step+1))
1277 smt_assert("(|%s_a| s%d)" % (topmod, step))
1278 smt_assert(get_constr_expr(constr_asserts, step))
1279
1280 if step > num_steps-skip_steps:
1281 print_msg("Skipping induction in step %d.." % (step))
1282 continue
1283
1284 skip_counter += 1
1285 if skip_counter < step_size:
1286 print_msg("Skipping induction in step %d.." % (step))
1287 continue
1288
1289 skip_counter = 0
1290 print_msg("Trying induction in step %d.." % (step))
1291
1292 if smt_check_sat() == "sat":
1293 if step == 0:
1294 print_msg("Temporal induction failed!")
1295 print_anyconsts(num_steps)
1296 print_failed_asserts(num_steps)
1297 write_trace(step, num_steps+1, '%')
1298
1299 elif dumpall:
1300 print_anyconsts(num_steps)
1301 print_failed_asserts(num_steps)
1302 write_trace(step, num_steps+1, "%d" % step)
1303
1304 else:
1305 print_msg("Temporal induction successful.")
1306 retstatus = "PASSED"
1307 break
1308
1309 elif covermode:
1310 cover_expr, cover_desc = get_cover_list(topmod, "state")
1311 cover_mask = "1" * len(cover_desc)
1312
1313 if len(cover_expr) > 1:
1314 cover_expr = "(concat %s)" % " ".join(cover_expr)
1315 elif len(cover_expr) == 1:
1316 cover_expr = cover_expr[0]
1317 else:
1318 cover_expr = "#b0"
1319
1320 coveridx = 0
1321 smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr))
1322
1323 step = 0
1324 retstatus = "FAILED"
1325 found_failed_assert = False
1326
1327 assert step_size == 1
1328
1329 while step < num_steps:
1330 smt_state(step)
1331 smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
1332 smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
1333 smt_assert_consequent(get_constr_expr(constr_assumes, step))
1334
1335 if step == 0:
1336 if noinit:
1337 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1338 else:
1339 smt_assert_antecedent("(|%s_i| s0)" % (topmod))
1340 smt_assert_antecedent("(|%s_is| s0)" % (topmod))
1341
1342 else:
1343 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step))
1344 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1345
1346 while "1" in cover_mask:
1347 print_msg("Checking cover reachability in step %d.." % (step))
1348 smt_push()
1349 smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx, step, "0" * len(cover_desc)))
1350
1351 if smt_check_sat() == "unsat":
1352 smt_pop()
1353 break
1354
1355 if append_steps > 0:
1356 for i in range(step+1, step+1+append_steps):
1357 print_msg("Appending additional step %d." % i)
1358 smt_state(i)
1359 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
1360 smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
1361 smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
1362 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
1363 smt_assert_consequent(get_constr_expr(constr_assumes, i))
1364 print_msg("Re-solving with appended steps..")
1365 if smt_check_sat() == "unsat":
1366 print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
1367 found_failed_assert = True
1368 retstatus = "FAILED"
1369 break
1370
1371 reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
1372 assert len(reached_covers) == len(cover_desc)
1373
1374 new_cover_mask = []
1375
1376 for i in range(len(reached_covers)):
1377 if reached_covers[i] == "0":
1378 new_cover_mask.append(cover_mask[i])
1379 continue
1380
1381 print_msg("Reached cover statement at %s in step %d." % (cover_desc[i], step))
1382 new_cover_mask.append("0")
1383
1384 cover_mask = "".join(new_cover_mask)
1385
1386 for i in range(step+1+append_steps):
1387 if print_failed_asserts(i, extrainfo=" (step %d)" % i):
1388 found_failed_assert = True
1389
1390 write_trace(0, step+1+append_steps, "%d" % coveridx)
1391
1392 if found_failed_assert:
1393 break
1394
1395 coveridx += 1
1396 smt_pop()
1397 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))
1398
1399 if found_failed_assert:
1400 break
1401
1402 if "1" not in cover_mask:
1403 retstatus = "PASSED"
1404 break
1405
1406 step += 1
1407
1408 if "1" in cover_mask:
1409 for i in range(len(cover_mask)):
1410 if cover_mask[i] == "1":
1411 print_msg("Unreached cover statement at %s." % cover_desc[i])
1412
1413 else: # not tempind, covermode
1414 step = 0
1415 retstatus = "PASSED"
1416 while step < num_steps:
1417 smt_state(step)
1418 smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
1419 smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step))
1420 smt_assert_consequent(get_constr_expr(constr_assumes, step))
1421
1422 if step == 0:
1423 if noinit:
1424 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1425 else:
1426 smt_assert_antecedent("(|%s_i| s0)" % (topmod))
1427 smt_assert_antecedent("(|%s_is| s0)" % (topmod))
1428
1429 else:
1430 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step-1, step))
1431 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step))
1432
1433 if step < skip_steps:
1434 if assume_skipped is not None and step >= assume_skipped:
1435 print_msg("Skipping step %d (and assuming pass).." % (step))
1436 smt_assert("(|%s_a| s%d)" % (topmod, step))
1437 smt_assert(get_constr_expr(constr_asserts, step))
1438 else:
1439 print_msg("Skipping step %d.." % (step))
1440 step += 1
1441 continue
1442
1443 last_check_step = step
1444 for i in range(1, step_size):
1445 if step+i < num_steps:
1446 smt_state(step+i)
1447 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, step+i))
1448 smt_assert_consequent("(|%s_u| s%d)" % (topmod, step+i))
1449 smt_assert_antecedent("(|%s_h| s%d)" % (topmod, step+i))
1450 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, step+i-1, step+i))
1451 smt_assert_consequent(get_constr_expr(constr_assumes, step+i))
1452 last_check_step = step+i
1453
1454 if not gentrace:
1455 if presat:
1456 if last_check_step == step:
1457 print_msg("Checking assumptions in step %d.." % (step))
1458 else:
1459 print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step))
1460
1461 if smt_check_sat() == "unsat":
1462 print("%s Assumptions are unsatisfiable!" % smt.timestamp())
1463 retstatus = "PREUNSAT"
1464 break
1465
1466 if not final_only:
1467 if last_check_step == step:
1468 print_msg("Checking assertions in step %d.." % (step))
1469 else:
1470 print_msg("Checking assertions in steps %d to %d.." % (step, last_check_step))
1471 smt_push()
1472
1473 smt_assert("(not (and %s))" % " ".join(["(|%s_a| s%d)" % (topmod, i) for i in range(step, last_check_step+1)] +
1474 [get_constr_expr(constr_asserts, i) for i in range(step, last_check_step+1)]))
1475
1476 if smt_check_sat() == "sat":
1477 print("%s BMC failed!" % smt.timestamp())
1478 if append_steps > 0:
1479 for i in range(last_check_step+1, last_check_step+1+append_steps):
1480 print_msg("Appending additional step %d." % i)
1481 smt_state(i)
1482 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod, i))
1483 smt_assert_consequent("(|%s_u| s%d)" % (topmod, i))
1484 smt_assert_antecedent("(|%s_h| s%d)" % (topmod, i))
1485 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod, i-1, i))
1486 smt_assert_consequent(get_constr_expr(constr_assumes, i))
1487 print_msg("Re-solving with appended steps..")
1488 if smt_check_sat() == "unsat":
1489 print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
1490 retstatus = "FAILED"
1491 break
1492 print_anyconsts(step)
1493 for i in range(step, last_check_step+1):
1494 print_failed_asserts(i)
1495 write_trace(0, last_check_step+1+append_steps, '%')
1496 retstatus = "FAILED"
1497 break
1498
1499 smt_pop()
1500
1501 if (constr_final_start is not None) or (last_check_step+1 != num_steps):
1502 for i in range(step, last_check_step+1):
1503 smt_assert("(|%s_a| s%d)" % (topmod, i))
1504 smt_assert(get_constr_expr(constr_asserts, i))
1505
1506 if constr_final_start is not None:
1507 for i in range(step, last_check_step+1):
1508 if i < constr_final_start:
1509 continue
1510
1511 print_msg("Checking final constraints in step %d.." % (i))
1512 smt_push()
1513
1514 smt_assert_consequent(get_constr_expr(constr_assumes, i, final=True))
1515 smt_assert("(not %s)" % get_constr_expr(constr_asserts, i, final=True))
1516
1517 if smt_check_sat() == "sat":
1518 print("%s BMC failed!" % smt.timestamp())
1519 print_anyconsts(i)
1520 print_failed_asserts(i, final=True)
1521 write_trace(0, i+1, '%')
1522 retstatus = "FAILED"
1523 break
1524
1525 smt_pop()
1526 if not retstatus:
1527 break
1528
1529 else: # gentrace
1530 for i in range(step, last_check_step+1):
1531 smt_assert("(|%s_a| s%d)" % (topmod, i))
1532 smt_assert(get_constr_expr(constr_asserts, i))
1533
1534 print_msg("Solving for step %d.." % (last_check_step))
1535 if smt_check_sat() != "sat":
1536 print("%s No solution found!" % smt.timestamp())
1537 retstatus = "FAILED"
1538 break
1539
1540 elif dumpall:
1541 print_anyconsts(0)
1542 write_trace(0, last_check_step+1, "%d" % step)
1543
1544 step += step_size
1545
1546 if gentrace and retstatus:
1547 print_anyconsts(0)
1548 write_trace(0, num_steps, '%')
1549
1550
1551 smt.write("(exit)")
1552 smt.wait()
1553
1554 print_msg("Status: %s" % retstatus)
1555 sys.exit(0 if retstatus == "PASSED" else 1)