3 # yosys -- Yosys Open SYnthesis Suite
5 # Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
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.
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.
20 import os
, sys
, getopt
, re
22 from smtio
import SmtIo
, SmtOpts
, MkVcd
23 from collections
import defaultdict
56 yosys-smtbmc [options] <yosys_smt2_output>
59 -t <skip_steps>:<num_steps>
60 -t <skip_steps>:<step_size>:<num_steps>
61 default: skip_steps=0, step_size=1, num_steps=20
64 generate an arbitrary trace that satisfies
65 all assertions and assumptions.
68 instead of BMC run temporal induction
71 instead of regular BMC run cover analysis
74 name of the top module
76 --smtc <constr_filename>
80 read cex file as written by ABC's "write_cex -n"
83 read AIGER map file (as written by Yosys' "write_aiger -map")
84 and AIGER witness file. The file names are <prefix>.aim for
85 the map file and <prefix>.aiw for the witness file.
87 --aig <aim_filename>:<aiw_filename>
88 like above, but for map files and witness files that do not
89 share a filename prefix (or use differen file extensions).
92 the AIGER witness file does not include the status and
96 only run the core proof, do not collect and print any
97 additional information (e.g. which assert failed)
100 check if the design with assumptions but without assertions
101 is SAT before checking if assertions are UNSAT. This will
102 detect if there are contradicting assumtions. In some cases
103 this will also help to "warmup" the solver, potentially
107 only check final constraints, assume base case
109 --assume-skipped <start_step>
110 assume asserts in skipped steps in BMC.
111 no assumptions are created for skipped steps
114 --dump-vcd <vcd_filename>
115 write trace to this VCD file
116 (hint: use 'write_smt2 -wires' for maximum
117 coverage of signals in generated VCD file)
119 --dump-vlogtb <verilog_filename>
120 write trace as Verilog test bench
122 --vlogtb-top <hierarchical_name>
123 use the given entity as top module for the generated
124 Verilog test bench. The <hierarchical_name> is relative
125 to the design top module without the top module name.
127 --dump-smtc <constr_filename>
128 write trace as constraints file
131 write just the last state as initial constraint to smtc file
133 --smtc-top <old>[:<new>]
134 replace <old> with <new> in constraints dumped to smtc
135 file and only dump object below <old> in design hierarchy.
138 do not assume initial conditions in state 0
141 when using -g or -i, create a dump file for each
142 step. The character '%' is replaces in all dump
143 filenames with the step number.
146 add <num_steps> time steps at the end of the trace
147 when creating a counter example (this additional time
148 steps will still be constrained by assumtions)
154 opts
, args
= getopt
.getopt(sys
.argv
[1:], so
.shortopts
+ "t:igcm:", so
.longopts
+
155 ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "presat",
156 "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
157 "smtc-init", "smtc-top=", "noinit"])
166 num_steps
= int(a
[0])
168 skip_steps
= int(a
[0])
169 num_steps
= int(a
[1])
171 skip_steps
= int(a
[0])
172 step_size
= int(a
[1])
173 num_steps
= int(a
[2])
176 elif o
== "--assume-skipped":
177 assume_skipped
= int(a
)
178 elif o
== "--final-only":
186 aimfile
, aiwfile
= a
.split(":")
190 elif o
== "--aig-noheader":
192 elif o
== "--dump-vcd":
194 elif o
== "--dump-vlogtb":
196 elif o
== "--vlogtb-top":
198 elif o
== "--dump-smtc":
200 elif o
== "--smtc-init":
202 elif o
== "--smtc-top":
203 smtctop
= a
.split(":")
204 if len(smtctop
) == 1:
206 assert len(smtctop
) == 2
207 smtctop
= tuple(smtctop
)
208 elif o
== "--dump-all":
210 elif o
== "--presat":
212 elif o
== "--noinfo":
214 elif o
== "--noinit":
216 elif o
== "--append":
217 append_steps
= int(a
)
226 elif so
.handle(o
, a
):
234 if sum([tempind
, gentrace
, covermode
]) > 1:
237 constr_final_start
= None
238 constr_asserts
= defaultdict(list)
239 constr_assumes
= defaultdict(list)
240 constr_write
= list()
243 current_states
= None
246 with
open(fn
, "r") as f
:
250 if line
.startswith("#"):
253 tokens
= line
.split()
258 if tokens
[0] == "initial":
259 current_states
= set()
261 current_states
.add(0)
264 if tokens
[0] == "final":
267 current_states
= set(["final-%d" % i
for i
in range(0, num_steps
+1)])
268 constr_final_start
= 0
269 elif len(tokens
) == 2:
270 arg
= abs(int(tokens
[1]))
271 current_states
= set(["final-%d" % i
for i
in range(arg
, num_steps
+1)])
272 constr_final_start
= arg
if constr_final_start
is None else min(constr_final_start
, arg
)
277 if tokens
[0] == "state":
278 current_states
= set()
280 for token
in tokens
[1:]:
281 tok
= token
.split(":")
283 current_states
.add(int(token
))
290 for i
in range(lower
, upper
+1):
291 current_states
.add(i
)
296 if tokens
[0] == "always":
298 current_states
= set(range(0, num_steps
+1))
299 elif len(tokens
) == 2:
300 arg
= abs(int(tokens
[1]))
301 current_states
= set(range(arg
, num_steps
+1))
306 if tokens
[0] == "assert":
307 assert current_states
is not None
309 for state
in current_states
:
310 constr_asserts
[state
].append(("%s:%d" % (fn
, current_line
), " ".join(tokens
[1:])))
314 if tokens
[0] == "assume":
315 assert current_states
is not None
317 for state
in current_states
:
318 constr_assumes
[state
].append(("%s:%d" % (fn
, current_line
), " ".join(tokens
[1:])))
322 if tokens
[0] == "write":
323 constr_write
.append(" ".join(tokens
[1:]))
326 if tokens
[0] == "logic":
327 so
.logic
= " ".join(tokens
[1:])
333 def get_constr_expr(db
, state
, final
=False, getvalues
=False):
335 if ("final-%d" % state
) not in db
:
336 return ([], [], []) if getvalues
else "true"
339 return ([], [], []) if getvalues
else "true"
341 netref_regex
= re
.compile(r
'(^|[( ])\[(-?[0-9]+:|)([^\]]*|\S*)\](?=[ )]|$)')
343 def replace_netref(match
):
344 state_sel
= match
.group(2)
348 elif state_sel
[0] == "-":
349 st
= state
+ int(state_sel
[:-1])
351 st
= int(state_sel
[:-1])
353 expr
= smt
.net_expr(topmod
, "s%d" % st
, smt
.get_path(topmod
, match
.group(3)))
355 return match
.group(1) + expr
358 for loc
, expr
in db
[("final-%d" % state
) if final
else state
]:
359 actual_expr
= netref_regex
.sub(replace_netref
, expr
)
361 expr_list
.append((loc
, expr
, actual_expr
))
363 expr_list
.append(actual_expr
)
366 loc_list
, expr_list
, acual_expr_list
= zip(*expr_list
)
367 value_list
= smt
.get_list(acual_expr_list
)
368 return loc_list
, expr_list
, value_list
370 if len(expr_list
) == 0:
373 if len(expr_list
) == 1:
376 return "(and %s)" % " ".join(expr_list
)
381 if noinfo
and vcdfile
is None and vlogtbfile
is None and outconstr
is None:
382 smt
.produce_models
= False
385 print("%s %s" % (smt
.timestamp(), msg
))
388 print_msg("Solver: %s" % (so
.solver
))
390 with
open(args
[0], "r") as f
:
394 for line
in constr_write
:
400 assert topmod
is not None
401 assert topmod
in smt
.modinfo
403 if cexfile
is not None:
409 with
open(cexfile
, "r") as f
:
410 cex_regex
= re
.compile(r
'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
411 for entry
in f
.read().split():
412 match
= cex_regex
.match(entry
)
415 name
, bit
, extra_name
, step
, val
= match
.group(1), match
.group(2), match
.group(3), match
.group(4), match
.group(5)
420 if name
not in smt
.modinfo
[topmod
].inputs
:
431 if smt
.modinfo
[topmod
].wsize
[name
] == 1:
433 smtexpr
= "(= [%s] %s)" % (name
, "true" if val
else "false")
435 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bit
, bit
, name
, val
)
437 # print("cex@%d: %s" % (step, smtexpr))
438 constr_assumes
[step
].append((cexfile
, smtexpr
))
441 skip_steps
= max(skip_steps
, step
)
442 num_steps
= max(num_steps
, step
+1)
444 if aimfile
is not None:
454 with
open(aimfile
, "r") as f
:
455 for entry
in f
.read().splitlines():
456 entry
= entry
.split()
458 if entry
[0] == "input":
459 input_map
[int(entry
[1])] = (entry
[3], int(entry
[2]))
462 if entry
[0] == "init":
463 init_map
[int(entry
[1])] = (entry
[3], int(entry
[2]))
466 if entry
[0] in ["latch", "invlatch"]:
467 latch_map
[int(entry
[1])] = (entry
[3], int(entry
[2]), entry
[0] == "invlatch")
470 if entry
[0] in ["output", "wire"]:
475 with
open(aiwfile
, "r") as f
:
483 for entry
in f
.read().splitlines():
484 if len(entry
) == 0 or entry
[0] in "bcjfu.":
494 if len(init_map
) == 0:
495 for i
in range(len(entry
)):
500 value
= int(entry
[i
])
501 name
= latch_map
[i
][0]
502 bitidx
= latch_map
[i
][1]
503 invert
= latch_map
[i
][2]
508 path
= smt
.get_path(topmod
, name
)
509 width
= smt
.net_width(topmod
, path
)
513 smtexpr
= "(= [%s] %s)" % (name
, "true" if value
else "false")
515 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx
, bitidx
, name
, value
)
517 constr_assumes
[0].append((cexfile
, smtexpr
))
520 for i
in range(len(entry
)):
524 if (step
== 0) and (i
in init_map
):
525 value
= int(entry
[i
])
526 name
= init_map
[i
][0]
527 bitidx
= init_map
[i
][1]
529 path
= smt
.get_path(topmod
, name
)
531 if not smt
.net_exists(topmod
, path
):
532 match
= re
.match(r
"(.*)\[(\d+)\]$", path
[-1])
534 path
[-1] = match
.group(1)
535 addr
= int(match
.group(2))
537 if not match
or not smt
.mem_exists(topmod
, path
):
538 print_msg("Ignoring init value for unknown net: %s" % (name
))
541 meminfo
= smt
.mem_info(topmod
, path
)
542 smtexpr
= "(select [%s] #b%s)" % (".".join(path
), bin(addr
)[2:].zfill(meminfo
[0]))
546 smtexpr
= "[%s]" % name
547 width
= smt
.net_width(topmod
, path
)
551 smtexpr
= "(= %s %s)" % (smtexpr
, "true" if value
else "false")
553 smtexpr
= "(= ((_ extract %d %d) %s) #b%d)" % (bitidx
, bitidx
, smtexpr
, value
)
555 constr_assumes
[0].append((cexfile
, smtexpr
))
558 value
= int(entry
[i
])
559 name
= input_map
[i
][0]
560 bitidx
= input_map
[i
][1]
562 path
= smt
.get_path(topmod
, name
)
563 width
= smt
.net_width(topmod
, path
)
567 smtexpr
= "(= [%s] %s)" % (name
, "true" if value
else "false")
569 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx
, bitidx
, name
, value
)
571 constr_assumes
[step
].append((cexfile
, smtexpr
))
574 skip_steps
= max(skip_steps
, step
)
575 num_steps
= max(num_steps
, step
+1)
578 def write_vcd_trace(steps_start
, steps_stop
, index
):
579 filename
= vcdfile
.replace("%", index
)
580 print_msg("Writing trace to VCD file: %s" % (filename
))
582 with
open(filename
, "w") as vcd_file
:
583 vcd
= MkVcd(vcd_file
)
586 for netpath
in sorted(smt
.hiernets(topmod
)):
589 if n
.startswith("$"):
592 edge
= smt
.net_clock(topmod
, netpath
)
594 vcd
.add_net([topmod
] + netpath
, smt
.net_width(topmod
, netpath
))
596 vcd
.add_clock([topmod
] + netpath
, edge
)
597 path_list
.append(netpath
)
599 mem_trace_data
= dict()
600 for mempath
in sorted(smt
.hiermems(topmod
)):
601 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(topmod
, mempath
)
605 for i
in range(steps_start
, steps_stop
):
606 for j
in range(rports
):
607 expr_id
.append(('R', i
-steps_start
, j
, 'A'))
608 expr_id
.append(('R', i
-steps_start
, j
, 'D'))
609 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "R%dA" % j
))
610 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "R%dD" % j
))
611 for j
in range(wports
):
612 expr_id
.append(('W', i
-steps_start
, j
, 'A'))
613 expr_id
.append(('W', i
-steps_start
, j
, 'D'))
614 expr_id
.append(('W', i
-steps_start
, j
, 'M'))
615 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dA" % j
))
616 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dD" % j
))
617 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dM" % j
))
623 for eid
, edat
in zip(expr_id
, smt
.get_list(expr_list
)):
641 c
[f
] = smt
.bv2bin(edat
)
651 if len(wdata
) == 0 and len(rdata
) != 0:
652 wdata
= [[]] * len(rdata
)
654 assert len(rdata
) == len(wdata
)
656 for i
in range(len(wdata
)):
658 for j_data
in rdata
[i
]:
659 if j_data
["A"] == addr
:
660 data
= list(j_data
["D"])
666 for i
in reversed(range(len(tdata
))):
667 for k
in range(width
):
668 if tdata
[i
][k
] == "x":
674 tdata
.append(data
[:])
676 for j_data
in wdata
[i
]:
677 if j_data
["A"] != addr
:
683 for k
in range(width
):
688 tdata
.append(data
[:])
690 assert len(tdata
) == len(rdata
)
693 netpath
[-1] += "<%0*x>" % ((len(addr
)+3) // 4, int(addr
, 2))
694 vcd
.add_net([topmod
] + netpath
, width
)
696 for i
in range(steps_start
, steps_stop
):
697 if i
not in mem_trace_data
:
698 mem_trace_data
[i
] = list()
699 mem_trace_data
[i
].append((netpath
, "".join(tdata
[i
-steps_start
])))
701 for i
in range(steps_start
, steps_stop
):
703 value_list
= smt
.get_net_bin_list(topmod
, path_list
, "s%d" % i
)
704 for path
, value
in zip(path_list
, value_list
):
705 vcd
.set_net([topmod
] + path
, value
)
706 if i
in mem_trace_data
:
707 for path
, value
in mem_trace_data
[i
]:
708 vcd
.set_net([topmod
] + path
, value
)
710 vcd
.set_time(steps_stop
)
713 def write_vlogtb_trace(steps_start
, steps_stop
, index
):
714 filename
= vlogtbfile
.replace("%", index
)
715 print_msg("Writing trace to Verilog testbench: %s" % (filename
))
717 vlogtb_topmod
= topmod
718 vlogtb_state
= "s@@step_idx@@"
720 if vlogtbtop
is not None:
721 for item
in vlogtbtop
.split("."):
722 assert item
in smt
.modinfo
[vlogtb_topmod
].cells
723 vlogtb_state
= "(|%s_h %s| %s)" % (vlogtb_topmod
, item
, vlogtb_state
)
724 vlogtb_topmod
= smt
.modinfo
[vlogtb_topmod
].cells
[item
]
726 with
open(filename
, "w") as f
:
727 print("`ifndef VERILATOR", file=f
)
728 print("module testbench;", file=f
)
729 print(" reg [4095:0] vcdfile;", file=f
)
730 print(" reg clock;", file=f
)
731 print("`else", file=f
)
732 print("module testbench(input clock, output reg genclock);", file=f
)
733 print(" initial genclock = 1;", file=f
)
734 print("`endif", file=f
)
736 print(" reg genclock = 1;", file=f
)
737 print(" reg [31:0] cycle = 0;", file=f
)
739 primary_inputs
= list()
742 for name
in smt
.modinfo
[vlogtb_topmod
].inputs
:
743 if name
in ["clk", "clock", "CLK", "CLOCK"]:
744 clock_inputs
.add(name
)
745 width
= smt
.modinfo
[vlogtb_topmod
].wsize
[name
]
746 primary_inputs
.append((name
, width
))
748 for name
, width
in primary_inputs
:
749 if name
in clock_inputs
:
750 print(" wire [%d:0] PI_%s = clock;" % (width
-1, name
), file=f
)
752 print(" reg [%d:0] PI_%s;" % (width
-1, name
), file=f
)
754 print(" %s UUT (" % vlogtb_topmod
, file=f
)
755 print(",\n".join(" .{name}(PI_{name})".format(name
=name
) for name
, _
in primary_inputs
), file=f
)
758 print("`ifndef VERILATOR", file=f
)
759 print(" initial begin", file=f
)
760 print(" if ($value$plusargs(\"vcd=%s\", vcdfile)) begin", file=f
)
761 print(" $dumpfile(vcdfile);", file=f
)
762 print(" $dumpvars(0, testbench);", file=f
)
763 print(" end", file=f
)
764 print(" #5 clock = 0;", file=f
)
765 print(" while (genclock) begin", file=f
)
766 print(" #5 clock = 0;", file=f
)
767 print(" #5 clock = 1;", file=f
)
768 print(" end", file=f
)
769 print(" end", file=f
)
770 print("`endif", file=f
)
772 print(" initial begin", file=f
)
774 regs
= sorted(smt
.hiernets(vlogtb_topmod
, regs_only
=True))
775 regvals
= smt
.get_net_bin_list(vlogtb_topmod
, regs
, vlogtb_state
.replace("@@step_idx@@", str(steps_start
)))
777 print("`ifndef VERILATOR", file=f
)
778 print(" #1;", file=f
)
779 print("`endif", file=f
)
780 for reg
, val
in zip(regs
, regvals
):
783 if n
.startswith("$"):
785 print(" %sUUT.%s = %d'b%s;" % ("// " if hidden_net
else "", ".".join(reg
), len(val
), val
), file=f
)
787 anyconsts
= sorted(smt
.hieranyconsts(vlogtb_topmod
))
788 for info
in anyconsts
:
789 if info
[3] is not None:
790 modstate
= smt
.net_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(steps_start
)), info
[0])
791 value
= smt
.bv2bin(smt
.get("(|%s| %s)" % (info
[1], modstate
)))
792 print(" UUT.%s = %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
794 mems
= sorted(smt
.hiermems(vlogtb_topmod
))
796 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(vlogtb_topmod
, mempath
)
798 addr_expr_list
= list()
799 data_expr_list
= list()
800 for i
in range(steps_start
, steps_stop
):
801 for j
in range(rports
):
802 addr_expr_list
.append(smt
.mem_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dA" % j
))
803 data_expr_list
.append(smt
.mem_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dD" % j
))
805 addr_list
= smt
.get_list(addr_expr_list
)
806 data_list
= smt
.get_list(data_expr_list
)
809 for addr
, data
in zip(addr_list
, data_list
):
810 addr
= smt
.bv2bin(addr
)
811 data
= smt
.bv2bin(data
)
812 if addr
not in addr_data
:
813 addr_data
[addr
] = data
815 for addr
, data
in addr_data
.items():
816 print(" UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath
), len(addr
), addr
, len(data
), data
), file=f
)
819 anyseqs
= sorted(smt
.hieranyseqs(vlogtb_topmod
))
821 for i
in range(steps_start
, steps_stop
):
822 pi_names
= [[name
] for name
, _
in primary_inputs
if name
not in clock_inputs
]
823 pi_values
= smt
.get_net_bin_list(vlogtb_topmod
, pi_names
, vlogtb_state
.replace("@@step_idx@@", str(i
)))
825 print(" // state %d" % i
, file=f
)
828 print(" if (cycle == %d) begin" % (i
-1), file=f
)
830 for name
, val
in zip(pi_names
, pi_values
):
832 print(" PI_%s <= %d'b%s;" % (".".join(name
), len(val
), val
), file=f
)
834 print(" PI_%s = %d'b%s;" % (".".join(name
), len(val
), val
), file=f
)
837 if info
[3] is not None:
838 modstate
= smt
.net_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), info
[0])
839 value
= smt
.bv2bin(smt
.get("(|%s| %s)" % (info
[1], modstate
)))
841 print(" UUT.%s <= %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
843 print(" UUT.%s = %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
846 print(" end", file=f
)
850 print(" end", file=f
)
851 print(" always @(posedge clock) begin", file=f
)
853 print(" genclock <= cycle < %d;" % (steps_stop
-1), file=f
)
854 print(" cycle <= cycle + 1;", file=f
)
855 print(" end", file=f
)
857 print("endmodule", file=f
)
860 def write_constr_trace(steps_start
, steps_stop
, index
):
861 filename
= outconstr
.replace("%", index
)
862 print_msg("Writing trace to constraints file: %s" % (filename
))
864 constr_topmod
= topmod
865 constr_state
= "s@@step_idx@@"
868 if smtctop
is not None:
869 for item
in smtctop
[0].split("."):
870 assert item
in smt
.modinfo
[constr_topmod
].cells
871 constr_state
= "(|%s_h %s| %s)" % (constr_topmod
, item
, constr_state
)
872 constr_topmod
= smt
.modinfo
[constr_topmod
].cells
[item
]
874 constr_prefix
= smtctop
[1] + "."
877 steps_start
= steps_stop
- 1
879 with
open(filename
, "w") as f
:
880 primary_inputs
= list()
882 for name
in smt
.modinfo
[constr_topmod
].inputs
:
883 width
= smt
.modinfo
[constr_topmod
].wsize
[name
]
884 primary_inputs
.append((name
, width
))
886 if steps_start
== 0 or smtcinit
:
887 print("initial", file=f
)
889 print("state %d" % steps_start
, file=f
)
891 regnames
= sorted(smt
.hiernets(constr_topmod
, regs_only
=True))
892 regvals
= smt
.get_net_list(constr_topmod
, regnames
, constr_state
.replace("@@step_idx@@", str(steps_start
)))
894 for name
, val
in zip(regnames
, regvals
):
895 print("assume (= [%s%s] %s)" % (constr_prefix
, ".".join(name
), val
), file=f
)
897 mems
= sorted(smt
.hiermems(constr_topmod
))
899 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(constr_topmod
, mempath
)
901 addr_expr_list
= list()
902 data_expr_list
= list()
903 for i
in range(steps_start
, steps_stop
):
904 for j
in range(rports
):
905 addr_expr_list
.append(smt
.mem_expr(constr_topmod
, constr_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dA" % j
))
906 data_expr_list
.append(smt
.mem_expr(constr_topmod
, constr_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dD" % j
))
908 addr_list
= smt
.get_list(addr_expr_list
)
909 data_list
= smt
.get_list(data_expr_list
)
912 for addr
, data
in zip(addr_list
, data_list
):
913 if addr
not in addr_data
:
914 addr_data
[addr
] = data
916 for addr
, data
in addr_data
.items():
917 print("assume (= (select [%s%s] %s) %s)" % (constr_prefix
, ".".join(mempath
), addr
, data
), file=f
)
919 for k
in range(steps_start
, steps_stop
):
922 print("state %d" % k
, file=f
)
924 pi_names
= [[name
] for name
, _
in sorted(primary_inputs
)]
925 pi_values
= smt
.get_net_list(constr_topmod
, pi_names
, constr_state
.replace("@@step_idx@@", str(k
)))
927 for name
, val
in zip(pi_names
, pi_values
):
928 print("assume (= [%s%s] %s)" % (constr_prefix
, ".".join(name
), val
), file=f
)
931 def write_trace(steps_start
, steps_stop
, index
):
932 if vcdfile
is not None:
933 write_vcd_trace(steps_start
, steps_stop
, index
)
935 if vlogtbfile
is not None:
936 write_vlogtb_trace(steps_start
, steps_stop
, index
)
938 if outconstr
is not None:
939 write_constr_trace(steps_start
, steps_stop
, index
)
942 def print_failed_asserts_worker(mod
, state
, path
, extrainfo
):
943 assert mod
in smt
.modinfo
944 found_failed_assert
= False
946 if smt
.get("(|%s_a| %s)" % (mod
, state
)) in ["true", "#b1"]:
949 for cellname
, celltype
in smt
.modinfo
[mod
].cells
.items():
950 if print_failed_asserts_worker(celltype
, "(|%s_h %s| %s)" % (mod
, cellname
, state
), path
+ "." + cellname
, extrainfo
):
951 found_failed_assert
= True
953 for assertfun
, assertinfo
in smt
.modinfo
[mod
].asserts
.items():
954 if smt
.get("(|%s| %s)" % (assertfun
, state
)) in ["false", "#b0"]:
955 print_msg("Assert failed in %s: %s%s" % (path
, assertinfo
, extrainfo
))
956 found_failed_assert
= True
958 return found_failed_assert
961 def print_failed_asserts(state
, final
=False, extrainfo
=""):
963 loc_list
, expr_list
, value_list
= get_constr_expr(constr_asserts
, state
, final
=final
, getvalues
=True)
964 found_failed_assert
= False
966 for loc
, expr
, value
in zip(loc_list
, expr_list
, value_list
):
967 if smt
.bv2int(value
) == 0:
968 print_msg("Assert %s failed: %s%s" % (loc
, expr
, extrainfo
))
969 found_failed_assert
= True
972 if print_failed_asserts_worker(topmod
, "s%d" % state
, topmod
, extrainfo
):
973 found_failed_assert
= True
975 return found_failed_assert
978 def print_anyconsts_worker(mod
, state
, path
):
979 assert mod
in smt
.modinfo
981 for cellname
, celltype
in smt
.modinfo
[mod
].cells
.items():
982 print_anyconsts_worker(celltype
, "(|%s_h %s| %s)" % (mod
, cellname
, state
), path
+ "." + cellname
)
984 for fun
, info
in smt
.modinfo
[mod
].anyconsts
.items():
986 print_msg("Value for anyconst in %s (%s): %d" % (path
, info
[0], smt
.bv2int(smt
.get("(|%s| %s)" % (fun
, state
)))))
988 print_msg("Value for anyconst %s.%s (%s): %d" % (path
, info
[1], info
[0], smt
.bv2int(smt
.get("(|%s| %s)" % (fun
, state
)))))
991 def print_anyconsts(state
):
993 print_anyconsts_worker(topmod
, "s%d" % state
, topmod
)
996 def get_cover_list(mod
, base
):
997 assert mod
in smt
.modinfo
1002 for expr
, desc
in smt
.modinfo
[mod
].covers
.items():
1003 cover_expr
.append("(ite (|%s| %s) #b1 #b0)" % (expr
, base
))
1004 cover_desc
.append(desc
)
1006 for cell
, submod
in smt
.modinfo
[mod
].cells
.items():
1007 e
, d
= get_cover_list(submod
, "(|%s_h %s| %s)" % (mod
, cell
, base
))
1011 return cover_expr
, cover_desc
1014 asserts_antecedent_cache
= [list()]
1015 asserts_consequent_cache
= [list()]
1016 asserts_cache_dirty
= False
1018 def smt_state(step
):
1019 smt
.write("(declare-fun s%d () |%s_s|)" % (step
, topmod
))
1020 states
.append("s%d" % step
)
1022 def smt_assert(expr
):
1026 smt
.write("(assert %s)" % expr
)
1028 def smt_assert_antecedent(expr
):
1032 smt
.write("(assert %s)" % expr
)
1034 global asserts_cache_dirty
1035 asserts_cache_dirty
= True
1036 asserts_antecedent_cache
[-1].append(expr
)
1038 def smt_assert_consequent(expr
):
1042 smt
.write("(assert %s)" % expr
)
1044 global asserts_cache_dirty
1045 asserts_cache_dirty
= True
1046 asserts_consequent_cache
[-1].append(expr
)
1048 def smt_forall_assert():
1052 global asserts_cache_dirty
1053 asserts_cache_dirty
= False
1055 def make_assert_expr(asserts_cache
):
1057 for lst
in asserts_cache
:
1060 assert len(expr
) != 0
1065 expr
= "(and %s)" % (" ".join(expr
))
1068 antecedent_expr
= make_assert_expr(asserts_antecedent_cache
)
1069 consequent_expr
= make_assert_expr(asserts_consequent_cache
)
1071 states_db
= set(states
)
1072 used_states_db
= set()
1073 new_antecedent_expr
= list()
1074 new_consequent_expr
= list()
1075 assert_expr
= list()
1077 def make_new_expr(new_expr
, expr
):
1079 while cursor
< len(expr
):
1081 if expr
[cursor
] in '|"':
1082 while cursor
+l
+1 < len(expr
) and expr
[cursor
] != expr
[cursor
+l
]:
1085 elif expr
[cursor
] not in '() ':
1086 while cursor
+l
< len(expr
) and expr
[cursor
+l
] not in '|"() ':
1089 word
= expr
[cursor
:cursor
+l
]
1090 if word
in states_db
:
1091 used_states_db
.add(word
)
1094 new_expr
.append(word
)
1097 make_new_expr(new_antecedent_expr
, antecedent_expr
)
1098 make_new_expr(new_consequent_expr
, consequent_expr
)
1100 new_antecedent_expr
= ["".join(new_antecedent_expr
)]
1101 new_consequent_expr
= ["".join(new_consequent_expr
)]
1103 if states
[0] in used_states_db
:
1104 new_antecedent_expr
.append("(|%s_ex_state_eq| %s %s_)" % (topmod
, states
[0], states
[0]))
1106 if s
in used_states_db
:
1107 new_antecedent_expr
.append("(|%s_ex_input_eq| %s %s_)" % (topmod
, s
, s
))
1109 if len(new_antecedent_expr
) == 0:
1110 new_antecedent_expr
= "true"
1111 elif len(new_antecedent_expr
) == 1:
1112 new_antecedent_expr
= new_antecedent_expr
[0]
1114 new_antecedent_expr
= "(and %s)" % (" ".join(new_antecedent_expr
))
1116 if len(new_consequent_expr
) == 0:
1117 new_consequent_expr
= "true"
1118 elif len(new_consequent_expr
) == 1:
1119 new_consequent_expr
= new_consequent_expr
[0]
1121 new_consequent_expr
= "(and %s)" % (" ".join(new_consequent_expr
))
1123 assert_expr
.append("(assert (forall (")
1126 if s
in used_states_db
:
1127 assert_expr
.append("%s(%s_ |%s_s|)" % ("" if first_state
else " ", s
, topmod
))
1129 assert_expr
.append(") (=> %s %s)))" % (new_antecedent_expr
, new_consequent_expr
))
1131 smt
.write("".join(assert_expr
))
1134 global asserts_cache_dirty
1135 asserts_cache_dirty
= True
1136 asserts_antecedent_cache
.append(list())
1137 asserts_consequent_cache
.append(list())
1138 smt
.write("(push 1)")
1141 global asserts_cache_dirty
1142 asserts_cache_dirty
= True
1143 asserts_antecedent_cache
.pop()
1144 asserts_consequent_cache
.pop()
1145 smt
.write("(pop 1)")
1147 def smt_check_sat():
1148 if asserts_cache_dirty
:
1150 return smt
.check_sat()
1154 skip_counter
= step_size
1155 for step
in range(num_steps
, -1, -1):
1157 print_msg("Temporal induction not supported for exists-forall problems.")
1161 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1162 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1163 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1164 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1166 if step
== num_steps
:
1167 smt_assert("(not (and (|%s_a| s%d) %s))" % (topmod
, step
, get_constr_expr(constr_asserts
, step
)))
1170 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
, step
+1))
1171 smt_assert("(|%s_a| s%d)" % (topmod
, step
))
1172 smt_assert(get_constr_expr(constr_asserts
, step
))
1174 if step
> num_steps
-skip_steps
:
1175 print_msg("Skipping induction in step %d.." % (step
))
1179 if skip_counter
< step_size
:
1180 print_msg("Skipping induction in step %d.." % (step
))
1184 print_msg("Trying induction in step %d.." % (step
))
1186 if smt_check_sat() == "sat":
1188 print_msg("Temporal induction failed!")
1189 print_anyconsts(num_steps
)
1190 print_failed_asserts(num_steps
)
1191 write_trace(step
, num_steps
+1, '%')
1194 print_anyconsts(num_steps
)
1195 print_failed_asserts(num_steps
)
1196 write_trace(step
, num_steps
+1, "%d" % step
)
1199 print_msg("Temporal induction successful.")
1204 cover_expr
, cover_desc
= get_cover_list(topmod
, "state")
1205 cover_mask
= "1" * len(cover_desc
)
1207 if len(cover_expr
) > 1:
1208 cover_expr
= "(concat %s)" % " ".join(cover_expr
)
1209 elif len(cover_expr
) == 1:
1210 cover_expr
= cover_expr
[0]
1215 smt
.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod
, len(cover_desc
), cover_expr
))
1219 found_failed_assert
= False
1221 assert step_size
== 1
1223 while step
< num_steps
:
1225 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1226 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1227 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1231 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1233 smt_assert_antecedent("(|%s_i| s0)" % (topmod
))
1234 smt_assert_antecedent("(|%s_is| s0)" % (topmod
))
1237 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
-1, step
))
1238 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1240 while "1" in cover_mask
:
1241 print_msg("Checking cover reachability in step %d.." % (step
))
1243 smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx
, step
, "0" * len(cover_desc
)))
1245 if smt_check_sat() == "unsat":
1249 if append_steps
> 0:
1250 for i
in range(step
+1, step
+1+append_steps
):
1251 print_msg("Appending additional step %d." % i
)
1253 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, i
))
1254 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, i
))
1255 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, i
))
1256 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, i
-1, i
))
1257 smt_assert_consequent(get_constr_expr(constr_assumes
, i
))
1258 print_msg("Re-solving with appended steps..")
1259 assert smt_check_sat() == "sat"
1261 reached_covers
= smt
.bv2bin(smt
.get("(covers_%d s%d)" % (coveridx
, step
)))
1262 assert len(reached_covers
) == len(cover_desc
)
1266 for i
in range(len(reached_covers
)):
1267 if reached_covers
[i
] == "0":
1268 new_cover_mask
.append(cover_mask
[i
])
1271 print_msg("Reached cover statement at %s in step %d." % (cover_desc
[i
], step
))
1272 new_cover_mask
.append("0")
1274 cover_mask
= "".join(new_cover_mask
)
1276 for i
in range(step
+1+append_steps
):
1277 if print_failed_asserts(i
, extrainfo
=" (step %d)" % i
):
1278 found_failed_assert
= True
1280 write_trace(0, step
+1+append_steps
, "%d" % coveridx
)
1282 if found_failed_assert
:
1287 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
))
1289 if found_failed_assert
:
1292 if "1" not in cover_mask
:
1298 if "1" in cover_mask
:
1299 for i
in range(len(cover_mask
)):
1300 if cover_mask
[i
] == "1":
1301 print_msg("Unreached cover statement at %s." % cover_desc
[i
])
1303 else: # not tempind, covermode
1306 while step
< num_steps
:
1308 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1309 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1310 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1314 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1316 smt_assert_antecedent("(|%s_i| s0)" % (topmod
))
1317 smt_assert_antecedent("(|%s_is| s0)" % (topmod
))
1320 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
-1, step
))
1321 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1323 if step
< skip_steps
:
1324 if assume_skipped
is not None and step
>= assume_skipped
:
1325 print_msg("Skipping step %d (and assuming pass).." % (step
))
1326 smt_assert("(|%s_a| s%d)" % (topmod
, step
))
1327 smt_assert(get_constr_expr(constr_asserts
, step
))
1329 print_msg("Skipping step %d.." % (step
))
1333 last_check_step
= step
1334 for i
in range(1, step_size
):
1335 if step
+i
< num_steps
:
1337 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
+i
))
1338 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
+i
))
1339 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
+i
))
1340 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
+i
-1, step
+i
))
1341 smt_assert_consequent(get_constr_expr(constr_assumes
, step
+i
))
1342 last_check_step
= step
+i
1346 if last_check_step
== step
:
1347 print_msg("Checking assumptions in step %d.." % (step
))
1349 print_msg("Checking assumptions in steps %d to %d.." % (step
, last_check_step
))
1351 if smt_check_sat() == "unsat":
1352 print("%s Warmup failed!" % smt
.timestamp())
1357 if last_check_step
== step
:
1358 print_msg("Checking assertions in step %d.." % (step
))
1360 print_msg("Checking assertions in steps %d to %d.." % (step
, last_check_step
))
1363 smt_assert("(not (and %s))" % " ".join(["(|%s_a| s%d)" % (topmod
, i
) for i
in range(step
, last_check_step
+1)] +
1364 [get_constr_expr(constr_asserts
, i
) for i
in range(step
, last_check_step
+1)]))
1366 if smt_check_sat() == "sat":
1367 print("%s BMC failed!" % smt
.timestamp())
1368 if append_steps
> 0:
1369 for i
in range(last_check_step
+1, last_check_step
+1+append_steps
):
1370 print_msg("Appending additional step %d." % i
)
1372 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, i
))
1373 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, i
))
1374 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, i
))
1375 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, i
-1, i
))
1376 smt_assert_consequent(get_constr_expr(constr_assumes
, i
))
1377 assert smt_check_sat() == "sat"
1378 print_anyconsts(step
)
1379 for i
in range(step
, last_check_step
+1):
1380 print_failed_asserts(i
)
1381 write_trace(0, last_check_step
+1+append_steps
, '%')
1387 if (constr_final_start
is not None) or (last_check_step
+1 != num_steps
):
1388 for i
in range(step
, last_check_step
+1):
1389 smt_assert("(|%s_a| s%d)" % (topmod
, i
))
1390 smt_assert(get_constr_expr(constr_asserts
, i
))
1392 if constr_final_start
is not None:
1393 for i
in range(step
, last_check_step
+1):
1394 if i
< constr_final_start
:
1397 print_msg("Checking final constraints in step %d.." % (i
))
1400 smt_assert_consequent(get_constr_expr(constr_assumes
, i
, final
=True))
1401 smt_assert("(not %s)" % get_constr_expr(constr_asserts
, i
, final
=True))
1403 if smt_check_sat() == "sat":
1404 print("%s BMC failed!" % smt
.timestamp())
1406 print_failed_asserts(i
, final
=True)
1407 write_trace(0, i
+1, '%')
1416 for i
in range(step
, last_check_step
+1):
1417 smt_assert("(|%s_a| s%d)" % (topmod
, i
))
1418 smt_assert(get_constr_expr(constr_asserts
, i
))
1420 print_msg("Solving for step %d.." % (last_check_step
))
1421 if smt_check_sat() != "sat":
1422 print("%s No solution found!" % smt
.timestamp())
1428 write_trace(0, last_check_step
+1, "%d" % step
)
1432 if gentrace
and retstatus
:
1434 write_trace(0, num_steps
, '%')
1440 print_msg("Status: %s" % ("PASSED" if retstatus
else "FAILED (!)"))
1441 sys
.exit(0 if retstatus
else 1)