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 print(os
.path
.basename(sys
.argv
[0]) + """ [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 different file extensions).
92 the AIGER witness file does not include the status and
95 --btorwit <btor_witness_filename>
99 only run the core proof, do not collect and print any
100 additional information (e.g. which assert failed)
103 check if the design with assumptions but without assertions
104 is SAT before checking if assertions are UNSAT. This will
105 detect if there are contradicting assumptions. In some cases
106 this will also help to "warm up" the solver, potentially
110 only check final constraints, assume base case
112 --assume-skipped <start_step>
113 assume asserts in skipped steps in BMC.
114 no assumptions are created for skipped steps
117 --dump-vcd <vcd_filename>
118 write trace to this VCD file
119 (hint: use 'write_smt2 -wires' for maximum
120 coverage of signals in generated VCD file)
122 --dump-vlogtb <verilog_filename>
123 write trace as Verilog test bench
125 --vlogtb-top <hierarchical_name>
126 use the given entity as top module for the generated
127 Verilog test bench. The <hierarchical_name> is relative
128 to the design top module without the top module name.
130 --dump-smtc <constr_filename>
131 write trace as constraints file
134 write just the last state as initial constraint to smtc file
136 --smtc-top <old>[:<new>]
137 replace <old> with <new> in constraints dumped to smtc
138 file and only dump object below <old> in design hierarchy.
141 do not assume initial conditions in state 0
144 when using -g or -i, create a dump file for each
145 step. The character '%' is replaces in all dump
146 filenames with the step number.
149 add <num_steps> time steps at the end of the trace
150 when creating a counter example (this additional time
151 steps will still be constrained by assumptions)
157 opts
, args
= getopt
.getopt(sys
.argv
[1:], so
.shortopts
+ "t:igcm:", so
.longopts
+
158 ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
159 "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
160 "smtc-init", "smtc-top=", "noinit"])
169 num_steps
= int(a
[0])
171 skip_steps
= int(a
[0])
172 num_steps
= int(a
[1])
174 skip_steps
= int(a
[0])
175 step_size
= int(a
[1])
176 num_steps
= int(a
[2])
179 elif o
== "--assume-skipped":
180 assume_skipped
= int(a
)
181 elif o
== "--final-only":
189 aimfile
, aiwfile
= a
.split(":")
193 elif o
== "--aig-noheader":
195 elif o
== "--btorwit":
197 elif o
== "--dump-vcd":
199 elif o
== "--dump-vlogtb":
201 elif o
== "--vlogtb-top":
203 elif o
== "--dump-smtc":
205 elif o
== "--smtc-init":
207 elif o
== "--smtc-top":
208 smtctop
= a
.split(":")
209 if len(smtctop
) == 1:
211 assert len(smtctop
) == 2
212 smtctop
= tuple(smtctop
)
213 elif o
== "--dump-all":
215 elif o
== "--presat":
217 elif o
== "--noinfo":
219 elif o
== "--noinit":
221 elif o
== "--append":
222 append_steps
= int(a
)
231 elif so
.handle(o
, a
):
239 if sum([tempind
, gentrace
, covermode
]) > 1:
242 constr_final_start
= None
243 constr_asserts
= defaultdict(list)
244 constr_assumes
= defaultdict(list)
245 constr_write
= list()
248 current_states
= None
251 with
open(fn
, "r") as f
:
255 if line
.startswith("#"):
258 tokens
= line
.split()
263 if tokens
[0] == "initial":
264 current_states
= set()
266 current_states
.add(0)
269 if tokens
[0] == "final":
272 current_states
= set(["final-%d" % i
for i
in range(0, num_steps
+1)])
273 constr_final_start
= 0
274 elif len(tokens
) == 2:
275 arg
= abs(int(tokens
[1]))
276 current_states
= set(["final-%d" % i
for i
in range(arg
, num_steps
+1)])
277 constr_final_start
= arg
if constr_final_start
is None else min(constr_final_start
, arg
)
282 if tokens
[0] == "state":
283 current_states
= set()
285 for token
in tokens
[1:]:
286 tok
= token
.split(":")
288 current_states
.add(int(token
))
295 for i
in range(lower
, upper
+1):
296 current_states
.add(i
)
301 if tokens
[0] == "always":
303 current_states
= set(range(0, num_steps
+1))
304 elif len(tokens
) == 2:
305 arg
= abs(int(tokens
[1]))
306 current_states
= set(range(arg
, num_steps
+1))
311 if tokens
[0] == "assert":
312 assert current_states
is not None
314 for state
in current_states
:
315 constr_asserts
[state
].append(("%s:%d" % (fn
, current_line
), " ".join(tokens
[1:])))
319 if tokens
[0] == "assume":
320 assert current_states
is not None
322 for state
in current_states
:
323 constr_assumes
[state
].append(("%s:%d" % (fn
, current_line
), " ".join(tokens
[1:])))
327 if tokens
[0] == "write":
328 constr_write
.append(" ".join(tokens
[1:]))
331 if tokens
[0] == "logic":
332 so
.logic
= " ".join(tokens
[1:])
338 def get_constr_expr(db
, state
, final
=False, getvalues
=False):
340 if ("final-%d" % state
) not in db
:
341 return ([], [], []) if getvalues
else "true"
344 return ([], [], []) if getvalues
else "true"
346 netref_regex
= re
.compile(r
'(^|[( ])\[(-?[0-9]+:|)([^\]]*|\S*)\](?=[ )]|$)')
348 def replace_netref(match
):
349 state_sel
= match
.group(2)
353 elif state_sel
[0] == "-":
354 st
= state
+ int(state_sel
[:-1])
356 st
= int(state_sel
[:-1])
358 expr
= smt
.net_expr(topmod
, "s%d" % st
, smt
.get_path(topmod
, match
.group(3)))
360 return match
.group(1) + expr
363 for loc
, expr
in db
[("final-%d" % state
) if final
else state
]:
364 actual_expr
= netref_regex
.sub(replace_netref
, expr
)
366 expr_list
.append((loc
, expr
, actual_expr
))
368 expr_list
.append(actual_expr
)
371 loc_list
, expr_list
, acual_expr_list
= zip(*expr_list
)
372 value_list
= smt
.get_list(acual_expr_list
)
373 return loc_list
, expr_list
, value_list
375 if len(expr_list
) == 0:
378 if len(expr_list
) == 1:
381 return "(and %s)" % " ".join(expr_list
)
386 if noinfo
and vcdfile
is None and vlogtbfile
is None and outconstr
is None:
387 smt
.produce_models
= False
390 print("%s %s" % (smt
.timestamp(), msg
))
393 print_msg("Solver: %s" % (so
.solver
))
395 with
open(args
[0], "r") as f
:
399 for line
in constr_write
:
405 assert topmod
is not None
406 assert topmod
in smt
.modinfo
408 if cexfile
is not None:
414 with
open(cexfile
, "r") as f
:
415 cex_regex
= re
.compile(r
'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
416 for entry
in f
.read().split():
417 match
= cex_regex
.match(entry
)
420 name
, bit
, extra_name
, step
, val
= match
.group(1), match
.group(2), match
.group(3), match
.group(4), match
.group(5)
425 if name
not in smt
.modinfo
[topmod
].inputs
:
436 if smt
.modinfo
[topmod
].wsize
[name
] == 1:
438 smtexpr
= "(= [%s] %s)" % (name
, "true" if val
else "false")
440 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bit
, bit
, name
, val
)
442 # print("cex@%d: %s" % (step, smtexpr))
443 constr_assumes
[step
].append((cexfile
, smtexpr
))
446 skip_steps
= max(skip_steps
, step
)
447 num_steps
= max(num_steps
, step
+1)
449 if aimfile
is not None:
459 with
open(aimfile
, "r") as f
:
460 for entry
in f
.read().splitlines():
461 entry
= entry
.split()
463 if entry
[0] == "input":
464 input_map
[int(entry
[1])] = (entry
[3], int(entry
[2]))
467 if entry
[0] == "init":
468 init_map
[int(entry
[1])] = (entry
[3], int(entry
[2]))
471 if entry
[0] in ["latch", "invlatch"]:
472 latch_map
[int(entry
[1])] = (entry
[3], int(entry
[2]), entry
[0] == "invlatch")
475 if entry
[0] in ["output", "wire"]:
480 with
open(aiwfile
, "r") as f
:
488 for entry
in f
.read().splitlines():
489 if len(entry
) == 0 or entry
[0] in "bcjfu.":
499 if len(init_map
) == 0:
500 for i
in range(len(entry
)):
505 value
= int(entry
[i
])
506 name
= latch_map
[i
][0]
507 bitidx
= latch_map
[i
][1]
508 invert
= latch_map
[i
][2]
513 path
= smt
.get_path(topmod
, name
)
514 width
= smt
.net_width(topmod
, path
)
518 smtexpr
= "(= [%s] %s)" % (name
, "true" if value
else "false")
520 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx
, bitidx
, name
, value
)
522 constr_assumes
[0].append((cexfile
, smtexpr
))
525 for i
in range(len(entry
)):
529 if (step
== 0) and (i
in init_map
):
530 value
= int(entry
[i
])
531 name
= init_map
[i
][0]
532 bitidx
= init_map
[i
][1]
534 path
= smt
.get_path(topmod
, name
)
536 if not smt
.net_exists(topmod
, path
):
537 match
= re
.match(r
"(.*)\[(\d+)\]$", path
[-1])
539 path
[-1] = match
.group(1)
540 addr
= int(match
.group(2))
542 if not match
or not smt
.mem_exists(topmod
, path
):
543 print_msg("Ignoring init value for unknown net: %s" % (name
))
546 meminfo
= smt
.mem_info(topmod
, path
)
547 smtexpr
= "(select [%s] #b%s)" % (".".join(path
), bin(addr
)[2:].zfill(meminfo
[0]))
551 smtexpr
= "[%s]" % name
552 width
= smt
.net_width(topmod
, path
)
556 smtexpr
= "(= %s %s)" % (smtexpr
, "true" if value
else "false")
558 smtexpr
= "(= ((_ extract %d %d) %s) #b%d)" % (bitidx
, bitidx
, smtexpr
, value
)
560 constr_assumes
[0].append((cexfile
, smtexpr
))
563 value
= int(entry
[i
])
564 name
= input_map
[i
][0]
565 bitidx
= input_map
[i
][1]
567 path
= smt
.get_path(topmod
, name
)
568 width
= smt
.net_width(topmod
, path
)
572 smtexpr
= "(= [%s] %s)" % (name
, "true" if value
else "false")
574 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx
, bitidx
, name
, value
)
576 constr_assumes
[step
].append((cexfile
, smtexpr
))
579 skip_steps
= max(skip_steps
, step
)
580 num_steps
= max(num_steps
, step
+1)
583 if btorwitfile
is not None:
584 with
open(btorwitfile
, "r") as f
:
600 if line
== "" or line
[0] == "b" or line
[0] == "j":
606 if line
[0] == '#' or line
[0] == '@':
611 altsuffix
= "#" + suffix
[1:]
613 altsuffix
= "@" + suffix
[1:]
621 if line
[-1].endswith(suffix
):
622 line
[-1] = line
[-1][0:len(line
[-1]) - len(suffix
)]
624 if line
[-1].endswith(altsuffix
):
625 line
[-1] = line
[-1][0:len(line
[-1]) - len(altsuffix
)]
627 if line
[-1][0] == "$":
631 if len(line
) == 3 and line
[1][0] != "[":
635 path
= smt
.get_path(topmod
, name
)
637 if not smt
.net_exists(topmod
, path
):
640 width
= smt
.net_width(topmod
, path
)
643 assert value
in ["0", "1"]
644 value
= "true" if value
== "1" else "false"
648 smtexpr
= "(= [%s] %s)" % (name
, value
)
649 constr_assumes
[step
].append((btorwitfile
, smtexpr
))
652 if len(line
) == 4 and line
[1][0] == "[":
657 path
= smt
.get_path(topmod
, name
)
659 if not smt
.mem_exists(topmod
, path
):
662 meminfo
= smt
.mem_info(topmod
, path
)
665 assert value
in ["0", "1"]
666 value
= "true" if value
== "1" else "false"
670 assert index
[0] == "["
671 assert index
[-1] == "]"
672 index
= "#b" + index
[1:-1]
674 smtexpr
= "(= (select [%s] %s) %s)" % (name
, index
, value
)
675 constr_assumes
[step
].append((btorwitfile
, smtexpr
))
680 def write_vcd_trace(steps_start
, steps_stop
, index
):
681 filename
= vcdfile
.replace("%", index
)
682 print_msg("Writing trace to VCD file: %s" % (filename
))
684 with
open(filename
, "w") as vcd_file
:
685 vcd
= MkVcd(vcd_file
)
688 for netpath
in sorted(smt
.hiernets(topmod
)):
691 if n
.startswith("$"):
694 edge
= smt
.net_clock(topmod
, netpath
)
696 vcd
.add_net([topmod
] + netpath
, smt
.net_width(topmod
, netpath
))
698 vcd
.add_clock([topmod
] + netpath
, edge
)
699 path_list
.append(netpath
)
701 mem_trace_data
= dict()
702 for mempath
in sorted(smt
.hiermems(topmod
)):
703 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(topmod
, mempath
)
707 for i
in range(steps_start
, steps_stop
):
708 for j
in range(rports
):
709 expr_id
.append(('R', i
-steps_start
, j
, 'A'))
710 expr_id
.append(('R', i
-steps_start
, j
, 'D'))
711 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "R%dA" % j
))
712 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "R%dD" % j
))
713 for j
in range(wports
):
714 expr_id
.append(('W', i
-steps_start
, j
, 'A'))
715 expr_id
.append(('W', i
-steps_start
, j
, 'D'))
716 expr_id
.append(('W', i
-steps_start
, j
, 'M'))
717 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dA" % j
))
718 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dD" % j
))
719 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dM" % j
))
725 for eid
, edat
in zip(expr_id
, smt
.get_list(expr_list
)):
743 c
[f
] = smt
.bv2bin(edat
)
753 if len(wdata
) == 0 and len(rdata
) != 0:
754 wdata
= [[]] * len(rdata
)
756 assert len(rdata
) == len(wdata
)
758 for i
in range(len(wdata
)):
760 for j_data
in rdata
[i
]:
761 if j_data
["A"] == addr
:
762 data
= list(j_data
["D"])
768 for i
in reversed(range(len(tdata
))):
769 for k
in range(width
):
770 if tdata
[i
][k
] == "x":
776 tdata
.append(data
[:])
778 for j_data
in wdata
[i
]:
779 if j_data
["A"] != addr
:
785 for k
in range(width
):
790 tdata
.append(data
[:])
792 assert len(tdata
) == len(rdata
)
795 netpath
[-1] += "<%0*x>" % ((len(addr
)+3) // 4, int(addr
, 2))
796 vcd
.add_net([topmod
] + netpath
, width
)
798 for i
in range(steps_start
, steps_stop
):
799 if i
not in mem_trace_data
:
800 mem_trace_data
[i
] = list()
801 mem_trace_data
[i
].append((netpath
, "".join(tdata
[i
-steps_start
])))
803 for i
in range(steps_start
, steps_stop
):
805 value_list
= smt
.get_net_bin_list(topmod
, path_list
, "s%d" % i
)
806 for path
, value
in zip(path_list
, value_list
):
807 vcd
.set_net([topmod
] + path
, value
)
808 if i
in mem_trace_data
:
809 for path
, value
in mem_trace_data
[i
]:
810 vcd
.set_net([topmod
] + path
, value
)
812 vcd
.set_time(steps_stop
)
815 def write_vlogtb_trace(steps_start
, steps_stop
, index
):
816 filename
= vlogtbfile
.replace("%", index
)
817 print_msg("Writing trace to Verilog testbench: %s" % (filename
))
819 vlogtb_topmod
= topmod
820 vlogtb_state
= "s@@step_idx@@"
822 if vlogtbtop
is not None:
823 for item
in vlogtbtop
.split("."):
824 if item
in smt
.modinfo
[vlogtb_topmod
].cells
:
825 vlogtb_state
= "(|%s_h %s| %s)" % (vlogtb_topmod
, item
, vlogtb_state
)
826 vlogtb_topmod
= smt
.modinfo
[vlogtb_topmod
].cells
[item
]
828 print_msg("Vlog top module '%s' not found: no cell '%s' in module '%s'" % (vlogtbtop
, item
, vlogtb_topmod
))
831 with
open(filename
, "w") as f
:
832 print("`ifndef VERILATOR", file=f
)
833 print("module testbench;", file=f
)
834 print(" reg [4095:0] vcdfile;", file=f
)
835 print(" reg clock;", file=f
)
836 print("`else", file=f
)
837 print("module testbench(input clock, output reg genclock);", file=f
)
838 print(" initial genclock = 1;", file=f
)
839 print("`endif", file=f
)
841 print(" reg genclock = 1;", file=f
)
842 print(" reg [31:0] cycle = 0;", file=f
)
844 primary_inputs
= list()
847 for name
in smt
.modinfo
[vlogtb_topmod
].inputs
:
848 if name
in ["clk", "clock", "CLK", "CLOCK"]:
849 clock_inputs
.add(name
)
850 width
= smt
.modinfo
[vlogtb_topmod
].wsize
[name
]
851 primary_inputs
.append((name
, width
))
853 for name
, width
in primary_inputs
:
854 if name
in clock_inputs
:
855 print(" wire [%d:0] PI_%s = clock;" % (width
-1, name
), file=f
)
857 print(" reg [%d:0] PI_%s;" % (width
-1, name
), file=f
)
859 print(" %s UUT (" % vlogtb_topmod
, file=f
)
860 print(",\n".join(" .{name}(PI_{name})".format(name
=name
) for name
, _
in primary_inputs
), file=f
)
863 print("`ifndef VERILATOR", file=f
)
864 print(" initial begin", file=f
)
865 print(" if ($value$plusargs(\"vcd=%s\", vcdfile)) begin", file=f
)
866 print(" $dumpfile(vcdfile);", file=f
)
867 print(" $dumpvars(0, testbench);", file=f
)
868 print(" end", file=f
)
869 print(" #5 clock = 0;", file=f
)
870 print(" while (genclock) begin", file=f
)
871 print(" #5 clock = 0;", file=f
)
872 print(" #5 clock = 1;", file=f
)
873 print(" end", file=f
)
874 print(" end", file=f
)
875 print("`endif", file=f
)
877 print(" initial begin", file=f
)
879 regs
= sorted(smt
.hiernets(vlogtb_topmod
, regs_only
=True))
880 regvals
= smt
.get_net_bin_list(vlogtb_topmod
, regs
, vlogtb_state
.replace("@@step_idx@@", str(steps_start
)))
882 print("`ifndef VERILATOR", file=f
)
883 print(" #1;", file=f
)
884 print("`endif", file=f
)
885 for reg
, val
in zip(regs
, regvals
):
888 if n
.startswith("$"):
890 print(" %sUUT.%s = %d'b%s;" % ("// " if hidden_net
else "", ".".join(reg
), len(val
), val
), file=f
)
892 anyconsts
= sorted(smt
.hieranyconsts(vlogtb_topmod
))
893 for info
in anyconsts
:
894 if info
[3] is not None:
895 modstate
= smt
.net_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(steps_start
)), info
[0])
896 value
= smt
.bv2bin(smt
.get("(|%s| %s)" % (info
[1], modstate
)))
897 print(" UUT.%s = %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
899 mems
= sorted(smt
.hiermems(vlogtb_topmod
))
901 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(vlogtb_topmod
, mempath
)
903 addr_expr_list
= list()
904 data_expr_list
= list()
905 for i
in range(steps_start
, steps_stop
):
906 for j
in range(rports
):
907 addr_expr_list
.append(smt
.mem_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dA" % j
))
908 data_expr_list
.append(smt
.mem_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dD" % j
))
910 addr_list
= smt
.get_list(addr_expr_list
)
911 data_list
= smt
.get_list(data_expr_list
)
914 for addr
, data
in zip(addr_list
, data_list
):
915 addr
= smt
.bv2bin(addr
)
916 data
= smt
.bv2bin(data
)
917 if addr
not in addr_data
:
918 addr_data
[addr
] = data
920 for addr
, data
in addr_data
.items():
921 print(" UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath
), len(addr
), addr
, len(data
), data
), file=f
)
924 anyseqs
= sorted(smt
.hieranyseqs(vlogtb_topmod
))
926 for i
in range(steps_start
, steps_stop
):
927 pi_names
= [[name
] for name
, _
in primary_inputs
if name
not in clock_inputs
]
928 pi_values
= smt
.get_net_bin_list(vlogtb_topmod
, pi_names
, vlogtb_state
.replace("@@step_idx@@", str(i
)))
930 print(" // state %d" % i
, file=f
)
933 print(" if (cycle == %d) begin" % (i
-1), file=f
)
935 for name
, val
in zip(pi_names
, pi_values
):
937 print(" PI_%s <= %d'b%s;" % (".".join(name
), len(val
), val
), file=f
)
939 print(" PI_%s = %d'b%s;" % (".".join(name
), len(val
), val
), file=f
)
942 if info
[3] is not None:
943 modstate
= smt
.net_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), info
[0])
944 value
= smt
.bv2bin(smt
.get("(|%s| %s)" % (info
[1], modstate
)))
946 print(" UUT.%s <= %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
948 print(" UUT.%s = %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
951 print(" end", file=f
)
955 print(" end", file=f
)
956 print(" always @(posedge clock) begin", file=f
)
958 print(" genclock <= cycle < %d;" % (steps_stop
-1), file=f
)
959 print(" cycle <= cycle + 1;", file=f
)
960 print(" end", file=f
)
962 print("endmodule", file=f
)
965 def write_constr_trace(steps_start
, steps_stop
, index
):
966 filename
= outconstr
.replace("%", index
)
967 print_msg("Writing trace to constraints file: %s" % (filename
))
969 constr_topmod
= topmod
970 constr_state
= "s@@step_idx@@"
973 if smtctop
is not None:
974 for item
in smtctop
[0].split("."):
975 assert item
in smt
.modinfo
[constr_topmod
].cells
976 constr_state
= "(|%s_h %s| %s)" % (constr_topmod
, item
, constr_state
)
977 constr_topmod
= smt
.modinfo
[constr_topmod
].cells
[item
]
979 constr_prefix
= smtctop
[1] + "."
982 steps_start
= steps_stop
- 1
984 with
open(filename
, "w") as f
:
985 primary_inputs
= list()
987 for name
in smt
.modinfo
[constr_topmod
].inputs
:
988 width
= smt
.modinfo
[constr_topmod
].wsize
[name
]
989 primary_inputs
.append((name
, width
))
991 if steps_start
== 0 or smtcinit
:
992 print("initial", file=f
)
994 print("state %d" % steps_start
, file=f
)
996 regnames
= sorted(smt
.hiernets(constr_topmod
, regs_only
=True))
997 regvals
= smt
.get_net_list(constr_topmod
, regnames
, constr_state
.replace("@@step_idx@@", str(steps_start
)))
999 for name
, val
in zip(regnames
, regvals
):
1000 print("assume (= [%s%s] %s)" % (constr_prefix
, ".".join(name
), val
), file=f
)
1002 mems
= sorted(smt
.hiermems(constr_topmod
))
1003 for mempath
in mems
:
1004 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(constr_topmod
, mempath
)
1006 addr_expr_list
= list()
1007 data_expr_list
= list()
1008 for i
in range(steps_start
, steps_stop
):
1009 for j
in range(rports
):
1010 addr_expr_list
.append(smt
.mem_expr(constr_topmod
, constr_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dA" % j
))
1011 data_expr_list
.append(smt
.mem_expr(constr_topmod
, constr_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dD" % j
))
1013 addr_list
= smt
.get_list(addr_expr_list
)
1014 data_list
= smt
.get_list(data_expr_list
)
1017 for addr
, data
in zip(addr_list
, data_list
):
1018 if addr
not in addr_data
:
1019 addr_data
[addr
] = data
1021 for addr
, data
in addr_data
.items():
1022 print("assume (= (select [%s%s] %s) %s)" % (constr_prefix
, ".".join(mempath
), addr
, data
), file=f
)
1024 for k
in range(steps_start
, steps_stop
):
1027 print("state %d" % k
, file=f
)
1029 pi_names
= [[name
] for name
, _
in sorted(primary_inputs
)]
1030 pi_values
= smt
.get_net_list(constr_topmod
, pi_names
, constr_state
.replace("@@step_idx@@", str(k
)))
1032 for name
, val
in zip(pi_names
, pi_values
):
1033 print("assume (= [%s%s] %s)" % (constr_prefix
, ".".join(name
), val
), file=f
)
1036 def write_trace(steps_start
, steps_stop
, index
):
1037 if vcdfile
is not None:
1038 write_vcd_trace(steps_start
, steps_stop
, index
)
1040 if vlogtbfile
is not None:
1041 write_vlogtb_trace(steps_start
, steps_stop
, index
)
1043 if outconstr
is not None:
1044 write_constr_trace(steps_start
, steps_stop
, index
)
1047 def print_failed_asserts_worker(mod
, state
, path
, extrainfo
):
1048 assert mod
in smt
.modinfo
1049 found_failed_assert
= False
1051 if smt
.get("(|%s_a| %s)" % (mod
, state
)) in ["true", "#b1"]:
1054 for cellname
, celltype
in smt
.modinfo
[mod
].cells
.items():
1055 if print_failed_asserts_worker(celltype
, "(|%s_h %s| %s)" % (mod
, cellname
, state
), path
+ "." + cellname
, extrainfo
):
1056 found_failed_assert
= True
1058 for assertfun
, assertinfo
in smt
.modinfo
[mod
].asserts
.items():
1059 if smt
.get("(|%s| %s)" % (assertfun
, state
)) in ["false", "#b0"]:
1060 print_msg("Assert failed in %s: %s%s" % (path
, assertinfo
, extrainfo
))
1061 found_failed_assert
= True
1063 return found_failed_assert
1066 def print_failed_asserts(state
, final
=False, extrainfo
=""):
1068 loc_list
, expr_list
, value_list
= get_constr_expr(constr_asserts
, state
, final
=final
, getvalues
=True)
1069 found_failed_assert
= False
1071 for loc
, expr
, value
in zip(loc_list
, expr_list
, value_list
):
1072 if smt
.bv2int(value
) == 0:
1073 print_msg("Assert %s failed: %s%s" % (loc
, expr
, extrainfo
))
1074 found_failed_assert
= True
1077 if print_failed_asserts_worker(topmod
, "s%d" % state
, topmod
, extrainfo
):
1078 found_failed_assert
= True
1080 return found_failed_assert
1083 def print_anyconsts_worker(mod
, state
, path
):
1084 assert mod
in smt
.modinfo
1086 for cellname
, celltype
in smt
.modinfo
[mod
].cells
.items():
1087 print_anyconsts_worker(celltype
, "(|%s_h %s| %s)" % (mod
, cellname
, state
), path
+ "." + cellname
)
1089 for fun
, info
in smt
.modinfo
[mod
].anyconsts
.items():
1091 print_msg("Value for anyconst in %s (%s): %d" % (path
, info
[0], smt
.bv2int(smt
.get("(|%s| %s)" % (fun
, state
)))))
1093 print_msg("Value for anyconst %s.%s (%s): %d" % (path
, info
[1], info
[0], smt
.bv2int(smt
.get("(|%s| %s)" % (fun
, state
)))))
1096 def print_anyconsts(state
):
1098 print_anyconsts_worker(topmod
, "s%d" % state
, topmod
)
1101 def get_cover_list(mod
, base
):
1102 assert mod
in smt
.modinfo
1107 for expr
, desc
in smt
.modinfo
[mod
].covers
.items():
1108 cover_expr
.append("(ite (|%s| %s) #b1 #b0)" % (expr
, base
))
1109 cover_desc
.append(desc
)
1111 for cell
, submod
in smt
.modinfo
[mod
].cells
.items():
1112 e
, d
= get_cover_list(submod
, "(|%s_h %s| %s)" % (mod
, cell
, base
))
1116 return cover_expr
, cover_desc
1119 asserts_antecedent_cache
= [list()]
1120 asserts_consequent_cache
= [list()]
1121 asserts_cache_dirty
= False
1123 def smt_state(step
):
1124 smt
.write("(declare-fun s%d () |%s_s|)" % (step
, topmod
))
1125 states
.append("s%d" % step
)
1127 def smt_assert(expr
):
1131 smt
.write("(assert %s)" % expr
)
1133 def smt_assert_antecedent(expr
):
1137 smt
.write("(assert %s)" % expr
)
1139 global asserts_cache_dirty
1140 asserts_cache_dirty
= True
1141 asserts_antecedent_cache
[-1].append(expr
)
1143 def smt_assert_consequent(expr
):
1147 smt
.write("(assert %s)" % expr
)
1149 global asserts_cache_dirty
1150 asserts_cache_dirty
= True
1151 asserts_consequent_cache
[-1].append(expr
)
1153 def smt_forall_assert():
1157 global asserts_cache_dirty
1158 asserts_cache_dirty
= False
1160 assert (len(smt
.modinfo
[topmod
].maximize
) + len(smt
.modinfo
[topmod
].minimize
) <= 1)
1162 def make_assert_expr(asserts_cache
):
1164 for lst
in asserts_cache
:
1167 assert len(expr
) != 0
1172 expr
= "(and %s)" % (" ".join(expr
))
1175 antecedent_expr
= make_assert_expr(asserts_antecedent_cache
)
1176 consequent_expr
= make_assert_expr(asserts_consequent_cache
)
1178 states_db
= set(states
)
1179 used_states_db
= set()
1180 new_antecedent_expr
= list()
1181 new_consequent_expr
= list()
1182 assert_expr
= list()
1184 def make_new_expr(new_expr
, expr
):
1186 while cursor
< len(expr
):
1188 if expr
[cursor
] in '|"':
1189 while cursor
+l
+1 < len(expr
) and expr
[cursor
] != expr
[cursor
+l
]:
1192 elif expr
[cursor
] not in '() ':
1193 while cursor
+l
< len(expr
) and expr
[cursor
+l
] not in '|"() ':
1196 word
= expr
[cursor
:cursor
+l
]
1197 if word
in states_db
:
1198 used_states_db
.add(word
)
1201 new_expr
.append(word
)
1204 make_new_expr(new_antecedent_expr
, antecedent_expr
)
1205 make_new_expr(new_consequent_expr
, consequent_expr
)
1207 new_antecedent_expr
= ["".join(new_antecedent_expr
)]
1208 new_consequent_expr
= ["".join(new_consequent_expr
)]
1210 if states
[0] in used_states_db
:
1211 new_antecedent_expr
.append("(|%s_ex_state_eq| %s %s_)" % (topmod
, states
[0], states
[0]))
1213 if s
in used_states_db
:
1214 new_antecedent_expr
.append("(|%s_ex_input_eq| %s %s_)" % (topmod
, s
, s
))
1216 if len(new_antecedent_expr
) == 0:
1217 new_antecedent_expr
= "true"
1218 elif len(new_antecedent_expr
) == 1:
1219 new_antecedent_expr
= new_antecedent_expr
[0]
1221 new_antecedent_expr
= "(and %s)" % (" ".join(new_antecedent_expr
))
1223 if len(new_consequent_expr
) == 0:
1224 new_consequent_expr
= "true"
1225 elif len(new_consequent_expr
) == 1:
1226 new_consequent_expr
= new_consequent_expr
[0]
1228 new_consequent_expr
= "(and %s)" % (" ".join(new_consequent_expr
))
1230 assert_expr
.append("(assert (forall (")
1233 if s
in used_states_db
:
1234 assert_expr
.append("%s(%s_ |%s_s|)" % ("" if first_state
else " ", s
, topmod
))
1236 assert_expr
.append(") (=> %s %s)))" % (new_antecedent_expr
, new_consequent_expr
))
1238 smt
.write("".join(assert_expr
))
1240 if len(smt
.modinfo
[topmod
].maximize
) > 0:
1242 if s
in used_states_db
:
1243 smt
.write("(maximize (|%s| %s))\n" % (smt
.modinfo
[topmod
].maximize
.copy().pop(), s
))
1246 if len(smt
.modinfo
[topmod
].minimize
) > 0:
1248 if s
in used_states_db
:
1249 smt
.write("(minimize (|%s| %s))\n" % (smt
.modinfo
[topmod
].minimize
.copy().pop(), s
))
1253 global asserts_cache_dirty
1254 asserts_cache_dirty
= True
1255 asserts_antecedent_cache
.append(list())
1256 asserts_consequent_cache
.append(list())
1257 smt
.write("(push 1)")
1260 global asserts_cache_dirty
1261 asserts_cache_dirty
= True
1262 asserts_antecedent_cache
.pop()
1263 asserts_consequent_cache
.pop()
1264 smt
.write("(pop 1)")
1266 def smt_check_sat():
1267 if asserts_cache_dirty
:
1269 return smt
.check_sat()
1272 retstatus
= "FAILED"
1273 skip_counter
= step_size
1274 for step
in range(num_steps
, -1, -1):
1276 print_msg("Temporal induction not supported for exists-forall problems.")
1280 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1281 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1282 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1283 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1285 if step
== num_steps
:
1286 smt_assert("(not (and (|%s_a| s%d) %s))" % (topmod
, step
, get_constr_expr(constr_asserts
, step
)))
1289 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
, step
+1))
1290 smt_assert("(|%s_a| s%d)" % (topmod
, step
))
1291 smt_assert(get_constr_expr(constr_asserts
, step
))
1293 if step
> num_steps
-skip_steps
:
1294 print_msg("Skipping induction in step %d.." % (step
))
1298 if skip_counter
< step_size
:
1299 print_msg("Skipping induction in step %d.." % (step
))
1303 print_msg("Trying induction in step %d.." % (step
))
1305 if smt_check_sat() == "sat":
1307 print_msg("Temporal induction failed!")
1308 print_anyconsts(num_steps
)
1309 print_failed_asserts(num_steps
)
1310 write_trace(step
, num_steps
+1, '%')
1313 print_anyconsts(num_steps
)
1314 print_failed_asserts(num_steps
)
1315 write_trace(step
, num_steps
+1, "%d" % step
)
1318 print_msg("Temporal induction successful.")
1319 retstatus
= "PASSED"
1323 cover_expr
, cover_desc
= get_cover_list(topmod
, "state")
1324 cover_mask
= "1" * len(cover_desc
)
1326 if len(cover_expr
) > 1:
1327 cover_expr
= "(concat %s)" % " ".join(cover_expr
)
1328 elif len(cover_expr
) == 1:
1329 cover_expr
= cover_expr
[0]
1334 smt
.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod
, len(cover_desc
), cover_expr
))
1337 retstatus
= "FAILED"
1338 found_failed_assert
= False
1340 assert step_size
== 1
1342 while step
< num_steps
:
1344 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1345 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1346 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1350 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1352 smt_assert_antecedent("(|%s_i| s0)" % (topmod
))
1353 smt_assert_antecedent("(|%s_is| s0)" % (topmod
))
1356 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
-1, step
))
1357 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1359 while "1" in cover_mask
:
1360 print_msg("Checking cover reachability in step %d.." % (step
))
1362 smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx
, step
, "0" * len(cover_desc
)))
1364 if smt_check_sat() == "unsat":
1368 if append_steps
> 0:
1369 for i
in range(step
+1, 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 print_msg("Re-solving with appended steps..")
1378 if smt_check_sat() == "unsat":
1379 print("%s Cannot appended steps without violating assumptions!" % smt
.timestamp())
1380 found_failed_assert
= True
1381 retstatus
= "FAILED"
1384 reached_covers
= smt
.bv2bin(smt
.get("(covers_%d s%d)" % (coveridx
, step
)))
1385 assert len(reached_covers
) == len(cover_desc
)
1389 for i
in range(len(reached_covers
)):
1390 if reached_covers
[i
] == "0":
1391 new_cover_mask
.append(cover_mask
[i
])
1394 print_msg("Reached cover statement at %s in step %d." % (cover_desc
[i
], step
))
1395 new_cover_mask
.append("0")
1397 cover_mask
= "".join(new_cover_mask
)
1399 for i
in range(step
+1+append_steps
):
1400 if print_failed_asserts(i
, extrainfo
=" (step %d)" % i
):
1401 found_failed_assert
= True
1403 write_trace(0, step
+1+append_steps
, "%d" % coveridx
)
1405 if found_failed_assert
:
1410 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 if found_failed_assert
:
1415 if "1" not in cover_mask
:
1416 retstatus
= "PASSED"
1421 if "1" in cover_mask
:
1422 for i
in range(len(cover_mask
)):
1423 if cover_mask
[i
] == "1":
1424 print_msg("Unreached cover statement at %s." % cover_desc
[i
])
1426 else: # not tempind, covermode
1428 retstatus
= "PASSED"
1429 while step
< num_steps
:
1431 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1432 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1433 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1437 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1439 smt_assert_antecedent("(|%s_i| s0)" % (topmod
))
1440 smt_assert_antecedent("(|%s_is| s0)" % (topmod
))
1443 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
-1, step
))
1444 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1446 if step
< skip_steps
:
1447 if assume_skipped
is not None and step
>= assume_skipped
:
1448 print_msg("Skipping step %d (and assuming pass).." % (step
))
1449 smt_assert("(|%s_a| s%d)" % (topmod
, step
))
1450 smt_assert(get_constr_expr(constr_asserts
, step
))
1452 print_msg("Skipping step %d.." % (step
))
1456 last_check_step
= step
1457 for i
in range(1, step_size
):
1458 if step
+i
< num_steps
:
1460 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
+i
))
1461 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
+i
))
1462 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
+i
))
1463 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
+i
-1, step
+i
))
1464 smt_assert_consequent(get_constr_expr(constr_assumes
, step
+i
))
1465 last_check_step
= step
+i
1469 if last_check_step
== step
:
1470 print_msg("Checking assumptions in step %d.." % (step
))
1472 print_msg("Checking assumptions in steps %d to %d.." % (step
, last_check_step
))
1474 if smt_check_sat() == "unsat":
1475 print("%s Assumptions are unsatisfiable!" % smt
.timestamp())
1476 retstatus
= "PREUNSAT"
1480 if last_check_step
== step
:
1481 print_msg("Checking assertions in step %d.." % (step
))
1483 print_msg("Checking assertions in steps %d to %d.." % (step
, last_check_step
))
1486 smt_assert("(not (and %s))" % " ".join(["(|%s_a| s%d)" % (topmod
, i
) for i
in range(step
, last_check_step
+1)] +
1487 [get_constr_expr(constr_asserts
, i
) for i
in range(step
, last_check_step
+1)]))
1489 if smt_check_sat() == "sat":
1490 print("%s BMC failed!" % smt
.timestamp())
1491 if append_steps
> 0:
1492 for i
in range(last_check_step
+1, last_check_step
+1+append_steps
):
1493 print_msg("Appending additional step %d." % i
)
1495 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, i
))
1496 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, i
))
1497 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, i
))
1498 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, i
-1, i
))
1499 smt_assert_consequent(get_constr_expr(constr_assumes
, i
))
1500 print_msg("Re-solving with appended steps..")
1501 if smt_check_sat() == "unsat":
1502 print("%s Cannot appended steps without violating assumptions!" % smt
.timestamp())
1503 retstatus
= "FAILED"
1505 print_anyconsts(step
)
1506 for i
in range(step
, last_check_step
+1):
1507 print_failed_asserts(i
)
1508 write_trace(0, last_check_step
+1+append_steps
, '%')
1509 retstatus
= "FAILED"
1514 if (constr_final_start
is not None) or (last_check_step
+1 != num_steps
):
1515 for i
in range(step
, last_check_step
+1):
1516 smt_assert("(|%s_a| s%d)" % (topmod
, i
))
1517 smt_assert(get_constr_expr(constr_asserts
, i
))
1519 if constr_final_start
is not None:
1520 for i
in range(step
, last_check_step
+1):
1521 if i
< constr_final_start
:
1524 print_msg("Checking final constraints in step %d.." % (i
))
1527 smt_assert_consequent(get_constr_expr(constr_assumes
, i
, final
=True))
1528 smt_assert("(not %s)" % get_constr_expr(constr_asserts
, i
, final
=True))
1530 if smt_check_sat() == "sat":
1531 print("%s BMC failed!" % smt
.timestamp())
1533 print_failed_asserts(i
, final
=True)
1534 write_trace(0, i
+1, '%')
1535 retstatus
= "FAILED"
1543 for i
in range(step
, last_check_step
+1):
1544 smt_assert("(|%s_a| s%d)" % (topmod
, i
))
1545 smt_assert(get_constr_expr(constr_asserts
, i
))
1547 print_msg("Solving for step %d.." % (last_check_step
))
1548 if smt_check_sat() != "sat":
1549 print("%s No solution found!" % smt
.timestamp())
1550 retstatus
= "FAILED"
1555 write_trace(0, last_check_step
+1, "%d" % step
)
1559 if gentrace
and retstatus
:
1561 write_trace(0, num_steps
, '%')
1567 print_msg("Status: %s" % retstatus
)
1568 sys
.exit(0 if retstatus
== "PASSED" else 1)