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 print(os
.path
.basename(sys
.argv
[0]) + """ [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)
155 dump anyconst values as raw bit strings
161 opts
, args
= getopt
.getopt(sys
.argv
[1:], so
.shortopts
+ "t:igcm:", so
.longopts
+
162 ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
163 "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
164 "smtc-init", "smtc-top=", "noinit", "binary"])
173 num_steps
= int(a
[0])
175 skip_steps
= int(a
[0])
176 num_steps
= int(a
[1])
178 skip_steps
= int(a
[0])
179 step_size
= int(a
[1])
180 num_steps
= int(a
[2])
183 elif o
== "--assume-skipped":
184 assume_skipped
= int(a
)
185 elif o
== "--final-only":
193 aimfile
, aiwfile
= a
.split(":")
197 elif o
== "--aig-noheader":
199 elif o
== "--btorwit":
201 elif o
== "--dump-vcd":
203 elif o
== "--dump-vlogtb":
205 elif o
== "--vlogtb-top":
207 elif o
== "--dump-smtc":
209 elif o
== "--smtc-init":
211 elif o
== "--smtc-top":
212 smtctop
= a
.split(":")
213 if len(smtctop
) == 1:
215 assert len(smtctop
) == 2
216 smtctop
= tuple(smtctop
)
217 elif o
== "--dump-all":
219 elif o
== "--presat":
221 elif o
== "--noinfo":
223 elif o
== "--noinit":
225 elif o
== "--append":
226 append_steps
= int(a
)
235 elif o
== "--binary":
237 elif so
.handle(o
, a
):
245 if sum([tempind
, gentrace
, covermode
]) > 1:
248 constr_final_start
= None
249 constr_asserts
= defaultdict(list)
250 constr_assumes
= defaultdict(list)
251 constr_write
= list()
254 current_states
= None
257 with
open(fn
, "r") as f
:
261 if line
.startswith("#"):
264 tokens
= line
.split()
269 if tokens
[0] == "initial":
270 current_states
= set()
272 current_states
.add(0)
275 if tokens
[0] == "final":
278 current_states
= set(["final-%d" % i
for i
in range(0, num_steps
+1)])
279 constr_final_start
= 0
280 elif len(tokens
) == 2:
281 arg
= abs(int(tokens
[1]))
282 current_states
= set(["final-%d" % i
for i
in range(arg
, num_steps
+1)])
283 constr_final_start
= arg
if constr_final_start
is None else min(constr_final_start
, arg
)
288 if tokens
[0] == "state":
289 current_states
= set()
291 for token
in tokens
[1:]:
292 tok
= token
.split(":")
294 current_states
.add(int(token
))
301 for i
in range(lower
, upper
+1):
302 current_states
.add(i
)
307 if tokens
[0] == "always":
309 current_states
= set(range(0, num_steps
+1))
310 elif len(tokens
) == 2:
311 arg
= abs(int(tokens
[1]))
312 current_states
= set(range(arg
, num_steps
+1))
317 if tokens
[0] == "assert":
318 assert current_states
is not None
320 for state
in current_states
:
321 constr_asserts
[state
].append(("%s:%d" % (fn
, current_line
), " ".join(tokens
[1:])))
325 if tokens
[0] == "assume":
326 assert current_states
is not None
328 for state
in current_states
:
329 constr_assumes
[state
].append(("%s:%d" % (fn
, current_line
), " ".join(tokens
[1:])))
333 if tokens
[0] == "write":
334 constr_write
.append(" ".join(tokens
[1:]))
337 if tokens
[0] == "logic":
338 so
.logic
= " ".join(tokens
[1:])
344 def get_constr_expr(db
, state
, final
=False, getvalues
=False):
346 if ("final-%d" % state
) not in db
:
347 return ([], [], []) if getvalues
else "true"
350 return ([], [], []) if getvalues
else "true"
352 netref_regex
= re
.compile(r
'(^|[( ])\[(-?[0-9]+:|)([^\]]*|\S*)\](?=[ )]|$)')
354 def replace_netref(match
):
355 state_sel
= match
.group(2)
359 elif state_sel
[0] == "-":
360 st
= state
+ int(state_sel
[:-1])
362 st
= int(state_sel
[:-1])
364 expr
= smt
.net_expr(topmod
, "s%d" % st
, smt
.get_path(topmod
, match
.group(3)))
366 return match
.group(1) + expr
369 for loc
, expr
in db
[("final-%d" % state
) if final
else state
]:
370 actual_expr
= netref_regex
.sub(replace_netref
, expr
)
372 expr_list
.append((loc
, expr
, actual_expr
))
374 expr_list
.append(actual_expr
)
377 loc_list
, expr_list
, acual_expr_list
= zip(*expr_list
)
378 value_list
= smt
.get_list(acual_expr_list
)
379 return loc_list
, expr_list
, value_list
381 if len(expr_list
) == 0:
384 if len(expr_list
) == 1:
387 return "(and %s)" % " ".join(expr_list
)
392 if noinfo
and vcdfile
is None and vlogtbfile
is None and outconstr
is None:
393 smt
.produce_models
= False
396 print("%s %s" % (smt
.timestamp(), msg
))
399 print_msg("Solver: %s" % (so
.solver
))
401 with
open(args
[0], "r") as f
:
405 for line
in constr_write
:
411 assert topmod
is not None
412 assert topmod
in smt
.modinfo
414 if cexfile
is not None:
420 with
open(cexfile
, "r") as f
:
421 cex_regex
= re
.compile(r
'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
422 for entry
in f
.read().split():
423 match
= cex_regex
.match(entry
)
426 name
, bit
, extra_name
, step
, val
= match
.group(1), match
.group(2), match
.group(3), match
.group(4), match
.group(5)
431 if name
not in smt
.modinfo
[topmod
].inputs
:
442 if smt
.modinfo
[topmod
].wsize
[name
] == 1:
444 smtexpr
= "(= [%s] %s)" % (name
, "true" if val
else "false")
446 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bit
, bit
, name
, val
)
448 # print("cex@%d: %s" % (step, smtexpr))
449 constr_assumes
[step
].append((cexfile
, smtexpr
))
452 skip_steps
= max(skip_steps
, step
)
453 num_steps
= max(num_steps
, step
+1)
455 if aimfile
is not None:
465 with
open(aimfile
, "r") as f
:
466 for entry
in f
.read().splitlines():
467 entry
= entry
.split()
469 if entry
[0] == "input":
470 input_map
[int(entry
[1])] = (entry
[3], int(entry
[2]))
473 if entry
[0] == "init":
474 init_map
[int(entry
[1])] = (entry
[3], int(entry
[2]))
477 if entry
[0] in ["latch", "invlatch"]:
478 latch_map
[int(entry
[1])] = (entry
[3], int(entry
[2]), entry
[0] == "invlatch")
481 if entry
[0] in ["output", "wire"]:
486 with
open(aiwfile
, "r") as f
:
494 for entry
in f
.read().splitlines():
495 if len(entry
) == 0 or entry
[0] in "bcjfu.":
505 if len(init_map
) == 0:
506 for i
in range(len(entry
)):
511 value
= int(entry
[i
])
512 name
= latch_map
[i
][0]
513 bitidx
= latch_map
[i
][1]
514 invert
= latch_map
[i
][2]
519 path
= smt
.get_path(topmod
, name
)
520 width
= smt
.net_width(topmod
, path
)
524 smtexpr
= "(= [%s] %s)" % (name
, "true" if value
else "false")
526 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx
, bitidx
, name
, value
)
528 constr_assumes
[0].append((cexfile
, smtexpr
))
531 for i
in range(len(entry
)):
535 if (step
== 0) and (i
in init_map
):
536 value
= int(entry
[i
])
537 name
= init_map
[i
][0]
538 bitidx
= init_map
[i
][1]
540 path
= smt
.get_path(topmod
, name
)
542 if not smt
.net_exists(topmod
, path
):
543 match
= re
.match(r
"(.*)\[(\d+)\]$", path
[-1])
545 path
[-1] = match
.group(1)
546 addr
= int(match
.group(2))
548 if not match
or not smt
.mem_exists(topmod
, path
):
549 print_msg("Ignoring init value for unknown net: %s" % (name
))
552 meminfo
= smt
.mem_info(topmod
, path
)
553 smtexpr
= "(select [%s] #b%s)" % (".".join(path
), bin(addr
)[2:].zfill(meminfo
[0]))
557 smtexpr
= "[%s]" % name
558 width
= smt
.net_width(topmod
, path
)
562 smtexpr
= "(= %s %s)" % (smtexpr
, "true" if value
else "false")
564 smtexpr
= "(= ((_ extract %d %d) %s) #b%d)" % (bitidx
, bitidx
, smtexpr
, value
)
566 constr_assumes
[0].append((cexfile
, smtexpr
))
569 value
= int(entry
[i
])
570 name
= input_map
[i
][0]
571 bitidx
= input_map
[i
][1]
573 path
= smt
.get_path(topmod
, name
)
574 width
= smt
.net_width(topmod
, path
)
578 smtexpr
= "(= [%s] %s)" % (name
, "true" if value
else "false")
580 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx
, bitidx
, name
, value
)
582 constr_assumes
[step
].append((cexfile
, smtexpr
))
585 skip_steps
= max(skip_steps
, step
)
586 num_steps
= max(num_steps
, step
+1)
589 if btorwitfile
is not None:
590 with
open(btorwitfile
, "r") as f
:
606 if line
== "" or line
[0] == "b" or line
[0] == "j":
612 if line
[0] == '#' or line
[0] == '@':
617 altsuffix
= "#" + suffix
[1:]
619 altsuffix
= "@" + suffix
[1:]
627 if line
[-1].endswith(suffix
):
628 line
[-1] = line
[-1][0:len(line
[-1]) - len(suffix
)]
630 if line
[-1].endswith(altsuffix
):
631 line
[-1] = line
[-1][0:len(line
[-1]) - len(altsuffix
)]
633 if line
[-1][0] == "$":
637 if len(line
) == 3 and line
[1][0] != "[":
641 path
= smt
.get_path(topmod
, name
)
643 if not smt
.net_exists(topmod
, path
):
646 width
= smt
.net_width(topmod
, path
)
649 assert value
in ["0", "1"]
650 value
= "true" if value
== "1" else "false"
654 smtexpr
= "(= [%s] %s)" % (name
, value
)
655 constr_assumes
[step
].append((btorwitfile
, smtexpr
))
658 if len(line
) == 4 and line
[1][0] == "[":
663 path
= smt
.get_path(topmod
, name
)
665 if not smt
.mem_exists(topmod
, path
):
668 meminfo
= smt
.mem_info(topmod
, path
)
671 assert value
in ["0", "1"]
672 value
= "true" if value
== "1" else "false"
676 assert index
[0] == "["
677 assert index
[-1] == "]"
678 index
= "#b" + index
[1:-1]
680 smtexpr
= "(= (select [%s] %s) %s)" % (name
, index
, value
)
681 constr_assumes
[step
].append((btorwitfile
, smtexpr
))
686 def write_vcd_trace(steps_start
, steps_stop
, index
):
687 filename
= vcdfile
.replace("%", index
)
688 print_msg("Writing trace to VCD file: %s" % (filename
))
690 with
open(filename
, "w") as vcd_file
:
691 vcd
= MkVcd(vcd_file
)
694 for netpath
in sorted(smt
.hiernets(topmod
)):
697 if n
.startswith("$"):
700 edge
= smt
.net_clock(topmod
, netpath
)
702 vcd
.add_net([topmod
] + netpath
, smt
.net_width(topmod
, netpath
))
704 vcd
.add_clock([topmod
] + netpath
, edge
)
705 path_list
.append(netpath
)
707 mem_trace_data
= dict()
708 for mempath
in sorted(smt
.hiermems(topmod
)):
709 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(topmod
, mempath
)
713 for i
in range(steps_start
, steps_stop
):
714 for j
in range(rports
):
715 expr_id
.append(('R', i
-steps_start
, j
, 'A'))
716 expr_id
.append(('R', i
-steps_start
, j
, 'D'))
717 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "R%dA" % j
))
718 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "R%dD" % j
))
719 for j
in range(wports
):
720 expr_id
.append(('W', i
-steps_start
, j
, 'A'))
721 expr_id
.append(('W', i
-steps_start
, j
, 'D'))
722 expr_id
.append(('W', i
-steps_start
, j
, 'M'))
723 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dA" % j
))
724 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dD" % j
))
725 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dM" % j
))
731 for eid
, edat
in zip(expr_id
, smt
.get_list(expr_list
)):
749 c
[f
] = smt
.bv2bin(edat
)
759 if len(wdata
) == 0 and len(rdata
) != 0:
760 wdata
= [[]] * len(rdata
)
762 assert len(rdata
) == len(wdata
)
764 for i
in range(len(wdata
)):
766 for j_data
in rdata
[i
]:
767 if j_data
["A"] == addr
:
768 data
= list(j_data
["D"])
774 for i
in reversed(range(len(tdata
))):
775 for k
in range(width
):
776 if tdata
[i
][k
] == "x":
782 tdata
.append(data
[:])
784 for j_data
in wdata
[i
]:
785 if j_data
["A"] != addr
:
791 for k
in range(width
):
796 tdata
.append(data
[:])
798 assert len(tdata
) == len(rdata
)
801 netpath
[-1] += "<%0*x>" % ((len(addr
)+3) // 4, int(addr
, 2))
802 vcd
.add_net([topmod
] + netpath
, width
)
804 for i
in range(steps_start
, steps_stop
):
805 if i
not in mem_trace_data
:
806 mem_trace_data
[i
] = list()
807 mem_trace_data
[i
].append((netpath
, "".join(tdata
[i
-steps_start
])))
809 for i
in range(steps_start
, steps_stop
):
811 value_list
= smt
.get_net_bin_list(topmod
, path_list
, "s%d" % i
)
812 for path
, value
in zip(path_list
, value_list
):
813 vcd
.set_net([topmod
] + path
, value
)
814 if i
in mem_trace_data
:
815 for path
, value
in mem_trace_data
[i
]:
816 vcd
.set_net([topmod
] + path
, value
)
818 vcd
.set_time(steps_stop
)
821 def write_vlogtb_trace(steps_start
, steps_stop
, index
):
822 filename
= vlogtbfile
.replace("%", index
)
823 print_msg("Writing trace to Verilog testbench: %s" % (filename
))
825 vlogtb_topmod
= topmod
826 vlogtb_state
= "s@@step_idx@@"
828 if vlogtbtop
is not None:
829 for item
in vlogtbtop
.split("."):
830 if item
in smt
.modinfo
[vlogtb_topmod
].cells
:
831 vlogtb_state
= "(|%s_h %s| %s)" % (vlogtb_topmod
, item
, vlogtb_state
)
832 vlogtb_topmod
= smt
.modinfo
[vlogtb_topmod
].cells
[item
]
834 print_msg("Vlog top module '%s' not found: no cell '%s' in module '%s'" % (vlogtbtop
, item
, vlogtb_topmod
))
837 with
open(filename
, "w") as f
:
838 print("`ifndef VERILATOR", file=f
)
839 print("module testbench;", file=f
)
840 print(" reg [4095:0] vcdfile;", file=f
)
841 print(" reg clock;", file=f
)
842 print("`else", file=f
)
843 print("module testbench(input clock, output reg genclock);", file=f
)
844 print(" initial genclock = 1;", file=f
)
845 print("`endif", file=f
)
847 print(" reg genclock = 1;", file=f
)
848 print(" reg [31:0] cycle = 0;", file=f
)
850 primary_inputs
= list()
853 for name
in smt
.modinfo
[vlogtb_topmod
].inputs
:
854 if name
in ["clk", "clock", "CLK", "CLOCK"]:
855 clock_inputs
.add(name
)
856 width
= smt
.modinfo
[vlogtb_topmod
].wsize
[name
]
857 primary_inputs
.append((name
, width
))
859 for name
, width
in primary_inputs
:
860 if name
in clock_inputs
:
861 print(" wire [%d:0] PI_%s = clock;" % (width
-1, name
), file=f
)
863 print(" reg [%d:0] PI_%s;" % (width
-1, name
), file=f
)
865 print(" %s UUT (" % vlogtb_topmod
, file=f
)
866 print(",\n".join(" .{name}(PI_{name})".format(name
=name
) for name
, _
in primary_inputs
), file=f
)
869 print("`ifndef VERILATOR", file=f
)
870 print(" initial begin", file=f
)
871 print(" if ($value$plusargs(\"vcd=%s\", vcdfile)) begin", file=f
)
872 print(" $dumpfile(vcdfile);", file=f
)
873 print(" $dumpvars(0, testbench);", file=f
)
874 print(" end", file=f
)
875 print(" #5 clock = 0;", file=f
)
876 print(" while (genclock) begin", file=f
)
877 print(" #5 clock = 0;", file=f
)
878 print(" #5 clock = 1;", file=f
)
879 print(" end", file=f
)
880 print(" end", file=f
)
881 print("`endif", file=f
)
883 print(" initial begin", file=f
)
885 regs
= sorted(smt
.hiernets(vlogtb_topmod
, regs_only
=True))
886 regvals
= smt
.get_net_bin_list(vlogtb_topmod
, regs
, vlogtb_state
.replace("@@step_idx@@", str(steps_start
)))
888 print("`ifndef VERILATOR", file=f
)
889 print(" #1;", file=f
)
890 print("`endif", file=f
)
891 for reg
, val
in zip(regs
, regvals
):
894 if n
.startswith("$"):
896 print(" %sUUT.%s = %d'b%s;" % ("// " if hidden_net
else "", ".".join(reg
), len(val
), val
), file=f
)
898 anyconsts
= sorted(smt
.hieranyconsts(vlogtb_topmod
))
899 for info
in anyconsts
:
900 if info
[3] is not None:
901 modstate
= smt
.net_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(steps_start
)), info
[0])
902 value
= smt
.bv2bin(smt
.get("(|%s| %s)" % (info
[1], modstate
)))
903 print(" UUT.%s = %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
905 mems
= sorted(smt
.hiermems(vlogtb_topmod
))
907 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(vlogtb_topmod
, mempath
)
909 addr_expr_list
= list()
910 data_expr_list
= list()
911 for i
in range(steps_start
, steps_stop
):
912 for j
in range(rports
):
913 addr_expr_list
.append(smt
.mem_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dA" % j
))
914 data_expr_list
.append(smt
.mem_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dD" % j
))
916 addr_list
= smt
.get_list(addr_expr_list
)
917 data_list
= smt
.get_list(data_expr_list
)
920 for addr
, data
in zip(addr_list
, data_list
):
921 addr
= smt
.bv2bin(addr
)
922 data
= smt
.bv2bin(data
)
923 if addr
not in addr_data
:
924 addr_data
[addr
] = data
926 for addr
, data
in addr_data
.items():
927 print(" UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath
), len(addr
), addr
, len(data
), data
), file=f
)
930 anyseqs
= sorted(smt
.hieranyseqs(vlogtb_topmod
))
932 for i
in range(steps_start
, steps_stop
):
933 pi_names
= [[name
] for name
, _
in primary_inputs
if name
not in clock_inputs
]
934 pi_values
= smt
.get_net_bin_list(vlogtb_topmod
, pi_names
, vlogtb_state
.replace("@@step_idx@@", str(i
)))
936 print(" // state %d" % i
, file=f
)
939 print(" if (cycle == %d) begin" % (i
-1), file=f
)
941 for name
, val
in zip(pi_names
, pi_values
):
943 print(" PI_%s <= %d'b%s;" % (".".join(name
), len(val
), val
), file=f
)
945 print(" PI_%s = %d'b%s;" % (".".join(name
), len(val
), val
), file=f
)
948 if info
[3] is not None:
949 modstate
= smt
.net_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), info
[0])
950 value
= smt
.bv2bin(smt
.get("(|%s| %s)" % (info
[1], modstate
)))
952 print(" UUT.%s <= %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
954 print(" UUT.%s = %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
957 print(" end", file=f
)
961 print(" end", file=f
)
962 print(" always @(posedge clock) begin", file=f
)
964 print(" genclock <= cycle < %d;" % (steps_stop
-1), file=f
)
965 print(" cycle <= cycle + 1;", file=f
)
966 print(" end", file=f
)
968 print("endmodule", file=f
)
971 def write_constr_trace(steps_start
, steps_stop
, index
):
972 filename
= outconstr
.replace("%", index
)
973 print_msg("Writing trace to constraints file: %s" % (filename
))
975 constr_topmod
= topmod
976 constr_state
= "s@@step_idx@@"
979 if smtctop
is not None:
980 for item
in smtctop
[0].split("."):
981 assert item
in smt
.modinfo
[constr_topmod
].cells
982 constr_state
= "(|%s_h %s| %s)" % (constr_topmod
, item
, constr_state
)
983 constr_topmod
= smt
.modinfo
[constr_topmod
].cells
[item
]
985 constr_prefix
= smtctop
[1] + "."
988 steps_start
= steps_stop
- 1
990 with
open(filename
, "w") as f
:
991 primary_inputs
= list()
993 for name
in smt
.modinfo
[constr_topmod
].inputs
:
994 width
= smt
.modinfo
[constr_topmod
].wsize
[name
]
995 primary_inputs
.append((name
, width
))
997 if steps_start
== 0 or smtcinit
:
998 print("initial", file=f
)
1000 print("state %d" % steps_start
, file=f
)
1002 regnames
= sorted(smt
.hiernets(constr_topmod
, regs_only
=True))
1003 regvals
= smt
.get_net_list(constr_topmod
, regnames
, constr_state
.replace("@@step_idx@@", str(steps_start
)))
1005 for name
, val
in zip(regnames
, regvals
):
1006 print("assume (= [%s%s] %s)" % (constr_prefix
, ".".join(name
), val
), file=f
)
1008 mems
= sorted(smt
.hiermems(constr_topmod
))
1009 for mempath
in mems
:
1010 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(constr_topmod
, mempath
)
1012 addr_expr_list
= list()
1013 data_expr_list
= list()
1014 for i
in range(steps_start
, steps_stop
):
1015 for j
in range(rports
):
1016 addr_expr_list
.append(smt
.mem_expr(constr_topmod
, constr_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dA" % j
))
1017 data_expr_list
.append(smt
.mem_expr(constr_topmod
, constr_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dD" % j
))
1019 addr_list
= smt
.get_list(addr_expr_list
)
1020 data_list
= smt
.get_list(data_expr_list
)
1023 for addr
, data
in zip(addr_list
, data_list
):
1024 if addr
not in addr_data
:
1025 addr_data
[addr
] = data
1027 for addr
, data
in addr_data
.items():
1028 print("assume (= (select [%s%s] %s) %s)" % (constr_prefix
, ".".join(mempath
), addr
, data
), file=f
)
1030 for k
in range(steps_start
, steps_stop
):
1033 print("state %d" % k
, file=f
)
1035 pi_names
= [[name
] for name
, _
in sorted(primary_inputs
)]
1036 pi_values
= smt
.get_net_list(constr_topmod
, pi_names
, constr_state
.replace("@@step_idx@@", str(k
)))
1038 for name
, val
in zip(pi_names
, pi_values
):
1039 print("assume (= [%s%s] %s)" % (constr_prefix
, ".".join(name
), val
), file=f
)
1042 def write_trace(steps_start
, steps_stop
, index
):
1043 if vcdfile
is not None:
1044 write_vcd_trace(steps_start
, steps_stop
, index
)
1046 if vlogtbfile
is not None:
1047 write_vlogtb_trace(steps_start
, steps_stop
, index
)
1049 if outconstr
is not None:
1050 write_constr_trace(steps_start
, steps_stop
, index
)
1053 def print_failed_asserts_worker(mod
, state
, path
, extrainfo
):
1054 assert mod
in smt
.modinfo
1055 found_failed_assert
= False
1057 if smt
.get("(|%s_a| %s)" % (mod
, state
)) in ["true", "#b1"]:
1060 for cellname
, celltype
in smt
.modinfo
[mod
].cells
.items():
1061 if print_failed_asserts_worker(celltype
, "(|%s_h %s| %s)" % (mod
, cellname
, state
), path
+ "." + cellname
, extrainfo
):
1062 found_failed_assert
= True
1064 for assertfun
, assertinfo
in smt
.modinfo
[mod
].asserts
.items():
1065 if smt
.get("(|%s| %s)" % (assertfun
, state
)) in ["false", "#b0"]:
1066 print_msg("Assert failed in %s: %s%s" % (path
, assertinfo
, extrainfo
))
1067 found_failed_assert
= True
1069 return found_failed_assert
1072 def print_failed_asserts(state
, final
=False, extrainfo
=""):
1074 loc_list
, expr_list
, value_list
= get_constr_expr(constr_asserts
, state
, final
=final
, getvalues
=True)
1075 found_failed_assert
= False
1077 for loc
, expr
, value
in zip(loc_list
, expr_list
, value_list
):
1078 if smt
.bv2int(value
) == 0:
1079 print_msg("Assert %s failed: %s%s" % (loc
, expr
, extrainfo
))
1080 found_failed_assert
= True
1083 if print_failed_asserts_worker(topmod
, "s%d" % state
, topmod
, extrainfo
):
1084 found_failed_assert
= True
1086 return found_failed_assert
1089 def print_anyconsts_worker(mod
, state
, path
):
1090 assert mod
in smt
.modinfo
1092 for cellname
, celltype
in smt
.modinfo
[mod
].cells
.items():
1093 print_anyconsts_worker(celltype
, "(|%s_h %s| %s)" % (mod
, cellname
, state
), path
+ "." + cellname
)
1095 for fun
, info
in smt
.modinfo
[mod
].anyconsts
.items():
1098 print_msg("Value for anyconst in %s (%s): %d" % (path
, info
[0], smt
.bv2int(smt
.get("(|%s| %s)" % (fun
, state
)))))
1100 print_msg("Value for anyconst in %s (%s): %s" % (path
, info
[0], smt
.bv2bin(smt
.get("(|%s| %s)" % (fun
, state
)))))
1103 print_msg("Value for anyconst %s.%s (%s): %d" % (path
, info
[1], info
[0], smt
.bv2int(smt
.get("(|%s| %s)" % (fun
, state
)))))
1105 print_msg("Value for anyconst %s.%s (%s): %s" % (path
, info
[1], info
[0], smt
.bv2bin(smt
.get("(|%s| %s)" % (fun
, state
)))))
1108 def print_anyconsts(state
):
1110 print_anyconsts_worker(topmod
, "s%d" % state
, topmod
)
1113 def get_cover_list(mod
, base
):
1114 assert mod
in smt
.modinfo
1119 for expr
, desc
in smt
.modinfo
[mod
].covers
.items():
1120 cover_expr
.append("(ite (|%s| %s) #b1 #b0)" % (expr
, base
))
1121 cover_desc
.append(desc
)
1123 for cell
, submod
in smt
.modinfo
[mod
].cells
.items():
1124 e
, d
= get_cover_list(submod
, "(|%s_h %s| %s)" % (mod
, cell
, base
))
1128 return cover_expr
, cover_desc
1131 asserts_antecedent_cache
= [list()]
1132 asserts_consequent_cache
= [list()]
1133 asserts_cache_dirty
= False
1135 def smt_state(step
):
1136 smt
.write("(declare-fun s%d () |%s_s|)" % (step
, topmod
))
1137 states
.append("s%d" % step
)
1139 def smt_assert(expr
):
1143 smt
.write("(assert %s)" % expr
)
1145 def smt_assert_antecedent(expr
):
1149 smt
.write("(assert %s)" % expr
)
1151 global asserts_cache_dirty
1152 asserts_cache_dirty
= True
1153 asserts_antecedent_cache
[-1].append(expr
)
1155 def smt_assert_consequent(expr
):
1159 smt
.write("(assert %s)" % expr
)
1161 global asserts_cache_dirty
1162 asserts_cache_dirty
= True
1163 asserts_consequent_cache
[-1].append(expr
)
1165 def smt_forall_assert():
1169 global asserts_cache_dirty
1170 asserts_cache_dirty
= False
1172 assert (len(smt
.modinfo
[topmod
].maximize
) + len(smt
.modinfo
[topmod
].minimize
) <= 1)
1174 def make_assert_expr(asserts_cache
):
1176 for lst
in asserts_cache
:
1179 assert len(expr
) != 0
1184 expr
= "(and %s)" % (" ".join(expr
))
1187 antecedent_expr
= make_assert_expr(asserts_antecedent_cache
)
1188 consequent_expr
= make_assert_expr(asserts_consequent_cache
)
1190 states_db
= set(states
)
1191 used_states_db
= set()
1192 new_antecedent_expr
= list()
1193 new_consequent_expr
= list()
1194 assert_expr
= list()
1196 def make_new_expr(new_expr
, expr
):
1198 while cursor
< len(expr
):
1200 if expr
[cursor
] in '|"':
1201 while cursor
+l
+1 < len(expr
) and expr
[cursor
] != expr
[cursor
+l
]:
1204 elif expr
[cursor
] not in '() ':
1205 while cursor
+l
< len(expr
) and expr
[cursor
+l
] not in '|"() ':
1208 word
= expr
[cursor
:cursor
+l
]
1209 if word
in states_db
:
1210 used_states_db
.add(word
)
1213 new_expr
.append(word
)
1216 make_new_expr(new_antecedent_expr
, antecedent_expr
)
1217 make_new_expr(new_consequent_expr
, consequent_expr
)
1219 new_antecedent_expr
= ["".join(new_antecedent_expr
)]
1220 new_consequent_expr
= ["".join(new_consequent_expr
)]
1222 if states
[0] in used_states_db
:
1223 new_antecedent_expr
.append("(|%s_ex_state_eq| %s %s_)" % (topmod
, states
[0], states
[0]))
1225 if s
in used_states_db
:
1226 new_antecedent_expr
.append("(|%s_ex_input_eq| %s %s_)" % (topmod
, s
, s
))
1228 if len(new_antecedent_expr
) == 0:
1229 new_antecedent_expr
= "true"
1230 elif len(new_antecedent_expr
) == 1:
1231 new_antecedent_expr
= new_antecedent_expr
[0]
1233 new_antecedent_expr
= "(and %s)" % (" ".join(new_antecedent_expr
))
1235 if len(new_consequent_expr
) == 0:
1236 new_consequent_expr
= "true"
1237 elif len(new_consequent_expr
) == 1:
1238 new_consequent_expr
= new_consequent_expr
[0]
1240 new_consequent_expr
= "(and %s)" % (" ".join(new_consequent_expr
))
1242 assert_expr
.append("(assert (forall (")
1245 if s
in used_states_db
:
1246 assert_expr
.append("%s(%s_ |%s_s|)" % ("" if first_state
else " ", s
, topmod
))
1248 assert_expr
.append(") (=> %s %s)))" % (new_antecedent_expr
, new_consequent_expr
))
1250 smt
.write("".join(assert_expr
))
1252 if len(smt
.modinfo
[topmod
].maximize
) > 0:
1254 if s
in used_states_db
:
1255 smt
.write("(maximize (|%s| %s))\n" % (smt
.modinfo
[topmod
].maximize
.copy().pop(), s
))
1258 if len(smt
.modinfo
[topmod
].minimize
) > 0:
1260 if s
in used_states_db
:
1261 smt
.write("(minimize (|%s| %s))\n" % (smt
.modinfo
[topmod
].minimize
.copy().pop(), s
))
1265 global asserts_cache_dirty
1266 asserts_cache_dirty
= True
1267 asserts_antecedent_cache
.append(list())
1268 asserts_consequent_cache
.append(list())
1269 smt
.write("(push 1)")
1272 global asserts_cache_dirty
1273 asserts_cache_dirty
= True
1274 asserts_antecedent_cache
.pop()
1275 asserts_consequent_cache
.pop()
1276 smt
.write("(pop 1)")
1278 def smt_check_sat():
1279 if asserts_cache_dirty
:
1281 return smt
.check_sat()
1284 retstatus
= "FAILED"
1285 skip_counter
= step_size
1286 for step
in range(num_steps
, -1, -1):
1288 print_msg("Temporal induction not supported for exists-forall problems.")
1292 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1293 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1294 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1295 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1297 if step
== num_steps
:
1298 smt_assert("(not (and (|%s_a| s%d) %s))" % (topmod
, step
, get_constr_expr(constr_asserts
, step
)))
1301 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
, step
+1))
1302 smt_assert("(|%s_a| s%d)" % (topmod
, step
))
1303 smt_assert(get_constr_expr(constr_asserts
, step
))
1305 if step
> num_steps
-skip_steps
:
1306 print_msg("Skipping induction in step %d.." % (step
))
1310 if skip_counter
< step_size
:
1311 print_msg("Skipping induction in step %d.." % (step
))
1315 print_msg("Trying induction in step %d.." % (step
))
1317 if smt_check_sat() == "sat":
1319 print_msg("Temporal induction failed!")
1320 print_anyconsts(num_steps
)
1321 print_failed_asserts(num_steps
)
1322 write_trace(step
, num_steps
+1, '%')
1325 print_anyconsts(num_steps
)
1326 print_failed_asserts(num_steps
)
1327 write_trace(step
, num_steps
+1, "%d" % step
)
1330 print_msg("Temporal induction successful.")
1331 retstatus
= "PASSED"
1335 cover_expr
, cover_desc
= get_cover_list(topmod
, "state")
1336 cover_mask
= "1" * len(cover_desc
)
1338 if len(cover_expr
) > 1:
1339 cover_expr
= "(concat %s)" % " ".join(cover_expr
)
1340 elif len(cover_expr
) == 1:
1341 cover_expr
= cover_expr
[0]
1346 smt
.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod
, len(cover_desc
), cover_expr
))
1349 retstatus
= "FAILED"
1350 found_failed_assert
= False
1352 assert step_size
== 1
1354 while step
< num_steps
:
1356 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1357 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1358 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1362 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1364 smt_assert_antecedent("(|%s_i| s0)" % (topmod
))
1365 smt_assert_antecedent("(|%s_is| s0)" % (topmod
))
1368 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
-1, step
))
1369 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1371 while "1" in cover_mask
:
1372 print_msg("Checking cover reachability in step %d.." % (step
))
1374 smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx
, step
, "0" * len(cover_desc
)))
1376 if smt_check_sat() == "unsat":
1380 if append_steps
> 0:
1381 for i
in range(step
+1, step
+1+append_steps
):
1382 print_msg("Appending additional step %d." % i
)
1384 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, i
))
1385 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, i
))
1386 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, i
))
1387 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, i
-1, i
))
1388 smt_assert_consequent(get_constr_expr(constr_assumes
, i
))
1389 print_msg("Re-solving with appended steps..")
1390 if smt_check_sat() == "unsat":
1391 print("%s Cannot appended steps without violating assumptions!" % smt
.timestamp())
1392 found_failed_assert
= True
1393 retstatus
= "FAILED"
1396 reached_covers
= smt
.bv2bin(smt
.get("(covers_%d s%d)" % (coveridx
, step
)))
1397 assert len(reached_covers
) == len(cover_desc
)
1401 for i
in range(len(reached_covers
)):
1402 if reached_covers
[i
] == "0":
1403 new_cover_mask
.append(cover_mask
[i
])
1406 print_msg("Reached cover statement at %s in step %d." % (cover_desc
[i
], step
))
1407 new_cover_mask
.append("0")
1409 cover_mask
= "".join(new_cover_mask
)
1411 for i
in range(step
+1+append_steps
):
1412 if print_failed_asserts(i
, extrainfo
=" (step %d)" % i
):
1413 found_failed_assert
= True
1415 write_trace(0, step
+1+append_steps
, "%d" % coveridx
)
1417 if found_failed_assert
:
1422 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
))
1424 if found_failed_assert
:
1427 if "1" not in cover_mask
:
1428 retstatus
= "PASSED"
1433 if "1" in cover_mask
:
1434 for i
in range(len(cover_mask
)):
1435 if cover_mask
[i
] == "1":
1436 print_msg("Unreached cover statement at %s." % cover_desc
[i
])
1438 else: # not tempind, covermode
1440 retstatus
= "PASSED"
1441 while step
< num_steps
:
1443 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1444 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1445 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1449 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1451 smt_assert_antecedent("(|%s_i| s0)" % (topmod
))
1452 smt_assert_antecedent("(|%s_is| s0)" % (topmod
))
1455 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
-1, step
))
1456 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1458 if step
< skip_steps
:
1459 if assume_skipped
is not None and step
>= assume_skipped
:
1460 print_msg("Skipping step %d (and assuming pass).." % (step
))
1461 smt_assert("(|%s_a| s%d)" % (topmod
, step
))
1462 smt_assert(get_constr_expr(constr_asserts
, step
))
1464 print_msg("Skipping step %d.." % (step
))
1468 last_check_step
= step
1469 for i
in range(1, step_size
):
1470 if step
+i
< num_steps
:
1472 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
+i
))
1473 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
+i
))
1474 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
+i
))
1475 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
+i
-1, step
+i
))
1476 smt_assert_consequent(get_constr_expr(constr_assumes
, step
+i
))
1477 last_check_step
= step
+i
1481 if last_check_step
== step
:
1482 print_msg("Checking assumptions in step %d.." % (step
))
1484 print_msg("Checking assumptions in steps %d to %d.." % (step
, last_check_step
))
1486 if smt_check_sat() == "unsat":
1487 print("%s Assumptions are unsatisfiable!" % smt
.timestamp())
1488 retstatus
= "PREUNSAT"
1492 if last_check_step
== step
:
1493 print_msg("Checking assertions in step %d.." % (step
))
1495 print_msg("Checking assertions in steps %d to %d.." % (step
, last_check_step
))
1498 smt_assert("(not (and %s))" % " ".join(["(|%s_a| s%d)" % (topmod
, i
) for i
in range(step
, last_check_step
+1)] +
1499 [get_constr_expr(constr_asserts
, i
) for i
in range(step
, last_check_step
+1)]))
1501 if smt_check_sat() == "sat":
1502 print("%s BMC failed!" % smt
.timestamp())
1503 if append_steps
> 0:
1504 for i
in range(last_check_step
+1, last_check_step
+1+append_steps
):
1505 print_msg("Appending additional step %d." % i
)
1507 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, i
))
1508 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, i
))
1509 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, i
))
1510 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, i
-1, i
))
1511 smt_assert_consequent(get_constr_expr(constr_assumes
, i
))
1512 print_msg("Re-solving with appended steps..")
1513 if smt_check_sat() == "unsat":
1514 print("%s Cannot appended steps without violating assumptions!" % smt
.timestamp())
1515 retstatus
= "FAILED"
1517 print_anyconsts(step
)
1518 for i
in range(step
, last_check_step
+1):
1519 print_failed_asserts(i
)
1520 write_trace(0, last_check_step
+1+append_steps
, '%')
1521 retstatus
= "FAILED"
1526 if (constr_final_start
is not None) or (last_check_step
+1 != num_steps
):
1527 for i
in range(step
, last_check_step
+1):
1528 smt_assert("(|%s_a| s%d)" % (topmod
, i
))
1529 smt_assert(get_constr_expr(constr_asserts
, i
))
1531 if constr_final_start
is not None:
1532 for i
in range(step
, last_check_step
+1):
1533 if i
< constr_final_start
:
1536 print_msg("Checking final constraints in step %d.." % (i
))
1539 smt_assert_consequent(get_constr_expr(constr_assumes
, i
, final
=True))
1540 smt_assert("(not %s)" % get_constr_expr(constr_asserts
, i
, final
=True))
1542 if smt_check_sat() == "sat":
1543 print("%s BMC failed!" % smt
.timestamp())
1545 print_failed_asserts(i
, final
=True)
1546 write_trace(0, i
+1, '%')
1547 retstatus
= "FAILED"
1555 for i
in range(step
, last_check_step
+1):
1556 smt_assert("(|%s_a| s%d)" % (topmod
, i
))
1557 smt_assert(get_constr_expr(constr_asserts
, i
))
1559 print_msg("Solving for step %d.." % (last_check_step
))
1560 if smt_check_sat() != "sat":
1561 print("%s No solution found!" % smt
.timestamp())
1562 retstatus
= "FAILED"
1567 write_trace(0, last_check_step
+1, "%d" % step
)
1571 if gentrace
and retstatus
:
1573 write_trace(0, num_steps
, '%')
1579 print_msg("Status: %s" % retstatus
)
1580 sys
.exit(0 if retstatus
== "PASSED" else 1)