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
57 yosys-smtbmc [options] <yosys_smt2_output>
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
65 generate an arbitrary trace that satisfies
66 all assertions and assumptions.
69 instead of BMC run temporal induction
72 instead of regular BMC run cover analysis
75 name of the top module
77 --smtc <constr_filename>
81 read cex file as written by ABC's "write_cex -n"
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.
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).
93 the AIGER witness file does not include the status and
96 --btorwit <btor_witness_filename>
100 only run the core proof, do not collect and print any
101 additional information (e.g. which assert failed)
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
111 only check final constraints, assume base case
113 --assume-skipped <start_step>
114 assume asserts in skipped steps in BMC.
115 no assumptions are created for skipped steps
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)
123 --dump-vlogtb <verilog_filename>
124 write trace as Verilog test bench
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.
131 --dump-smtc <constr_filename>
132 write trace as constraints file
135 write just the last state as initial constraint to smtc file
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.
142 do not assume initial conditions in state 0
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.
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)
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"])
170 num_steps
= int(a
[0])
172 skip_steps
= int(a
[0])
173 num_steps
= int(a
[1])
175 skip_steps
= int(a
[0])
176 step_size
= int(a
[1])
177 num_steps
= int(a
[2])
180 elif o
== "--assume-skipped":
181 assume_skipped
= int(a
)
182 elif o
== "--final-only":
190 aimfile
, aiwfile
= a
.split(":")
194 elif o
== "--aig-noheader":
196 elif o
== "--btorwit":
198 elif o
== "--dump-vcd":
200 elif o
== "--dump-vlogtb":
202 elif o
== "--vlogtb-top":
204 elif o
== "--dump-smtc":
206 elif o
== "--smtc-init":
208 elif o
== "--smtc-top":
209 smtctop
= a
.split(":")
210 if len(smtctop
) == 1:
212 assert len(smtctop
) == 2
213 smtctop
= tuple(smtctop
)
214 elif o
== "--dump-all":
216 elif o
== "--presat":
218 elif o
== "--noinfo":
220 elif o
== "--noinit":
222 elif o
== "--append":
223 append_steps
= int(a
)
232 elif so
.handle(o
, a
):
240 if sum([tempind
, gentrace
, covermode
]) > 1:
243 constr_final_start
= None
244 constr_asserts
= defaultdict(list)
245 constr_assumes
= defaultdict(list)
246 constr_write
= list()
249 current_states
= None
252 with
open(fn
, "r") as f
:
256 if line
.startswith("#"):
259 tokens
= line
.split()
264 if tokens
[0] == "initial":
265 current_states
= set()
267 current_states
.add(0)
270 if tokens
[0] == "final":
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
)
283 if tokens
[0] == "state":
284 current_states
= set()
286 for token
in tokens
[1:]:
287 tok
= token
.split(":")
289 current_states
.add(int(token
))
296 for i
in range(lower
, upper
+1):
297 current_states
.add(i
)
302 if tokens
[0] == "always":
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))
312 if tokens
[0] == "assert":
313 assert current_states
is not None
315 for state
in current_states
:
316 constr_asserts
[state
].append(("%s:%d" % (fn
, current_line
), " ".join(tokens
[1:])))
320 if tokens
[0] == "assume":
321 assert current_states
is not None
323 for state
in current_states
:
324 constr_assumes
[state
].append(("%s:%d" % (fn
, current_line
), " ".join(tokens
[1:])))
328 if tokens
[0] == "write":
329 constr_write
.append(" ".join(tokens
[1:]))
332 if tokens
[0] == "logic":
333 so
.logic
= " ".join(tokens
[1:])
339 def get_constr_expr(db
, state
, final
=False, getvalues
=False):
341 if ("final-%d" % state
) not in db
:
342 return ([], [], []) if getvalues
else "true"
345 return ([], [], []) if getvalues
else "true"
347 netref_regex
= re
.compile(r
'(^|[( ])\[(-?[0-9]+:|)([^\]]*|\S*)\](?=[ )]|$)')
349 def replace_netref(match
):
350 state_sel
= match
.group(2)
354 elif state_sel
[0] == "-":
355 st
= state
+ int(state_sel
[:-1])
357 st
= int(state_sel
[:-1])
359 expr
= smt
.net_expr(topmod
, "s%d" % st
, smt
.get_path(topmod
, match
.group(3)))
361 return match
.group(1) + expr
364 for loc
, expr
in db
[("final-%d" % state
) if final
else state
]:
365 actual_expr
= netref_regex
.sub(replace_netref
, expr
)
367 expr_list
.append((loc
, expr
, actual_expr
))
369 expr_list
.append(actual_expr
)
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
376 if len(expr_list
) == 0:
379 if len(expr_list
) == 1:
382 return "(and %s)" % " ".join(expr_list
)
387 if noinfo
and vcdfile
is None and vlogtbfile
is None and outconstr
is None:
388 smt
.produce_models
= False
391 print("%s %s" % (smt
.timestamp(), msg
))
394 print_msg("Solver: %s" % (so
.solver
))
396 with
open(args
[0], "r") as f
:
400 for line
in constr_write
:
406 assert topmod
is not None
407 assert topmod
in smt
.modinfo
409 if cexfile
is not None:
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
)
421 name
, bit
, extra_name
, step
, val
= match
.group(1), match
.group(2), match
.group(3), match
.group(4), match
.group(5)
426 if name
not in smt
.modinfo
[topmod
].inputs
:
437 if smt
.modinfo
[topmod
].wsize
[name
] == 1:
439 smtexpr
= "(= [%s] %s)" % (name
, "true" if val
else "false")
441 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bit
, bit
, name
, val
)
443 # print("cex@%d: %s" % (step, smtexpr))
444 constr_assumes
[step
].append((cexfile
, smtexpr
))
447 skip_steps
= max(skip_steps
, step
)
448 num_steps
= max(num_steps
, step
+1)
450 if aimfile
is not None:
460 with
open(aimfile
, "r") as f
:
461 for entry
in f
.read().splitlines():
462 entry
= entry
.split()
464 if entry
[0] == "input":
465 input_map
[int(entry
[1])] = (entry
[3], int(entry
[2]))
468 if entry
[0] == "init":
469 init_map
[int(entry
[1])] = (entry
[3], int(entry
[2]))
472 if entry
[0] in ["latch", "invlatch"]:
473 latch_map
[int(entry
[1])] = (entry
[3], int(entry
[2]), entry
[0] == "invlatch")
476 if entry
[0] in ["output", "wire"]:
481 with
open(aiwfile
, "r") as f
:
489 for entry
in f
.read().splitlines():
490 if len(entry
) == 0 or entry
[0] in "bcjfu.":
500 if len(init_map
) == 0:
501 for i
in range(len(entry
)):
506 value
= int(entry
[i
])
507 name
= latch_map
[i
][0]
508 bitidx
= latch_map
[i
][1]
509 invert
= latch_map
[i
][2]
514 path
= smt
.get_path(topmod
, name
)
515 width
= smt
.net_width(topmod
, path
)
519 smtexpr
= "(= [%s] %s)" % (name
, "true" if value
else "false")
521 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx
, bitidx
, name
, value
)
523 constr_assumes
[0].append((cexfile
, smtexpr
))
526 for i
in range(len(entry
)):
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]
535 path
= smt
.get_path(topmod
, name
)
537 if not smt
.net_exists(topmod
, path
):
538 match
= re
.match(r
"(.*)\[(\d+)\]$", path
[-1])
540 path
[-1] = match
.group(1)
541 addr
= int(match
.group(2))
543 if not match
or not smt
.mem_exists(topmod
, path
):
544 print_msg("Ignoring init value for unknown net: %s" % (name
))
547 meminfo
= smt
.mem_info(topmod
, path
)
548 smtexpr
= "(select [%s] #b%s)" % (".".join(path
), bin(addr
)[2:].zfill(meminfo
[0]))
552 smtexpr
= "[%s]" % name
553 width
= smt
.net_width(topmod
, path
)
557 smtexpr
= "(= %s %s)" % (smtexpr
, "true" if value
else "false")
559 smtexpr
= "(= ((_ extract %d %d) %s) #b%d)" % (bitidx
, bitidx
, smtexpr
, value
)
561 constr_assumes
[0].append((cexfile
, smtexpr
))
564 value
= int(entry
[i
])
565 name
= input_map
[i
][0]
566 bitidx
= input_map
[i
][1]
568 path
= smt
.get_path(topmod
, name
)
569 width
= smt
.net_width(topmod
, path
)
573 smtexpr
= "(= [%s] %s)" % (name
, "true" if value
else "false")
575 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx
, bitidx
, name
, value
)
577 constr_assumes
[step
].append((cexfile
, smtexpr
))
580 skip_steps
= max(skip_steps
, step
)
581 num_steps
= max(num_steps
, step
+1)
584 if btorwitfile
is not None:
585 with
open(btorwitfile
, "r") as f
:
601 if line
== "" or line
[0] == "b" or line
[0] == "j":
607 if line
[0] == '#' or line
[0] == '@':
612 altsuffix
= "#" + suffix
[1:]
614 altsuffix
= "@" + suffix
[1:]
622 if line
[-1].endswith(suffix
):
623 line
[-1] = line
[-1][0:len(line
[-1]) - len(suffix
)]
625 if line
[-1].endswith(altsuffix
):
626 line
[-1] = line
[-1][0:len(line
[-1]) - len(altsuffix
)]
628 if line
[-1][0] == "$":
632 if len(line
) == 3 and line
[1][0] != "[":
636 path
= smt
.get_path(topmod
, name
)
638 if not smt
.net_exists(topmod
, path
):
641 width
= smt
.net_width(topmod
, path
)
644 assert value
in ["0", "1"]
645 value
= "true" if value
== "1" else "false"
649 smtexpr
= "(= [%s] %s)" % (name
, value
)
650 constr_assumes
[step
].append((btorwitfile
, smtexpr
))
653 if len(line
) == 4 and line
[1][0] == "[":
658 path
= smt
.get_path(topmod
, name
)
660 if not smt
.mem_exists(topmod
, path
):
663 meminfo
= smt
.mem_info(topmod
, path
)
666 assert value
in ["0", "1"]
667 value
= "true" if value
== "1" else "false"
671 assert index
[0] == "["
672 assert index
[-1] == "]"
673 index
= "#b" + index
[1:-1]
675 smtexpr
= "(= (select [%s] %s) %s)" % (name
, index
, value
)
676 constr_assumes
[step
].append((btorwitfile
, smtexpr
))
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
))
685 with
open(filename
, "w") as vcd_file
:
686 vcd
= MkVcd(vcd_file
)
689 for netpath
in sorted(smt
.hiernets(topmod
)):
692 if n
.startswith("$"):
695 edge
= smt
.net_clock(topmod
, netpath
)
697 vcd
.add_net([topmod
] + netpath
, smt
.net_width(topmod
, netpath
))
699 vcd
.add_clock([topmod
] + netpath
, edge
)
700 path_list
.append(netpath
)
702 mem_trace_data
= dict()
703 for mempath
in sorted(smt
.hiermems(topmod
)):
704 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(topmod
, mempath
)
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
))
726 for eid
, edat
in zip(expr_id
, smt
.get_list(expr_list
)):
744 c
[f
] = smt
.bv2bin(edat
)
754 if len(wdata
) == 0 and len(rdata
) != 0:
755 wdata
= [[]] * len(rdata
)
757 assert len(rdata
) == len(wdata
)
759 for i
in range(len(wdata
)):
761 for j_data
in rdata
[i
]:
762 if j_data
["A"] == addr
:
763 data
= list(j_data
["D"])
769 for i
in reversed(range(len(tdata
))):
770 for k
in range(width
):
771 if tdata
[i
][k
] == "x":
777 tdata
.append(data
[:])
779 for j_data
in wdata
[i
]:
780 if j_data
["A"] != addr
:
786 for k
in range(width
):
791 tdata
.append(data
[:])
793 assert len(tdata
) == len(rdata
)
796 netpath
[-1] += "<%0*x>" % ((len(addr
)+3) // 4, int(addr
, 2))
797 vcd
.add_net([topmod
] + netpath
, width
)
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
])))
804 for i
in range(steps_start
, steps_stop
):
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
)
813 vcd
.set_time(steps_stop
)
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
))
820 vlogtb_topmod
= topmod
821 vlogtb_state
= "s@@step_idx@@"
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
]
829 print_msg("Vlog top module '%s' not found: no cell '%s' in module '%s'" % (vlogtbtop
, item
, vlogtb_topmod
))
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
)
842 print(" reg genclock = 1;", file=f
)
843 print(" reg [31:0] cycle = 0;", file=f
)
845 primary_inputs
= list()
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
))
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
)
858 print(" reg [%d:0] PI_%s;" % (width
-1, name
), file=f
)
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
)
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
)
878 print(" initial begin", file=f
)
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
)))
883 print("`ifndef VERILATOR", file=f
)
884 print(" #1;", file=f
)
885 print("`endif", file=f
)
886 for reg
, val
in zip(regs
, regvals
):
889 if n
.startswith("$"):
891 print(" %sUUT.%s = %d'b%s;" % ("// " if hidden_net
else "", ".".join(reg
), len(val
), val
), file=f
)
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
);
900 mems
= sorted(smt
.hiermems(vlogtb_topmod
))
902 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(vlogtb_topmod
, mempath
)
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
))
911 addr_list
= smt
.get_list(addr_expr_list
)
912 data_list
= smt
.get_list(data_expr_list
)
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
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
)
925 anyseqs
= sorted(smt
.hieranyseqs(vlogtb_topmod
))
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
)))
931 print(" // state %d" % i
, file=f
)
934 print(" if (cycle == %d) begin" % (i
-1), file=f
)
936 for name
, val
in zip(pi_names
, pi_values
):
938 print(" PI_%s <= %d'b%s;" % (".".join(name
), len(val
), val
), file=f
)
940 print(" PI_%s = %d'b%s;" % (".".join(name
), len(val
), val
), file=f
)
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
)))
947 print(" UUT.%s <= %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
949 print(" UUT.%s = %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
952 print(" end", file=f
)
956 print(" end", file=f
)
957 print(" always @(posedge clock) begin", file=f
)
959 print(" genclock <= cycle < %d;" % (steps_stop
-1), file=f
)
960 print(" cycle <= cycle + 1;", file=f
)
961 print(" end", file=f
)
963 print("endmodule", file=f
)
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
))
970 constr_topmod
= topmod
971 constr_state
= "s@@step_idx@@"
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
]
980 constr_prefix
= smtctop
[1] + "."
983 steps_start
= steps_stop
- 1
985 with
open(filename
, "w") as f
:
986 primary_inputs
= list()
988 for name
in smt
.modinfo
[constr_topmod
].inputs
:
989 width
= smt
.modinfo
[constr_topmod
].wsize
[name
]
990 primary_inputs
.append((name
, width
))
992 if steps_start
== 0 or smtcinit
:
993 print("initial", file=f
)
995 print("state %d" % steps_start
, file=f
)
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
)))
1000 for name
, val
in zip(regnames
, regvals
):
1001 print("assume (= [%s%s] %s)" % (constr_prefix
, ".".join(name
), val
), file=f
)
1003 mems
= sorted(smt
.hiermems(constr_topmod
))
1004 for mempath
in mems
:
1005 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(constr_topmod
, mempath
)
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
))
1014 addr_list
= smt
.get_list(addr_expr_list
)
1015 data_list
= smt
.get_list(data_expr_list
)
1018 for addr
, data
in zip(addr_list
, data_list
):
1019 if addr
not in addr_data
:
1020 addr_data
[addr
] = data
1022 for addr
, data
in addr_data
.items():
1023 print("assume (= (select [%s%s] %s) %s)" % (constr_prefix
, ".".join(mempath
), addr
, data
), file=f
)
1025 for k
in range(steps_start
, steps_stop
):
1028 print("state %d" % k
, file=f
)
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
)))
1033 for name
, val
in zip(pi_names
, pi_values
):
1034 print("assume (= [%s%s] %s)" % (constr_prefix
, ".".join(name
), val
), file=f
)
1037 def write_trace(steps_start
, steps_stop
, index
):
1038 if vcdfile
is not None:
1039 write_vcd_trace(steps_start
, steps_stop
, index
)
1041 if vlogtbfile
is not None:
1042 write_vlogtb_trace(steps_start
, steps_stop
, index
)
1044 if outconstr
is not None:
1045 write_constr_trace(steps_start
, steps_stop
, index
)
1048 def print_failed_asserts_worker(mod
, state
, path
, extrainfo
):
1049 assert mod
in smt
.modinfo
1050 found_failed_assert
= False
1052 if smt
.get("(|%s_a| %s)" % (mod
, state
)) in ["true", "#b1"]:
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
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
1064 return found_failed_assert
1067 def print_failed_asserts(state
, final
=False, extrainfo
=""):
1069 loc_list
, expr_list
, value_list
= get_constr_expr(constr_asserts
, state
, final
=final
, getvalues
=True)
1070 found_failed_assert
= False
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
1078 if print_failed_asserts_worker(topmod
, "s%d" % state
, topmod
, extrainfo
):
1079 found_failed_assert
= True
1081 return found_failed_assert
1084 def print_anyconsts_worker(mod
, state
, path
):
1085 assert mod
in smt
.modinfo
1087 for cellname
, celltype
in smt
.modinfo
[mod
].cells
.items():
1088 print_anyconsts_worker(celltype
, "(|%s_h %s| %s)" % (mod
, cellname
, state
), path
+ "." + cellname
)
1090 for fun
, info
in smt
.modinfo
[mod
].anyconsts
.items():
1092 print_msg("Value for anyconst in %s (%s): %d" % (path
, info
[0], smt
.bv2int(smt
.get("(|%s| %s)" % (fun
, state
)))))
1094 print_msg("Value for anyconst %s.%s (%s): %d" % (path
, info
[1], info
[0], smt
.bv2int(smt
.get("(|%s| %s)" % (fun
, state
)))))
1097 def print_anyconsts(state
):
1099 print_anyconsts_worker(topmod
, "s%d" % state
, topmod
)
1102 def get_cover_list(mod
, base
):
1103 assert mod
in smt
.modinfo
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
)
1112 for cell
, submod
in smt
.modinfo
[mod
].cells
.items():
1113 e
, d
= get_cover_list(submod
, "(|%s_h %s| %s)" % (mod
, cell
, base
))
1117 return cover_expr
, cover_desc
1120 asserts_antecedent_cache
= [list()]
1121 asserts_consequent_cache
= [list()]
1122 asserts_cache_dirty
= False
1124 def smt_state(step
):
1125 smt
.write("(declare-fun s%d () |%s_s|)" % (step
, topmod
))
1126 states
.append("s%d" % step
)
1128 def smt_assert(expr
):
1132 smt
.write("(assert %s)" % expr
)
1134 def smt_assert_antecedent(expr
):
1138 smt
.write("(assert %s)" % expr
)
1140 global asserts_cache_dirty
1141 asserts_cache_dirty
= True
1142 asserts_antecedent_cache
[-1].append(expr
)
1144 def smt_assert_consequent(expr
):
1148 smt
.write("(assert %s)" % expr
)
1150 global asserts_cache_dirty
1151 asserts_cache_dirty
= True
1152 asserts_consequent_cache
[-1].append(expr
)
1154 def smt_forall_assert():
1158 global asserts_cache_dirty
1159 asserts_cache_dirty
= False
1161 def make_assert_expr(asserts_cache
):
1163 for lst
in asserts_cache
:
1166 assert len(expr
) != 0
1171 expr
= "(and %s)" % (" ".join(expr
))
1174 antecedent_expr
= make_assert_expr(asserts_antecedent_cache
)
1175 consequent_expr
= make_assert_expr(asserts_consequent_cache
)
1177 states_db
= set(states
)
1178 used_states_db
= set()
1179 new_antecedent_expr
= list()
1180 new_consequent_expr
= list()
1181 assert_expr
= list()
1183 def make_new_expr(new_expr
, expr
):
1185 while cursor
< len(expr
):
1187 if expr
[cursor
] in '|"':
1188 while cursor
+l
+1 < len(expr
) and expr
[cursor
] != expr
[cursor
+l
]:
1191 elif expr
[cursor
] not in '() ':
1192 while cursor
+l
< len(expr
) and expr
[cursor
+l
] not in '|"() ':
1195 word
= expr
[cursor
:cursor
+l
]
1196 if word
in states_db
:
1197 used_states_db
.add(word
)
1200 new_expr
.append(word
)
1203 make_new_expr(new_antecedent_expr
, antecedent_expr
)
1204 make_new_expr(new_consequent_expr
, consequent_expr
)
1206 new_antecedent_expr
= ["".join(new_antecedent_expr
)]
1207 new_consequent_expr
= ["".join(new_consequent_expr
)]
1209 if states
[0] in used_states_db
:
1210 new_antecedent_expr
.append("(|%s_ex_state_eq| %s %s_)" % (topmod
, states
[0], states
[0]))
1212 if s
in used_states_db
:
1213 new_antecedent_expr
.append("(|%s_ex_input_eq| %s %s_)" % (topmod
, s
, s
))
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]
1220 new_antecedent_expr
= "(and %s)" % (" ".join(new_antecedent_expr
))
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]
1227 new_consequent_expr
= "(and %s)" % (" ".join(new_consequent_expr
))
1229 assert_expr
.append("(assert (forall (")
1232 if s
in used_states_db
:
1233 assert_expr
.append("%s(%s_ |%s_s|)" % ("" if first_state
else " ", s
, topmod
))
1235 assert_expr
.append(") (=> %s %s)))" % (new_antecedent_expr
, new_consequent_expr
))
1237 smt
.write("".join(assert_expr
))
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)")
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)")
1253 def smt_check_sat():
1254 if asserts_cache_dirty
:
1256 return smt
.check_sat()
1260 skip_counter
= step_size
1261 for step
in range(num_steps
, -1, -1):
1263 print_msg("Temporal induction not supported for exists-forall problems.")
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
))
1272 if step
== num_steps
:
1273 smt_assert("(not (and (|%s_a| s%d) %s))" % (topmod
, step
, get_constr_expr(constr_asserts
, step
)))
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
))
1280 if step
> num_steps
-skip_steps
:
1281 print_msg("Skipping induction in step %d.." % (step
))
1285 if skip_counter
< step_size
:
1286 print_msg("Skipping induction in step %d.." % (step
))
1290 print_msg("Trying induction in step %d.." % (step
))
1292 if smt_check_sat() == "sat":
1294 print_msg("Temporal induction failed!")
1295 print_anyconsts(num_steps
)
1296 print_failed_asserts(num_steps
)
1297 write_trace(step
, num_steps
+1, '%')
1300 print_anyconsts(num_steps
)
1301 print_failed_asserts(num_steps
)
1302 write_trace(step
, num_steps
+1, "%d" % step
)
1305 print_msg("Temporal induction successful.")
1310 cover_expr
, cover_desc
= get_cover_list(topmod
, "state")
1311 cover_mask
= "1" * len(cover_desc
)
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]
1321 smt
.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod
, len(cover_desc
), cover_expr
))
1325 found_failed_assert
= False
1327 assert step_size
== 1
1329 while step
< num_steps
:
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
))
1337 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1339 smt_assert_antecedent("(|%s_i| s0)" % (topmod
))
1340 smt_assert_antecedent("(|%s_is| s0)" % (topmod
))
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
))
1346 while "1" in cover_mask
:
1347 print_msg("Checking cover reachability in step %d.." % (step
))
1349 smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx
, step
, "0" * len(cover_desc
)))
1351 if smt_check_sat() == "unsat":
1355 if append_steps
> 0:
1356 for i
in range(step
+1, step
+1+append_steps
):
1357 print_msg("Appending additional step %d." % 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
1371 reached_covers
= smt
.bv2bin(smt
.get("(covers_%d s%d)" % (coveridx
, step
)))
1372 assert len(reached_covers
) == len(cover_desc
)
1376 for i
in range(len(reached_covers
)):
1377 if reached_covers
[i
] == "0":
1378 new_cover_mask
.append(cover_mask
[i
])
1381 print_msg("Reached cover statement at %s in step %d." % (cover_desc
[i
], step
))
1382 new_cover_mask
.append("0")
1384 cover_mask
= "".join(new_cover_mask
)
1386 for i
in range(step
+1+append_steps
):
1387 if print_failed_asserts(i
, extrainfo
=" (step %d)" % i
):
1388 found_failed_assert
= True
1390 write_trace(0, step
+1+append_steps
, "%d" % coveridx
)
1392 if found_failed_assert
:
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
))
1399 if found_failed_assert
:
1402 if "1" not in cover_mask
:
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
])
1413 else: # not tempind, covermode
1416 while step
< num_steps
:
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
))
1424 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1426 smt_assert_antecedent("(|%s_i| s0)" % (topmod
))
1427 smt_assert_antecedent("(|%s_is| s0)" % (topmod
))
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
))
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
))
1439 print_msg("Skipping step %d.." % (step
))
1443 last_check_step
= step
1444 for i
in range(1, step_size
):
1445 if step
+i
< num_steps
:
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
1456 if last_check_step
== step
:
1457 print_msg("Checking assumptions in step %d.." % (step
))
1459 print_msg("Checking assumptions in steps %d to %d.." % (step
, last_check_step
))
1461 if smt_check_sat() == "unsat":
1462 print("%s Warmup failed!" % smt
.timestamp())
1467 if last_check_step
== step
:
1468 print_msg("Checking assertions in step %d.." % (step
))
1470 print_msg("Checking assertions in steps %d to %d.." % (step
, last_check_step
))
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)]))
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
)
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())
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
, '%')
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
))
1506 if constr_final_start
is not None:
1507 for i
in range(step
, last_check_step
+1):
1508 if i
< constr_final_start
:
1511 print_msg("Checking final constraints in step %d.." % (i
))
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))
1517 if smt_check_sat() == "sat":
1518 print("%s BMC failed!" % smt
.timestamp())
1520 print_failed_asserts(i
, final
=True)
1521 write_trace(0, i
+1, '%')
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
))
1534 print_msg("Solving for step %d.." % (last_check_step
))
1535 if smt_check_sat() != "sat":
1536 print("%s No solution found!" % smt
.timestamp())
1542 write_trace(0, last_check_step
+1, "%d" % step
)
1546 if gentrace
and retstatus
:
1548 write_trace(0, num_steps
, '%')
1554 print_msg("Status: %s" % ("PASSED" if retstatus
else "FAILED (!)"))
1555 sys
.exit(0 if retstatus
else 1)