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 assert (len(smt
.modinfo
[topmod
].maximize
) + len(smt
.modinfo
[topmod
].minimize
) <= 1)
1163 def make_assert_expr(asserts_cache
):
1165 for lst
in asserts_cache
:
1168 assert len(expr
) != 0
1173 expr
= "(and %s)" % (" ".join(expr
))
1176 antecedent_expr
= make_assert_expr(asserts_antecedent_cache
)
1177 consequent_expr
= make_assert_expr(asserts_consequent_cache
)
1179 states_db
= set(states
)
1180 used_states_db
= set()
1181 new_antecedent_expr
= list()
1182 new_consequent_expr
= list()
1183 assert_expr
= list()
1185 def make_new_expr(new_expr
, expr
):
1187 while cursor
< len(expr
):
1189 if expr
[cursor
] in '|"':
1190 while cursor
+l
+1 < len(expr
) and expr
[cursor
] != expr
[cursor
+l
]:
1193 elif expr
[cursor
] not in '() ':
1194 while cursor
+l
< len(expr
) and expr
[cursor
+l
] not in '|"() ':
1197 word
= expr
[cursor
:cursor
+l
]
1198 if word
in states_db
:
1199 used_states_db
.add(word
)
1202 new_expr
.append(word
)
1205 make_new_expr(new_antecedent_expr
, antecedent_expr
)
1206 make_new_expr(new_consequent_expr
, consequent_expr
)
1208 new_antecedent_expr
= ["".join(new_antecedent_expr
)]
1209 new_consequent_expr
= ["".join(new_consequent_expr
)]
1211 if states
[0] in used_states_db
:
1212 new_antecedent_expr
.append("(|%s_ex_state_eq| %s %s_)" % (topmod
, states
[0], states
[0]))
1214 if s
in used_states_db
:
1215 new_antecedent_expr
.append("(|%s_ex_input_eq| %s %s_)" % (topmod
, s
, s
))
1217 if len(new_antecedent_expr
) == 0:
1218 new_antecedent_expr
= "true"
1219 elif len(new_antecedent_expr
) == 1:
1220 new_antecedent_expr
= new_antecedent_expr
[0]
1222 new_antecedent_expr
= "(and %s)" % (" ".join(new_antecedent_expr
))
1224 if len(new_consequent_expr
) == 0:
1225 new_consequent_expr
= "true"
1226 elif len(new_consequent_expr
) == 1:
1227 new_consequent_expr
= new_consequent_expr
[0]
1229 new_consequent_expr
= "(and %s)" % (" ".join(new_consequent_expr
))
1231 assert_expr
.append("(assert (forall (")
1234 if s
in used_states_db
:
1235 assert_expr
.append("%s(%s_ |%s_s|)" % ("" if first_state
else " ", s
, topmod
))
1237 assert_expr
.append(") (=> %s %s)))" % (new_antecedent_expr
, new_consequent_expr
))
1239 smt
.write("".join(assert_expr
))
1241 if len(smt
.modinfo
[topmod
].maximize
) > 0:
1243 if s
in used_states_db
:
1244 smt
.write("(maximize (|%s| %s))\n" % (smt
.modinfo
[topmod
].maximize
.copy().pop(), s
))
1247 if len(smt
.modinfo
[topmod
].minimize
) > 0:
1249 if s
in used_states_db
:
1250 smt
.write("(minimize (|%s| %s))\n" % (smt
.modinfo
[topmod
].minimize
.copy().pop(), s
))
1254 global asserts_cache_dirty
1255 asserts_cache_dirty
= True
1256 asserts_antecedent_cache
.append(list())
1257 asserts_consequent_cache
.append(list())
1258 smt
.write("(push 1)")
1261 global asserts_cache_dirty
1262 asserts_cache_dirty
= True
1263 asserts_antecedent_cache
.pop()
1264 asserts_consequent_cache
.pop()
1265 smt
.write("(pop 1)")
1267 def smt_check_sat():
1268 if asserts_cache_dirty
:
1270 return smt
.check_sat()
1273 retstatus
= "FAILED"
1274 skip_counter
= step_size
1275 for step
in range(num_steps
, -1, -1):
1277 print_msg("Temporal induction not supported for exists-forall problems.")
1281 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1282 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1283 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1284 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1286 if step
== num_steps
:
1287 smt_assert("(not (and (|%s_a| s%d) %s))" % (topmod
, step
, get_constr_expr(constr_asserts
, step
)))
1290 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
, step
+1))
1291 smt_assert("(|%s_a| s%d)" % (topmod
, step
))
1292 smt_assert(get_constr_expr(constr_asserts
, step
))
1294 if step
> num_steps
-skip_steps
:
1295 print_msg("Skipping induction in step %d.." % (step
))
1299 if skip_counter
< step_size
:
1300 print_msg("Skipping induction in step %d.." % (step
))
1304 print_msg("Trying induction in step %d.." % (step
))
1306 if smt_check_sat() == "sat":
1308 print_msg("Temporal induction failed!")
1309 print_anyconsts(num_steps
)
1310 print_failed_asserts(num_steps
)
1311 write_trace(step
, num_steps
+1, '%')
1314 print_anyconsts(num_steps
)
1315 print_failed_asserts(num_steps
)
1316 write_trace(step
, num_steps
+1, "%d" % step
)
1319 print_msg("Temporal induction successful.")
1320 retstatus
= "PASSED"
1324 cover_expr
, cover_desc
= get_cover_list(topmod
, "state")
1325 cover_mask
= "1" * len(cover_desc
)
1327 if len(cover_expr
) > 1:
1328 cover_expr
= "(concat %s)" % " ".join(cover_expr
)
1329 elif len(cover_expr
) == 1:
1330 cover_expr
= cover_expr
[0]
1335 smt
.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod
, len(cover_desc
), cover_expr
))
1338 retstatus
= "FAILED"
1339 found_failed_assert
= False
1341 assert step_size
== 1
1343 while step
< num_steps
:
1345 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1346 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1347 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1351 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1353 smt_assert_antecedent("(|%s_i| s0)" % (topmod
))
1354 smt_assert_antecedent("(|%s_is| s0)" % (topmod
))
1357 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
-1, step
))
1358 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1360 while "1" in cover_mask
:
1361 print_msg("Checking cover reachability in step %d.." % (step
))
1363 smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx
, step
, "0" * len(cover_desc
)))
1365 if smt_check_sat() == "unsat":
1369 if append_steps
> 0:
1370 for i
in range(step
+1, step
+1+append_steps
):
1371 print_msg("Appending additional step %d." % i
)
1373 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, i
))
1374 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, i
))
1375 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, i
))
1376 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, i
-1, i
))
1377 smt_assert_consequent(get_constr_expr(constr_assumes
, i
))
1378 print_msg("Re-solving with appended steps..")
1379 if smt_check_sat() == "unsat":
1380 print("%s Cannot appended steps without violating assumptions!" % smt
.timestamp())
1381 found_failed_assert
= True
1382 retstatus
= "FAILED"
1385 reached_covers
= smt
.bv2bin(smt
.get("(covers_%d s%d)" % (coveridx
, step
)))
1386 assert len(reached_covers
) == len(cover_desc
)
1390 for i
in range(len(reached_covers
)):
1391 if reached_covers
[i
] == "0":
1392 new_cover_mask
.append(cover_mask
[i
])
1395 print_msg("Reached cover statement at %s in step %d." % (cover_desc
[i
], step
))
1396 new_cover_mask
.append("0")
1398 cover_mask
= "".join(new_cover_mask
)
1400 for i
in range(step
+1+append_steps
):
1401 if print_failed_asserts(i
, extrainfo
=" (step %d)" % i
):
1402 found_failed_assert
= True
1404 write_trace(0, step
+1+append_steps
, "%d" % coveridx
)
1406 if found_failed_assert
:
1411 smt
.write("(define-fun covers_%d ((state |%s_s|)) (_ BitVec %d) (bvand (covers_%d state) #b%s))" % (coveridx
, topmod
, len(cover_desc
), coveridx
-1, cover_mask
))
1413 if found_failed_assert
:
1416 if "1" not in cover_mask
:
1417 retstatus
= "PASSED"
1422 if "1" in cover_mask
:
1423 for i
in range(len(cover_mask
)):
1424 if cover_mask
[i
] == "1":
1425 print_msg("Unreached cover statement at %s." % cover_desc
[i
])
1427 else: # not tempind, covermode
1429 retstatus
= "PASSED"
1430 while step
< num_steps
:
1432 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1433 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1434 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1438 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1440 smt_assert_antecedent("(|%s_i| s0)" % (topmod
))
1441 smt_assert_antecedent("(|%s_is| s0)" % (topmod
))
1444 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
-1, step
))
1445 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1447 if step
< skip_steps
:
1448 if assume_skipped
is not None and step
>= assume_skipped
:
1449 print_msg("Skipping step %d (and assuming pass).." % (step
))
1450 smt_assert("(|%s_a| s%d)" % (topmod
, step
))
1451 smt_assert(get_constr_expr(constr_asserts
, step
))
1453 print_msg("Skipping step %d.." % (step
))
1457 last_check_step
= step
1458 for i
in range(1, step_size
):
1459 if step
+i
< num_steps
:
1461 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
+i
))
1462 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
+i
))
1463 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
+i
))
1464 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
+i
-1, step
+i
))
1465 smt_assert_consequent(get_constr_expr(constr_assumes
, step
+i
))
1466 last_check_step
= step
+i
1470 if last_check_step
== step
:
1471 print_msg("Checking assumptions in step %d.." % (step
))
1473 print_msg("Checking assumptions in steps %d to %d.." % (step
, last_check_step
))
1475 if smt_check_sat() == "unsat":
1476 print("%s Assumptions are unsatisfiable!" % smt
.timestamp())
1477 retstatus
= "PREUNSAT"
1481 if last_check_step
== step
:
1482 print_msg("Checking assertions in step %d.." % (step
))
1484 print_msg("Checking assertions in steps %d to %d.." % (step
, last_check_step
))
1487 smt_assert("(not (and %s))" % " ".join(["(|%s_a| s%d)" % (topmod
, i
) for i
in range(step
, last_check_step
+1)] +
1488 [get_constr_expr(constr_asserts
, i
) for i
in range(step
, last_check_step
+1)]))
1490 if smt_check_sat() == "sat":
1491 print("%s BMC failed!" % smt
.timestamp())
1492 if append_steps
> 0:
1493 for i
in range(last_check_step
+1, last_check_step
+1+append_steps
):
1494 print_msg("Appending additional step %d." % i
)
1496 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, i
))
1497 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, i
))
1498 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, i
))
1499 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, i
-1, i
))
1500 smt_assert_consequent(get_constr_expr(constr_assumes
, i
))
1501 print_msg("Re-solving with appended steps..")
1502 if smt_check_sat() == "unsat":
1503 print("%s Cannot appended steps without violating assumptions!" % smt
.timestamp())
1504 retstatus
= "FAILED"
1506 print_anyconsts(step
)
1507 for i
in range(step
, last_check_step
+1):
1508 print_failed_asserts(i
)
1509 write_trace(0, last_check_step
+1+append_steps
, '%')
1510 retstatus
= "FAILED"
1515 if (constr_final_start
is not None) or (last_check_step
+1 != num_steps
):
1516 for i
in range(step
, last_check_step
+1):
1517 smt_assert("(|%s_a| s%d)" % (topmod
, i
))
1518 smt_assert(get_constr_expr(constr_asserts
, i
))
1520 if constr_final_start
is not None:
1521 for i
in range(step
, last_check_step
+1):
1522 if i
< constr_final_start
:
1525 print_msg("Checking final constraints in step %d.." % (i
))
1528 smt_assert_consequent(get_constr_expr(constr_assumes
, i
, final
=True))
1529 smt_assert("(not %s)" % get_constr_expr(constr_asserts
, i
, final
=True))
1531 if smt_check_sat() == "sat":
1532 print("%s BMC failed!" % smt
.timestamp())
1534 print_failed_asserts(i
, final
=True)
1535 write_trace(0, i
+1, '%')
1536 retstatus
= "FAILED"
1544 for i
in range(step
, last_check_step
+1):
1545 smt_assert("(|%s_a| s%d)" % (topmod
, i
))
1546 smt_assert(get_constr_expr(constr_asserts
, i
))
1548 print_msg("Solving for step %d.." % (last_check_step
))
1549 if smt_check_sat() != "sat":
1550 print("%s No solution found!" % smt
.timestamp())
1551 retstatus
= "FAILED"
1556 write_trace(0, last_check_step
+1, "%d" % step
)
1560 if gentrace
and retstatus
:
1562 write_trace(0, num_steps
, '%')
1568 print_msg("Status: %s" % retstatus
)
1569 sys
.exit(0 if retstatus
== "PASSED" else 1)