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
58 yosys-smtbmc [options] <yosys_smt2_output>
61 -t <skip_steps>:<num_steps>
62 -t <skip_steps>:<step_size>:<num_steps>
63 default: skip_steps=0, step_size=1, num_steps=20
66 generate an arbitrary trace that satisfies
67 all assertions and assumptions.
70 instead of BMC run temporal induction
73 instead of regular BMC run cover analysis
76 name of the top module
78 --smtc <constr_filename>
82 read cex file as written by ABC's "write_cex -n"
85 read AIGER map file (as written by Yosys' "write_aiger -map")
86 and AIGER witness file. The file names are <prefix>.aim for
87 the map file and <prefix>.aiw for the witness file.
89 --aig <aim_filename>:<aiw_filename>
90 like above, but for map files and witness files that do not
91 share a filename prefix (or use different file extensions).
94 the AIGER witness file does not include the status and
97 --btorwit <btor_witness_filename>
101 only run the core proof, do not collect and print any
102 additional information (e.g. which assert failed)
105 check if the design with assumptions but without assertions
106 is SAT before checking if assertions are UNSAT. This will
107 detect if there are contradicting assumptions. In some cases
108 this will also help to "warm up" the solver, potentially
112 only check final constraints, assume base case
114 --assume-skipped <start_step>
115 assume asserts in skipped steps in BMC.
116 no assumptions are created for skipped steps
119 --dump-vcd <vcd_filename>
120 write trace to this VCD file
121 (hint: use 'write_smt2 -wires' for maximum
122 coverage of signals in generated VCD file)
124 --dump-vlogtb <verilog_filename>
125 write trace as Verilog test bench
127 --vlogtb-top <hierarchical_name>
128 use the given entity as top module for the generated
129 Verilog test bench. The <hierarchical_name> is relative
130 to the design top module without the top module name.
132 --dump-smtc <constr_filename>
133 write trace as constraints file
136 write just the last state as initial constraint to smtc file
138 --smtc-top <old>[:<new>]
139 replace <old> with <new> in constraints dumped to smtc
140 file and only dump object below <old> in design hierarchy.
143 do not assume initial conditions in state 0
146 when using -g or -i, create a dump file for each
147 step. The character '%' is replaces in all dump
148 filenames with the step number.
151 add <num_steps> time steps at the end of the trace
152 when creating a counter example (this additional time
153 steps will still be constrained by assumptions)
156 dump anyconst values as raw bit strings
162 opts
, args
= getopt
.getopt(sys
.argv
[1:], so
.shortopts
+ "t:igcm:", so
.longopts
+
163 ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "btorwit=", "presat",
164 "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
165 "smtc-init", "smtc-top=", "noinit", "binary"])
174 num_steps
= int(a
[0])
176 skip_steps
= int(a
[0])
177 num_steps
= int(a
[1])
179 skip_steps
= int(a
[0])
180 step_size
= int(a
[1])
181 num_steps
= int(a
[2])
184 elif o
== "--assume-skipped":
185 assume_skipped
= int(a
)
186 elif o
== "--final-only":
194 aimfile
, aiwfile
= a
.split(":")
198 elif o
== "--aig-noheader":
200 elif o
== "--btorwit":
202 elif o
== "--dump-vcd":
204 elif o
== "--dump-vlogtb":
206 elif o
== "--vlogtb-top":
208 elif o
== "--dump-smtc":
210 elif o
== "--smtc-init":
212 elif o
== "--smtc-top":
213 smtctop
= a
.split(":")
214 if len(smtctop
) == 1:
216 assert len(smtctop
) == 2
217 smtctop
= tuple(smtctop
)
218 elif o
== "--dump-all":
220 elif o
== "--presat":
222 elif o
== "--noinfo":
224 elif o
== "--noinit":
226 elif o
== "--append":
227 append_steps
= int(a
)
236 elif o
== "--binary":
238 elif so
.handle(o
, a
):
246 if sum([tempind
, gentrace
, covermode
]) > 1:
249 constr_final_start
= None
250 constr_asserts
= defaultdict(list)
251 constr_assumes
= defaultdict(list)
252 constr_write
= list()
255 current_states
= None
258 with
open(fn
, "r") as f
:
262 if line
.startswith("#"):
265 tokens
= line
.split()
270 if tokens
[0] == "initial":
271 current_states
= set()
273 current_states
.add(0)
276 if tokens
[0] == "final":
279 current_states
= set(["final-%d" % i
for i
in range(0, num_steps
+1)])
280 constr_final_start
= 0
281 elif len(tokens
) == 2:
282 arg
= abs(int(tokens
[1]))
283 current_states
= set(["final-%d" % i
for i
in range(arg
, num_steps
+1)])
284 constr_final_start
= arg
if constr_final_start
is None else min(constr_final_start
, arg
)
289 if tokens
[0] == "state":
290 current_states
= set()
292 for token
in tokens
[1:]:
293 tok
= token
.split(":")
295 current_states
.add(int(token
))
302 for i
in range(lower
, upper
+1):
303 current_states
.add(i
)
308 if tokens
[0] == "always":
310 current_states
= set(range(0, num_steps
+1))
311 elif len(tokens
) == 2:
312 arg
= abs(int(tokens
[1]))
313 current_states
= set(range(arg
, num_steps
+1))
318 if tokens
[0] == "assert":
319 assert current_states
is not None
321 for state
in current_states
:
322 constr_asserts
[state
].append(("%s:%d" % (fn
, current_line
), " ".join(tokens
[1:])))
326 if tokens
[0] == "assume":
327 assert current_states
is not None
329 for state
in current_states
:
330 constr_assumes
[state
].append(("%s:%d" % (fn
, current_line
), " ".join(tokens
[1:])))
334 if tokens
[0] == "write":
335 constr_write
.append(" ".join(tokens
[1:]))
338 if tokens
[0] == "logic":
339 so
.logic
= " ".join(tokens
[1:])
345 def get_constr_expr(db
, state
, final
=False, getvalues
=False):
347 if ("final-%d" % state
) not in db
:
348 return ([], [], []) if getvalues
else "true"
351 return ([], [], []) if getvalues
else "true"
353 netref_regex
= re
.compile(r
'(^|[( ])\[(-?[0-9]+:|)([^\]]*|\S*)\](?=[ )]|$)')
355 def replace_netref(match
):
356 state_sel
= match
.group(2)
360 elif state_sel
[0] == "-":
361 st
= state
+ int(state_sel
[:-1])
363 st
= int(state_sel
[:-1])
365 expr
= smt
.net_expr(topmod
, "s%d" % st
, smt
.get_path(topmod
, match
.group(3)))
367 return match
.group(1) + expr
370 for loc
, expr
in db
[("final-%d" % state
) if final
else state
]:
371 actual_expr
= netref_regex
.sub(replace_netref
, expr
)
373 expr_list
.append((loc
, expr
, actual_expr
))
375 expr_list
.append(actual_expr
)
378 loc_list
, expr_list
, acual_expr_list
= zip(*expr_list
)
379 value_list
= smt
.get_list(acual_expr_list
)
380 return loc_list
, expr_list
, value_list
382 if len(expr_list
) == 0:
385 if len(expr_list
) == 1:
388 return "(and %s)" % " ".join(expr_list
)
393 if noinfo
and vcdfile
is None and vlogtbfile
is None and outconstr
is None:
394 smt
.produce_models
= False
397 print("%s %s" % (smt
.timestamp(), msg
))
400 print_msg("Solver: %s" % (so
.solver
))
402 with
open(args
[0], "r") as f
:
406 for line
in constr_write
:
412 assert topmod
is not None
413 assert topmod
in smt
.modinfo
415 if cexfile
is not None:
421 with
open(cexfile
, "r") as f
:
422 cex_regex
= re
.compile(r
'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
423 for entry
in f
.read().split():
424 match
= cex_regex
.match(entry
)
427 name
, bit
, extra_name
, step
, val
= match
.group(1), match
.group(2), match
.group(3), match
.group(4), match
.group(5)
432 if name
not in smt
.modinfo
[topmod
].inputs
:
443 if smt
.modinfo
[topmod
].wsize
[name
] == 1:
445 smtexpr
= "(= [%s] %s)" % (name
, "true" if val
else "false")
447 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bit
, bit
, name
, val
)
449 # print("cex@%d: %s" % (step, smtexpr))
450 constr_assumes
[step
].append((cexfile
, smtexpr
))
453 skip_steps
= max(skip_steps
, step
)
454 num_steps
= max(num_steps
, step
+1)
456 if aimfile
is not None:
466 with
open(aimfile
, "r") as f
:
467 for entry
in f
.read().splitlines():
468 entry
= entry
.split()
470 if entry
[0] == "input":
471 input_map
[int(entry
[1])] = (entry
[3], int(entry
[2]))
474 if entry
[0] == "init":
475 init_map
[int(entry
[1])] = (entry
[3], int(entry
[2]))
478 if entry
[0] in ["latch", "invlatch"]:
479 latch_map
[int(entry
[1])] = (entry
[3], int(entry
[2]), entry
[0] == "invlatch")
482 if entry
[0] in ["output", "wire"]:
487 with
open(aiwfile
, "r") as f
:
495 for entry
in f
.read().splitlines():
496 if len(entry
) == 0 or entry
[0] in "bcjfu.":
506 if len(init_map
) == 0:
507 for i
in range(len(entry
)):
512 value
= int(entry
[i
])
513 name
= latch_map
[i
][0]
514 bitidx
= latch_map
[i
][1]
515 invert
= latch_map
[i
][2]
520 path
= smt
.get_path(topmod
, name
)
521 width
= smt
.net_width(topmod
, path
)
525 smtexpr
= "(= [%s] %s)" % (name
, "true" if value
else "false")
527 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx
, bitidx
, name
, value
)
529 constr_assumes
[0].append((cexfile
, smtexpr
))
532 for i
in range(len(entry
)):
536 if (step
== 0) and (i
in init_map
):
537 value
= int(entry
[i
])
538 name
= init_map
[i
][0]
539 bitidx
= init_map
[i
][1]
541 path
= smt
.get_path(topmod
, name
)
543 if not smt
.net_exists(topmod
, path
):
544 match
= re
.match(r
"(.*)\[(\d+)\]$", path
[-1])
546 path
[-1] = match
.group(1)
547 addr
= int(match
.group(2))
549 if not match
or not smt
.mem_exists(topmod
, path
):
550 print_msg("Ignoring init value for unknown net: %s" % (name
))
553 meminfo
= smt
.mem_info(topmod
, path
)
554 smtexpr
= "(select [%s] #b%s)" % (".".join(path
), bin(addr
)[2:].zfill(meminfo
[0]))
558 smtexpr
= "[%s]" % name
559 width
= smt
.net_width(topmod
, path
)
563 smtexpr
= "(= %s %s)" % (smtexpr
, "true" if value
else "false")
565 smtexpr
= "(= ((_ extract %d %d) %s) #b%d)" % (bitidx
, bitidx
, smtexpr
, value
)
567 constr_assumes
[0].append((cexfile
, smtexpr
))
570 value
= int(entry
[i
])
571 name
= input_map
[i
][0]
572 bitidx
= input_map
[i
][1]
574 path
= smt
.get_path(topmod
, name
)
575 width
= smt
.net_width(topmod
, path
)
579 smtexpr
= "(= [%s] %s)" % (name
, "true" if value
else "false")
581 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx
, bitidx
, name
, value
)
583 constr_assumes
[step
].append((cexfile
, smtexpr
))
586 skip_steps
= max(skip_steps
, step
)
587 num_steps
= max(num_steps
, step
+1)
590 if btorwitfile
is not None:
591 with
open(btorwitfile
, "r") as f
:
607 if line
== "" or line
[0] == "b" or line
[0] == "j":
613 if line
[0] == '#' or line
[0] == '@':
618 altsuffix
= "#" + suffix
[1:]
620 altsuffix
= "@" + suffix
[1:]
628 if line
[-1].endswith(suffix
):
629 line
[-1] = line
[-1][0:len(line
[-1]) - len(suffix
)]
631 if line
[-1].endswith(altsuffix
):
632 line
[-1] = line
[-1][0:len(line
[-1]) - len(altsuffix
)]
634 if line
[-1][0] == "$":
638 if len(line
) == 3 and line
[1][0] != "[":
642 path
= smt
.get_path(topmod
, name
)
644 if not smt
.net_exists(topmod
, path
):
647 width
= smt
.net_width(topmod
, path
)
650 assert value
in ["0", "1"]
651 value
= "true" if value
== "1" else "false"
655 smtexpr
= "(= [%s] %s)" % (name
, value
)
656 constr_assumes
[step
].append((btorwitfile
, smtexpr
))
659 if len(line
) == 4 and line
[1][0] == "[":
664 path
= smt
.get_path(topmod
, name
)
666 if not smt
.mem_exists(topmod
, path
):
669 meminfo
= smt
.mem_info(topmod
, path
)
672 assert value
in ["0", "1"]
673 value
= "true" if value
== "1" else "false"
677 assert index
[0] == "["
678 assert index
[-1] == "]"
679 index
= "#b" + index
[1:-1]
681 smtexpr
= "(= (select [%s] %s) %s)" % (name
, index
, value
)
682 constr_assumes
[step
].append((btorwitfile
, smtexpr
))
687 def write_vcd_trace(steps_start
, steps_stop
, index
):
688 filename
= vcdfile
.replace("%", index
)
689 print_msg("Writing trace to VCD file: %s" % (filename
))
691 with
open(filename
, "w") as vcd_file
:
692 vcd
= MkVcd(vcd_file
)
695 for netpath
in sorted(smt
.hiernets(topmod
)):
698 if n
.startswith("$"):
701 edge
= smt
.net_clock(topmod
, netpath
)
703 vcd
.add_net([topmod
] + netpath
, smt
.net_width(topmod
, netpath
))
705 vcd
.add_clock([topmod
] + netpath
, edge
)
706 path_list
.append(netpath
)
708 mem_trace_data
= dict()
709 for mempath
in sorted(smt
.hiermems(topmod
)):
710 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(topmod
, mempath
)
714 for i
in range(steps_start
, steps_stop
):
715 for j
in range(rports
):
716 expr_id
.append(('R', i
-steps_start
, j
, 'A'))
717 expr_id
.append(('R', i
-steps_start
, j
, 'D'))
718 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "R%dA" % j
))
719 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "R%dD" % j
))
720 for j
in range(wports
):
721 expr_id
.append(('W', i
-steps_start
, j
, 'A'))
722 expr_id
.append(('W', i
-steps_start
, j
, 'D'))
723 expr_id
.append(('W', i
-steps_start
, j
, 'M'))
724 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dA" % j
))
725 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dD" % j
))
726 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dM" % j
))
732 for eid
, edat
in zip(expr_id
, smt
.get_list(expr_list
)):
750 c
[f
] = smt
.bv2bin(edat
)
760 if len(wdata
) == 0 and len(rdata
) != 0:
761 wdata
= [[]] * len(rdata
)
763 assert len(rdata
) == len(wdata
)
765 for i
in range(len(wdata
)):
767 for j_data
in rdata
[i
]:
768 if j_data
["A"] == addr
:
769 data
= list(j_data
["D"])
775 for i
in reversed(range(len(tdata
))):
776 for k
in range(width
):
777 if tdata
[i
][k
] == "x":
783 tdata
.append(data
[:])
785 for j_data
in wdata
[i
]:
786 if j_data
["A"] != addr
:
792 for k
in range(width
):
797 tdata
.append(data
[:])
799 assert len(tdata
) == len(rdata
)
802 netpath
[-1] += "<%0*x>" % ((len(addr
)+3) // 4, int(addr
, 2))
803 vcd
.add_net([topmod
] + netpath
, width
)
805 for i
in range(steps_start
, steps_stop
):
806 if i
not in mem_trace_data
:
807 mem_trace_data
[i
] = list()
808 mem_trace_data
[i
].append((netpath
, "".join(tdata
[i
-steps_start
])))
810 for i
in range(steps_start
, steps_stop
):
812 value_list
= smt
.get_net_bin_list(topmod
, path_list
, "s%d" % i
)
813 for path
, value
in zip(path_list
, value_list
):
814 vcd
.set_net([topmod
] + path
, value
)
815 if i
in mem_trace_data
:
816 for path
, value
in mem_trace_data
[i
]:
817 vcd
.set_net([topmod
] + path
, value
)
819 vcd
.set_time(steps_stop
)
822 def write_vlogtb_trace(steps_start
, steps_stop
, index
):
823 filename
= vlogtbfile
.replace("%", index
)
824 print_msg("Writing trace to Verilog testbench: %s" % (filename
))
826 vlogtb_topmod
= topmod
827 vlogtb_state
= "s@@step_idx@@"
829 if vlogtbtop
is not None:
830 for item
in vlogtbtop
.split("."):
831 if item
in smt
.modinfo
[vlogtb_topmod
].cells
:
832 vlogtb_state
= "(|%s_h %s| %s)" % (vlogtb_topmod
, item
, vlogtb_state
)
833 vlogtb_topmod
= smt
.modinfo
[vlogtb_topmod
].cells
[item
]
835 print_msg("Vlog top module '%s' not found: no cell '%s' in module '%s'" % (vlogtbtop
, item
, vlogtb_topmod
))
838 with
open(filename
, "w") as f
:
839 print("`ifndef VERILATOR", file=f
)
840 print("module testbench;", file=f
)
841 print(" reg [4095:0] vcdfile;", file=f
)
842 print(" reg clock;", file=f
)
843 print("`else", file=f
)
844 print("module testbench(input clock, output reg genclock);", file=f
)
845 print(" initial genclock = 1;", file=f
)
846 print("`endif", file=f
)
848 print(" reg genclock = 1;", file=f
)
849 print(" reg [31:0] cycle = 0;", file=f
)
851 primary_inputs
= list()
854 for name
in smt
.modinfo
[vlogtb_topmod
].inputs
:
855 if name
in ["clk", "clock", "CLK", "CLOCK"]:
856 clock_inputs
.add(name
)
857 width
= smt
.modinfo
[vlogtb_topmod
].wsize
[name
]
858 primary_inputs
.append((name
, width
))
860 for name
, width
in primary_inputs
:
861 if name
in clock_inputs
:
862 print(" wire [%d:0] PI_%s = clock;" % (width
-1, name
), file=f
)
864 print(" reg [%d:0] PI_%s;" % (width
-1, name
), file=f
)
866 print(" %s UUT (" % vlogtb_topmod
, file=f
)
867 print(",\n".join(" .{name}(PI_{name})".format(name
=name
) for name
, _
in primary_inputs
), file=f
)
870 print("`ifndef VERILATOR", file=f
)
871 print(" initial begin", file=f
)
872 print(" if ($value$plusargs(\"vcd=%s\", vcdfile)) begin", file=f
)
873 print(" $dumpfile(vcdfile);", file=f
)
874 print(" $dumpvars(0, testbench);", file=f
)
875 print(" end", file=f
)
876 print(" #5 clock = 0;", file=f
)
877 print(" while (genclock) begin", file=f
)
878 print(" #5 clock = 0;", file=f
)
879 print(" #5 clock = 1;", file=f
)
880 print(" end", file=f
)
881 print(" end", file=f
)
882 print("`endif", file=f
)
884 print(" initial begin", file=f
)
886 regs
= sorted(smt
.hiernets(vlogtb_topmod
, regs_only
=True))
887 regvals
= smt
.get_net_bin_list(vlogtb_topmod
, regs
, vlogtb_state
.replace("@@step_idx@@", str(steps_start
)))
889 print("`ifndef VERILATOR", file=f
)
890 print(" #1;", file=f
)
891 print("`endif", file=f
)
892 for reg
, val
in zip(regs
, regvals
):
895 if n
.startswith("$"):
897 print(" %sUUT.%s = %d'b%s;" % ("// " if hidden_net
else "", ".".join(reg
), len(val
), val
), file=f
)
899 anyconsts
= sorted(smt
.hieranyconsts(vlogtb_topmod
))
900 for info
in anyconsts
:
901 if info
[3] is not None:
902 modstate
= smt
.net_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(steps_start
)), info
[0])
903 value
= smt
.bv2bin(smt
.get("(|%s| %s)" % (info
[1], modstate
)))
904 print(" UUT.%s = %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
906 mems
= sorted(smt
.hiermems(vlogtb_topmod
))
908 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(vlogtb_topmod
, mempath
)
910 addr_expr_list
= list()
911 data_expr_list
= list()
912 for i
in range(steps_start
, steps_stop
):
913 for j
in range(rports
):
914 addr_expr_list
.append(smt
.mem_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dA" % j
))
915 data_expr_list
.append(smt
.mem_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dD" % j
))
917 addr_list
= smt
.get_list(addr_expr_list
)
918 data_list
= smt
.get_list(data_expr_list
)
921 for addr
, data
in zip(addr_list
, data_list
):
922 addr
= smt
.bv2bin(addr
)
923 data
= smt
.bv2bin(data
)
924 if addr
not in addr_data
:
925 addr_data
[addr
] = data
927 for addr
, data
in addr_data
.items():
928 print(" UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath
), len(addr
), addr
, len(data
), data
), file=f
)
931 anyseqs
= sorted(smt
.hieranyseqs(vlogtb_topmod
))
933 for i
in range(steps_start
, steps_stop
):
934 pi_names
= [[name
] for name
, _
in primary_inputs
if name
not in clock_inputs
]
935 pi_values
= smt
.get_net_bin_list(vlogtb_topmod
, pi_names
, vlogtb_state
.replace("@@step_idx@@", str(i
)))
937 print(" // state %d" % i
, file=f
)
940 print(" if (cycle == %d) begin" % (i
-1), file=f
)
942 for name
, val
in zip(pi_names
, pi_values
):
944 print(" PI_%s <= %d'b%s;" % (".".join(name
), len(val
), val
), file=f
)
946 print(" PI_%s = %d'b%s;" % (".".join(name
), len(val
), val
), file=f
)
949 if info
[3] is not None:
950 modstate
= smt
.net_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), info
[0])
951 value
= smt
.bv2bin(smt
.get("(|%s| %s)" % (info
[1], modstate
)))
953 print(" UUT.%s <= %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
955 print(" UUT.%s = %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
958 print(" end", file=f
)
962 print(" end", file=f
)
963 print(" always @(posedge clock) begin", file=f
)
965 print(" genclock <= cycle < %d;" % (steps_stop
-1), file=f
)
966 print(" cycle <= cycle + 1;", file=f
)
967 print(" end", file=f
)
969 print("endmodule", file=f
)
972 def write_constr_trace(steps_start
, steps_stop
, index
):
973 filename
= outconstr
.replace("%", index
)
974 print_msg("Writing trace to constraints file: %s" % (filename
))
976 constr_topmod
= topmod
977 constr_state
= "s@@step_idx@@"
980 if smtctop
is not None:
981 for item
in smtctop
[0].split("."):
982 assert item
in smt
.modinfo
[constr_topmod
].cells
983 constr_state
= "(|%s_h %s| %s)" % (constr_topmod
, item
, constr_state
)
984 constr_topmod
= smt
.modinfo
[constr_topmod
].cells
[item
]
986 constr_prefix
= smtctop
[1] + "."
989 steps_start
= steps_stop
- 1
991 with
open(filename
, "w") as f
:
992 primary_inputs
= list()
994 for name
in smt
.modinfo
[constr_topmod
].inputs
:
995 width
= smt
.modinfo
[constr_topmod
].wsize
[name
]
996 primary_inputs
.append((name
, width
))
998 if steps_start
== 0 or smtcinit
:
999 print("initial", file=f
)
1001 print("state %d" % steps_start
, file=f
)
1003 regnames
= sorted(smt
.hiernets(constr_topmod
, regs_only
=True))
1004 regvals
= smt
.get_net_list(constr_topmod
, regnames
, constr_state
.replace("@@step_idx@@", str(steps_start
)))
1006 for name
, val
in zip(regnames
, regvals
):
1007 print("assume (= [%s%s] %s)" % (constr_prefix
, ".".join(name
), val
), file=f
)
1009 mems
= sorted(smt
.hiermems(constr_topmod
))
1010 for mempath
in mems
:
1011 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(constr_topmod
, mempath
)
1013 addr_expr_list
= list()
1014 data_expr_list
= list()
1015 for i
in range(steps_start
, steps_stop
):
1016 for j
in range(rports
):
1017 addr_expr_list
.append(smt
.mem_expr(constr_topmod
, constr_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dA" % j
))
1018 data_expr_list
.append(smt
.mem_expr(constr_topmod
, constr_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dD" % j
))
1020 addr_list
= smt
.get_list(addr_expr_list
)
1021 data_list
= smt
.get_list(data_expr_list
)
1024 for addr
, data
in zip(addr_list
, data_list
):
1025 if addr
not in addr_data
:
1026 addr_data
[addr
] = data
1028 for addr
, data
in addr_data
.items():
1029 print("assume (= (select [%s%s] %s) %s)" % (constr_prefix
, ".".join(mempath
), addr
, data
), file=f
)
1031 for k
in range(steps_start
, steps_stop
):
1034 print("state %d" % k
, file=f
)
1036 pi_names
= [[name
] for name
, _
in sorted(primary_inputs
)]
1037 pi_values
= smt
.get_net_list(constr_topmod
, pi_names
, constr_state
.replace("@@step_idx@@", str(k
)))
1039 for name
, val
in zip(pi_names
, pi_values
):
1040 print("assume (= [%s%s] %s)" % (constr_prefix
, ".".join(name
), val
), file=f
)
1043 def write_trace(steps_start
, steps_stop
, index
):
1044 if vcdfile
is not None:
1045 write_vcd_trace(steps_start
, steps_stop
, index
)
1047 if vlogtbfile
is not None:
1048 write_vlogtb_trace(steps_start
, steps_stop
, index
)
1050 if outconstr
is not None:
1051 write_constr_trace(steps_start
, steps_stop
, index
)
1054 def print_failed_asserts_worker(mod
, state
, path
, extrainfo
):
1055 assert mod
in smt
.modinfo
1056 found_failed_assert
= False
1058 if smt
.get("(|%s_a| %s)" % (mod
, state
)) in ["true", "#b1"]:
1061 for cellname
, celltype
in smt
.modinfo
[mod
].cells
.items():
1062 if print_failed_asserts_worker(celltype
, "(|%s_h %s| %s)" % (mod
, cellname
, state
), path
+ "." + cellname
, extrainfo
):
1063 found_failed_assert
= True
1065 for assertfun
, assertinfo
in smt
.modinfo
[mod
].asserts
.items():
1066 if smt
.get("(|%s| %s)" % (assertfun
, state
)) in ["false", "#b0"]:
1067 print_msg("Assert failed in %s: %s%s" % (path
, assertinfo
, extrainfo
))
1068 found_failed_assert
= True
1070 return found_failed_assert
1073 def print_failed_asserts(state
, final
=False, extrainfo
=""):
1075 loc_list
, expr_list
, value_list
= get_constr_expr(constr_asserts
, state
, final
=final
, getvalues
=True)
1076 found_failed_assert
= False
1078 for loc
, expr
, value
in zip(loc_list
, expr_list
, value_list
):
1079 if smt
.bv2int(value
) == 0:
1080 print_msg("Assert %s failed: %s%s" % (loc
, expr
, extrainfo
))
1081 found_failed_assert
= True
1084 if print_failed_asserts_worker(topmod
, "s%d" % state
, topmod
, extrainfo
):
1085 found_failed_assert
= True
1087 return found_failed_assert
1090 def print_anyconsts_worker(mod
, state
, path
):
1091 assert mod
in smt
.modinfo
1093 for cellname
, celltype
in smt
.modinfo
[mod
].cells
.items():
1094 print_anyconsts_worker(celltype
, "(|%s_h %s| %s)" % (mod
, cellname
, state
), path
+ "." + cellname
)
1096 for fun
, info
in smt
.modinfo
[mod
].anyconsts
.items():
1099 print_msg("Value for anyconst in %s (%s): %d" % (path
, info
[0], smt
.bv2int(smt
.get("(|%s| %s)" % (fun
, state
)))))
1101 print_msg("Value for anyconst in %s (%s): %s" % (path
, info
[0], smt
.bv2bin(smt
.get("(|%s| %s)" % (fun
, state
)))))
1104 print_msg("Value for anyconst %s.%s (%s): %d" % (path
, info
[1], info
[0], smt
.bv2int(smt
.get("(|%s| %s)" % (fun
, state
)))))
1106 print_msg("Value for anyconst %s.%s (%s): %s" % (path
, info
[1], info
[0], smt
.bv2bin(smt
.get("(|%s| %s)" % (fun
, state
)))))
1109 def print_anyconsts(state
):
1111 print_anyconsts_worker(topmod
, "s%d" % state
, topmod
)
1114 def get_cover_list(mod
, base
):
1115 assert mod
in smt
.modinfo
1120 for expr
, desc
in smt
.modinfo
[mod
].covers
.items():
1121 cover_expr
.append("(ite (|%s| %s) #b1 #b0)" % (expr
, base
))
1122 cover_desc
.append(desc
)
1124 for cell
, submod
in smt
.modinfo
[mod
].cells
.items():
1125 e
, d
= get_cover_list(submod
, "(|%s_h %s| %s)" % (mod
, cell
, base
))
1129 return cover_expr
, cover_desc
1132 asserts_antecedent_cache
= [list()]
1133 asserts_consequent_cache
= [list()]
1134 asserts_cache_dirty
= False
1136 def smt_state(step
):
1137 smt
.write("(declare-fun s%d () |%s_s|)" % (step
, topmod
))
1138 states
.append("s%d" % step
)
1140 def smt_assert(expr
):
1144 smt
.write("(assert %s)" % expr
)
1146 def smt_assert_antecedent(expr
):
1150 smt
.write("(assert %s)" % expr
)
1152 global asserts_cache_dirty
1153 asserts_cache_dirty
= True
1154 asserts_antecedent_cache
[-1].append(expr
)
1156 def smt_assert_consequent(expr
):
1160 smt
.write("(assert %s)" % expr
)
1162 global asserts_cache_dirty
1163 asserts_cache_dirty
= True
1164 asserts_consequent_cache
[-1].append(expr
)
1166 def smt_forall_assert():
1170 global asserts_cache_dirty
1171 asserts_cache_dirty
= False
1173 assert (len(smt
.modinfo
[topmod
].maximize
) + len(smt
.modinfo
[topmod
].minimize
) <= 1)
1175 def make_assert_expr(asserts_cache
):
1177 for lst
in asserts_cache
:
1180 assert len(expr
) != 0
1185 expr
= "(and %s)" % (" ".join(expr
))
1188 antecedent_expr
= make_assert_expr(asserts_antecedent_cache
)
1189 consequent_expr
= make_assert_expr(asserts_consequent_cache
)
1191 states_db
= set(states
)
1192 used_states_db
= set()
1193 new_antecedent_expr
= list()
1194 new_consequent_expr
= list()
1195 assert_expr
= list()
1197 def make_new_expr(new_expr
, expr
):
1199 while cursor
< len(expr
):
1201 if expr
[cursor
] in '|"':
1202 while cursor
+l
+1 < len(expr
) and expr
[cursor
] != expr
[cursor
+l
]:
1205 elif expr
[cursor
] not in '() ':
1206 while cursor
+l
< len(expr
) and expr
[cursor
+l
] not in '|"() ':
1209 word
= expr
[cursor
:cursor
+l
]
1210 if word
in states_db
:
1211 used_states_db
.add(word
)
1214 new_expr
.append(word
)
1217 make_new_expr(new_antecedent_expr
, antecedent_expr
)
1218 make_new_expr(new_consequent_expr
, consequent_expr
)
1220 new_antecedent_expr
= ["".join(new_antecedent_expr
)]
1221 new_consequent_expr
= ["".join(new_consequent_expr
)]
1223 if states
[0] in used_states_db
:
1224 new_antecedent_expr
.append("(|%s_ex_state_eq| %s %s_)" % (topmod
, states
[0], states
[0]))
1226 if s
in used_states_db
:
1227 new_antecedent_expr
.append("(|%s_ex_input_eq| %s %s_)" % (topmod
, s
, s
))
1229 if len(new_antecedent_expr
) == 0:
1230 new_antecedent_expr
= "true"
1231 elif len(new_antecedent_expr
) == 1:
1232 new_antecedent_expr
= new_antecedent_expr
[0]
1234 new_antecedent_expr
= "(and %s)" % (" ".join(new_antecedent_expr
))
1236 if len(new_consequent_expr
) == 0:
1237 new_consequent_expr
= "true"
1238 elif len(new_consequent_expr
) == 1:
1239 new_consequent_expr
= new_consequent_expr
[0]
1241 new_consequent_expr
= "(and %s)" % (" ".join(new_consequent_expr
))
1243 assert_expr
.append("(assert (forall (")
1246 if s
in used_states_db
:
1247 assert_expr
.append("%s(%s_ |%s_s|)" % ("" if first_state
else " ", s
, topmod
))
1249 assert_expr
.append(") (=> %s %s)))" % (new_antecedent_expr
, new_consequent_expr
))
1251 smt
.write("".join(assert_expr
))
1253 if len(smt
.modinfo
[topmod
].maximize
) > 0:
1255 if s
in used_states_db
:
1256 smt
.write("(maximize (|%s| %s))\n" % (smt
.modinfo
[topmod
].maximize
.copy().pop(), s
))
1259 if len(smt
.modinfo
[topmod
].minimize
) > 0:
1261 if s
in used_states_db
:
1262 smt
.write("(minimize (|%s| %s))\n" % (smt
.modinfo
[topmod
].minimize
.copy().pop(), s
))
1266 global asserts_cache_dirty
1267 asserts_cache_dirty
= True
1268 asserts_antecedent_cache
.append(list())
1269 asserts_consequent_cache
.append(list())
1270 smt
.write("(push 1)")
1273 global asserts_cache_dirty
1274 asserts_cache_dirty
= True
1275 asserts_antecedent_cache
.pop()
1276 asserts_consequent_cache
.pop()
1277 smt
.write("(pop 1)")
1279 def smt_check_sat():
1280 if asserts_cache_dirty
:
1282 return smt
.check_sat()
1285 retstatus
= "FAILED"
1286 skip_counter
= step_size
1287 for step
in range(num_steps
, -1, -1):
1289 print_msg("Temporal induction not supported for exists-forall problems.")
1293 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1294 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1295 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1296 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1298 if step
== num_steps
:
1299 smt_assert("(not (and (|%s_a| s%d) %s))" % (topmod
, step
, get_constr_expr(constr_asserts
, step
)))
1302 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
, step
+1))
1303 smt_assert("(|%s_a| s%d)" % (topmod
, step
))
1304 smt_assert(get_constr_expr(constr_asserts
, step
))
1306 if step
> num_steps
-skip_steps
:
1307 print_msg("Skipping induction in step %d.." % (step
))
1311 if skip_counter
< step_size
:
1312 print_msg("Skipping induction in step %d.." % (step
))
1316 print_msg("Trying induction in step %d.." % (step
))
1318 if smt_check_sat() == "sat":
1320 print_msg("Temporal induction failed!")
1321 print_anyconsts(num_steps
)
1322 print_failed_asserts(num_steps
)
1323 write_trace(step
, num_steps
+1, '%')
1326 print_anyconsts(num_steps
)
1327 print_failed_asserts(num_steps
)
1328 write_trace(step
, num_steps
+1, "%d" % step
)
1331 print_msg("Temporal induction successful.")
1332 retstatus
= "PASSED"
1336 cover_expr
, cover_desc
= get_cover_list(topmod
, "state")
1337 cover_mask
= "1" * len(cover_desc
)
1339 if len(cover_expr
) > 1:
1340 cover_expr
= "(concat %s)" % " ".join(cover_expr
)
1341 elif len(cover_expr
) == 1:
1342 cover_expr
= cover_expr
[0]
1347 smt
.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod
, len(cover_desc
), cover_expr
))
1350 retstatus
= "FAILED"
1351 found_failed_assert
= False
1353 assert step_size
== 1
1355 while step
< num_steps
:
1357 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1358 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1359 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1363 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1365 smt_assert_antecedent("(|%s_i| s0)" % (topmod
))
1366 smt_assert_antecedent("(|%s_is| s0)" % (topmod
))
1369 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
-1, step
))
1370 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1372 while "1" in cover_mask
:
1373 print_msg("Checking cover reachability in step %d.." % (step
))
1375 smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx
, step
, "0" * len(cover_desc
)))
1377 if smt_check_sat() == "unsat":
1381 if append_steps
> 0:
1382 for i
in range(step
+1, step
+1+append_steps
):
1383 print_msg("Appending additional step %d." % i
)
1385 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, i
))
1386 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, i
))
1387 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, i
))
1388 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, i
-1, i
))
1389 smt_assert_consequent(get_constr_expr(constr_assumes
, i
))
1390 print_msg("Re-solving with appended steps..")
1391 if smt_check_sat() == "unsat":
1392 print("%s Cannot appended steps without violating assumptions!" % smt
.timestamp())
1393 found_failed_assert
= True
1394 retstatus
= "FAILED"
1397 reached_covers
= smt
.bv2bin(smt
.get("(covers_%d s%d)" % (coveridx
, step
)))
1398 assert len(reached_covers
) == len(cover_desc
)
1402 for i
in range(len(reached_covers
)):
1403 if reached_covers
[i
] == "0":
1404 new_cover_mask
.append(cover_mask
[i
])
1407 print_msg("Reached cover statement at %s in step %d." % (cover_desc
[i
], step
))
1408 new_cover_mask
.append("0")
1410 cover_mask
= "".join(new_cover_mask
)
1412 for i
in range(step
+1+append_steps
):
1413 if print_failed_asserts(i
, extrainfo
=" (step %d)" % i
):
1414 found_failed_assert
= True
1416 write_trace(0, step
+1+append_steps
, "%d" % coveridx
)
1418 if found_failed_assert
:
1423 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
))
1425 if found_failed_assert
:
1428 if "1" not in cover_mask
:
1429 retstatus
= "PASSED"
1434 if "1" in cover_mask
:
1435 for i
in range(len(cover_mask
)):
1436 if cover_mask
[i
] == "1":
1437 print_msg("Unreached cover statement at %s." % cover_desc
[i
])
1439 else: # not tempind, covermode
1441 retstatus
= "PASSED"
1442 while step
< num_steps
:
1444 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1445 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1446 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1450 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1452 smt_assert_antecedent("(|%s_i| s0)" % (topmod
))
1453 smt_assert_antecedent("(|%s_is| s0)" % (topmod
))
1456 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
-1, step
))
1457 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1459 if step
< skip_steps
:
1460 if assume_skipped
is not None and step
>= assume_skipped
:
1461 print_msg("Skipping step %d (and assuming pass).." % (step
))
1462 smt_assert("(|%s_a| s%d)" % (topmod
, step
))
1463 smt_assert(get_constr_expr(constr_asserts
, step
))
1465 print_msg("Skipping step %d.." % (step
))
1469 last_check_step
= step
1470 for i
in range(1, step_size
):
1471 if step
+i
< num_steps
:
1473 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
+i
))
1474 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
+i
))
1475 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
+i
))
1476 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
+i
-1, step
+i
))
1477 smt_assert_consequent(get_constr_expr(constr_assumes
, step
+i
))
1478 last_check_step
= step
+i
1482 if last_check_step
== step
:
1483 print_msg("Checking assumptions in step %d.." % (step
))
1485 print_msg("Checking assumptions in steps %d to %d.." % (step
, last_check_step
))
1487 if smt_check_sat() == "unsat":
1488 print("%s Assumptions are unsatisfiable!" % smt
.timestamp())
1489 retstatus
= "PREUNSAT"
1493 if last_check_step
== step
:
1494 print_msg("Checking assertions in step %d.." % (step
))
1496 print_msg("Checking assertions in steps %d to %d.." % (step
, last_check_step
))
1499 smt_assert("(not (and %s))" % " ".join(["(|%s_a| s%d)" % (topmod
, i
) for i
in range(step
, last_check_step
+1)] +
1500 [get_constr_expr(constr_asserts
, i
) for i
in range(step
, last_check_step
+1)]))
1502 if smt_check_sat() == "sat":
1503 print("%s BMC failed!" % smt
.timestamp())
1504 if append_steps
> 0:
1505 for i
in range(last_check_step
+1, last_check_step
+1+append_steps
):
1506 print_msg("Appending additional step %d." % i
)
1508 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, i
))
1509 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, i
))
1510 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, i
))
1511 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, i
-1, i
))
1512 smt_assert_consequent(get_constr_expr(constr_assumes
, i
))
1513 print_msg("Re-solving with appended steps..")
1514 if smt_check_sat() == "unsat":
1515 print("%s Cannot appended steps without violating assumptions!" % smt
.timestamp())
1516 retstatus
= "FAILED"
1518 print_anyconsts(step
)
1519 for i
in range(step
, last_check_step
+1):
1520 print_failed_asserts(i
)
1521 write_trace(0, last_check_step
+1+append_steps
, '%')
1522 retstatus
= "FAILED"
1527 if (constr_final_start
is not None) or (last_check_step
+1 != num_steps
):
1528 for i
in range(step
, last_check_step
+1):
1529 smt_assert("(|%s_a| s%d)" % (topmod
, i
))
1530 smt_assert(get_constr_expr(constr_asserts
, i
))
1532 if constr_final_start
is not None:
1533 for i
in range(step
, last_check_step
+1):
1534 if i
< constr_final_start
:
1537 print_msg("Checking final constraints in step %d.." % (i
))
1540 smt_assert_consequent(get_constr_expr(constr_assumes
, i
, final
=True))
1541 smt_assert("(not %s)" % get_constr_expr(constr_asserts
, i
, final
=True))
1543 if smt_check_sat() == "sat":
1544 print("%s BMC failed!" % smt
.timestamp())
1546 print_failed_asserts(i
, final
=True)
1547 write_trace(0, i
+1, '%')
1548 retstatus
= "FAILED"
1556 for i
in range(step
, last_check_step
+1):
1557 smt_assert("(|%s_a| s%d)" % (topmod
, i
))
1558 smt_assert(get_constr_expr(constr_asserts
, i
))
1560 print_msg("Solving for step %d.." % (last_check_step
))
1561 if smt_check_sat() != "sat":
1562 print("%s No solution found!" % smt
.timestamp())
1563 retstatus
= "FAILED"
1568 write_trace(0, last_check_step
+1, "%d" % step
)
1572 if gentrace
and retstatus
:
1574 write_trace(0, num_steps
, '%')
1580 print_msg("Status: %s" % retstatus
)
1581 sys
.exit(0 if retstatus
== "PASSED" else 1)