3 # yosys -- Yosys Open SYnthesis Suite
5 # Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
7 # Permission to use, copy, modify, and/or distribute this software for any
8 # purpose with or without fee is hereby granted, provided that the above
9 # copyright notice and this permission notice appear in all copies.
11 # THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
12 # WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
13 # MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
14 # ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
15 # WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
16 # ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
17 # OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
20 import os
, sys
, getopt
, re
22 from smtio
import SmtIo
, SmtOpts
, MkVcd
23 from collections
import defaultdict
56 yosys-smtbmc [options] <yosys_smt2_output>
59 -t <skip_steps>:<num_steps>
60 -t <skip_steps>:<step_size>:<num_steps>
61 default: skip_steps=0, step_size=1, num_steps=20
64 generate an arbitrary trace that satisfies
65 all assertions and assumptions.
68 instead of BMC run temporal induction
71 instead of regular BMC run cover analysis
74 name of the top module
76 --smtc <constr_filename>
80 read cex file as written by ABC's "write_cex -n"
83 read AIGER map file (as written by Yosys' "write_aiger -map")
84 and AIGER witness file. The file names are <prefix>.aim for
85 the map file and <prefix>.aiw for the witness file.
87 --aig <aim_filename>:<aiw_filename>
88 like above, but for map files and witness files that do not
89 share a filename prefix (or use differen file extensions).
92 the AIGER witness file does not include the status and
96 only run the core proof, do not collect and print any
97 additional information (e.g. which assert failed)
100 check if the design with assumptions but without assertions
101 is SAT before checking if assertions are UNSAT. This will
102 detect if there are contradicting assumtions. In some cases
103 this will also help to "warmup" the solver, potentially
107 only check final constraints, assume base case
109 --assume-skipped <start_step>
110 assume asserts in skipped steps in BMC.
111 no assumptions are created for skipped steps
114 --dump-vcd <vcd_filename>
115 write trace to this VCD file
116 (hint: use 'write_smt2 -wires' for maximum
117 coverage of signals in generated VCD file)
119 --dump-vlogtb <verilog_filename>
120 write trace as Verilog test bench
122 --vlogtb-top <hierarchical_name>
123 use the given entity as top module for the generated
124 Verilog test bench. The <hierarchical_name> is relative
125 to the design top module without the top module name.
127 --dump-smtc <constr_filename>
128 write trace as constraints file
131 write just the last state as initial constraint to smtc file
133 --smtc-top <old>[:<new>]
134 replace <old> with <new> in constraints dumped to smtc
135 file and only dump object below <old> in design hierarchy.
138 do not assume initial conditions in state 0
141 when using -g or -i, create a dump file for each
142 step. The character '%' is replaces in all dump
143 filenames with the step number.
146 add <num_steps> time steps at the end of the trace
147 when creating a counter example (this additional time
148 steps will still be constrained by assumtions)
154 opts
, args
= getopt
.getopt(sys
.argv
[1:], so
.shortopts
+ "t:igcm:", so
.longopts
+
155 ["final-only", "assume-skipped=", "smtc=", "cex=", "aig=", "aig-noheader", "presat",
156 "dump-vcd=", "dump-vlogtb=", "vlogtb-top=", "dump-smtc=", "dump-all", "noinfo", "append=",
157 "smtc-init", "smtc-top=", "noinit"])
166 num_steps
= int(a
[0])
168 skip_steps
= int(a
[0])
169 num_steps
= int(a
[1])
171 skip_steps
= int(a
[0])
172 step_size
= int(a
[1])
173 num_steps
= int(a
[2])
176 elif o
== "--assume-skipped":
177 assume_skipped
= int(a
)
178 elif o
== "--final-only":
186 aimfile
, aiwfile
= a
.split(":")
190 elif o
== "--aig-noheader":
192 elif o
== "--dump-vcd":
194 elif o
== "--dump-vlogtb":
196 elif o
== "--vlogtb-top":
198 elif o
== "--dump-smtc":
200 elif o
== "--smtc-init":
202 elif o
== "--smtc-top":
203 smtctop
= a
.split(":")
204 if len(smtctop
) == 1:
206 assert len(smtctop
) == 2
207 smtctop
= tuple(smtctop
)
208 elif o
== "--dump-all":
210 elif o
== "--presat":
212 elif o
== "--noinfo":
214 elif o
== "--noinit":
216 elif o
== "--append":
217 append_steps
= int(a
)
226 elif so
.handle(o
, a
):
234 if sum([tempind
, gentrace
, covermode
]) > 1:
237 constr_final_start
= None
238 constr_asserts
= defaultdict(list)
239 constr_assumes
= defaultdict(list)
240 constr_write
= list()
243 current_states
= None
246 with
open(fn
, "r") as f
:
250 if line
.startswith("#"):
253 tokens
= line
.split()
258 if tokens
[0] == "initial":
259 current_states
= set()
261 current_states
.add(0)
264 if tokens
[0] == "final":
267 current_states
= set(["final-%d" % i
for i
in range(0, num_steps
+1)])
268 constr_final_start
= 0
269 elif len(tokens
) == 2:
270 arg
= abs(int(tokens
[1]))
271 current_states
= set(["final-%d" % i
for i
in range(arg
, num_steps
+1)])
272 constr_final_start
= arg
if constr_final_start
is None else min(constr_final_start
, arg
)
277 if tokens
[0] == "state":
278 current_states
= set()
280 for token
in tokens
[1:]:
281 tok
= token
.split(":")
283 current_states
.add(int(token
))
290 for i
in range(lower
, upper
+1):
291 current_states
.add(i
)
296 if tokens
[0] == "always":
298 current_states
= set(range(0, num_steps
+1))
299 elif len(tokens
) == 2:
300 arg
= abs(int(tokens
[1]))
301 current_states
= set(range(arg
, num_steps
+1))
306 if tokens
[0] == "assert":
307 assert current_states
is not None
309 for state
in current_states
:
310 constr_asserts
[state
].append(("%s:%d" % (fn
, current_line
), " ".join(tokens
[1:])))
314 if tokens
[0] == "assume":
315 assert current_states
is not None
317 for state
in current_states
:
318 constr_assumes
[state
].append(("%s:%d" % (fn
, current_line
), " ".join(tokens
[1:])))
322 if tokens
[0] == "write":
323 constr_write
.append(" ".join(tokens
[1:]))
326 if tokens
[0] == "logic":
327 so
.logic
= " ".join(tokens
[1:])
333 def get_constr_expr(db
, state
, final
=False, getvalues
=False):
335 if ("final-%d" % state
) not in db
:
336 return ([], [], []) if getvalues
else "true"
339 return ([], [], []) if getvalues
else "true"
341 netref_regex
= re
.compile(r
'(^|[( ])\[(-?[0-9]+:|)([^\]]*|\S*)\](?=[ )]|$)')
343 def replace_netref(match
):
344 state_sel
= match
.group(2)
348 elif state_sel
[0] == "-":
349 st
= state
+ int(state_sel
[:-1])
351 st
= int(state_sel
[:-1])
353 expr
= smt
.net_expr(topmod
, "s%d" % st
, smt
.get_path(topmod
, match
.group(3)))
355 return match
.group(1) + expr
358 for loc
, expr
in db
[("final-%d" % state
) if final
else state
]:
359 actual_expr
= netref_regex
.sub(replace_netref
, expr
)
361 expr_list
.append((loc
, expr
, actual_expr
))
363 expr_list
.append(actual_expr
)
366 loc_list
, expr_list
, acual_expr_list
= zip(*expr_list
)
367 value_list
= smt
.get_list(acual_expr_list
)
368 return loc_list
, expr_list
, value_list
370 if len(expr_list
) == 0:
373 if len(expr_list
) == 1:
376 return "(and %s)" % " ".join(expr_list
)
381 if noinfo
and vcdfile
is None and vlogtbfile
is None and outconstr
is None:
382 smt
.produce_models
= False
385 print("%s %s" % (smt
.timestamp(), msg
))
388 print_msg("Solver: %s" % (so
.solver
))
390 with
open(args
[0], "r") as f
:
394 for line
in constr_write
:
400 assert topmod
is not None
401 assert topmod
in smt
.modinfo
403 if cexfile
is not None:
409 with
open(cexfile
, "r") as f
:
410 cex_regex
= re
.compile(r
'([^\[@=]+)(\[\d+\])?([^@=]*)(@\d+)=([01])')
411 for entry
in f
.read().split():
412 match
= cex_regex
.match(entry
)
415 name
, bit
, extra_name
, step
, val
= match
.group(1), match
.group(2), match
.group(3), match
.group(4), match
.group(5)
420 if name
not in smt
.modinfo
[topmod
].inputs
:
431 if smt
.modinfo
[topmod
].wsize
[name
] == 1:
433 smtexpr
= "(= [%s] %s)" % (name
, "true" if val
else "false")
435 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bit
, bit
, name
, val
)
437 # print("cex@%d: %s" % (step, smtexpr))
438 constr_assumes
[step
].append((cexfile
, smtexpr
))
441 skip_steps
= max(skip_steps
, step
)
442 num_steps
= max(num_steps
, step
+1)
444 if aimfile
is not None:
454 with
open(aimfile
, "r") as f
:
455 for entry
in f
.read().splitlines():
456 entry
= entry
.split()
458 if entry
[0] == "input":
459 input_map
[int(entry
[1])] = (entry
[3], int(entry
[2]))
462 if entry
[0] == "init":
463 init_map
[int(entry
[1])] = (entry
[3], int(entry
[2]))
466 if entry
[0] in ["latch", "invlatch"]:
467 latch_map
[int(entry
[1])] = (entry
[3], int(entry
[2]), entry
[0] == "invlatch")
470 if entry
[0] in ["output", "wire"]:
475 with
open(aiwfile
, "r") as f
:
483 for entry
in f
.read().splitlines():
484 if len(entry
) == 0 or entry
[0] in "bcjfu.":
494 if len(init_map
) == 0:
495 for i
in range(len(entry
)):
500 value
= int(entry
[i
])
501 name
= latch_map
[i
][0]
502 bitidx
= latch_map
[i
][1]
503 invert
= latch_map
[i
][2]
508 path
= smt
.get_path(topmod
, name
)
509 width
= smt
.net_width(topmod
, path
)
513 smtexpr
= "(= [%s] %s)" % (name
, "true" if value
else "false")
515 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx
, bitidx
, name
, value
)
517 constr_assumes
[0].append((cexfile
, smtexpr
))
520 for i
in range(len(entry
)):
524 if (step
== 0) and (i
in init_map
):
525 value
= int(entry
[i
])
526 name
= init_map
[i
][0]
527 bitidx
= init_map
[i
][1]
529 path
= smt
.get_path(topmod
, name
)
531 if not smt
.net_exists(topmod
, path
):
532 match
= re
.match(r
"(.*)\[(\d+)\]$", path
[-1])
534 path
[-1] = match
.group(1)
535 addr
= int(match
.group(2))
537 if not match
or not smt
.mem_exists(topmod
, path
):
538 print_msg("Ignoring init value for unknown net: %s" % (name
))
541 meminfo
= smt
.mem_info(topmod
, path
)
542 smtexpr
= "(select [%s] #b%s)" % (".".join(path
), bin(addr
)[2:].zfill(meminfo
[0]))
546 smtexpr
= "[%s]" % name
547 width
= smt
.net_width(topmod
, path
)
551 smtexpr
= "(= %s %s)" % (smtexpr
, "true" if value
else "false")
553 smtexpr
= "(= ((_ extract %d %d) %s) #b%d)" % (bitidx
, bitidx
, smtexpr
, value
)
555 constr_assumes
[0].append((cexfile
, smtexpr
))
558 value
= int(entry
[i
])
559 name
= input_map
[i
][0]
560 bitidx
= input_map
[i
][1]
562 path
= smt
.get_path(topmod
, name
)
563 width
= smt
.net_width(topmod
, path
)
567 smtexpr
= "(= [%s] %s)" % (name
, "true" if value
else "false")
569 smtexpr
= "(= ((_ extract %d %d) [%s]) #b%d)" % (bitidx
, bitidx
, name
, value
)
571 constr_assumes
[step
].append((cexfile
, smtexpr
))
574 skip_steps
= max(skip_steps
, step
)
575 num_steps
= max(num_steps
, step
+1)
578 def write_vcd_trace(steps_start
, steps_stop
, index
):
579 filename
= vcdfile
.replace("%", index
)
580 print_msg("Writing trace to VCD file: %s" % (filename
))
582 with
open(filename
, "w") as vcd_file
:
583 vcd
= MkVcd(vcd_file
)
586 for netpath
in sorted(smt
.hiernets(topmod
)):
589 if n
.startswith("$"):
592 edge
= smt
.net_clock(topmod
, netpath
)
594 vcd
.add_net([topmod
] + netpath
, smt
.net_width(topmod
, netpath
))
596 vcd
.add_clock([topmod
] + netpath
, edge
)
597 path_list
.append(netpath
)
599 mem_trace_data
= dict()
600 for mempath
in sorted(smt
.hiermems(topmod
)):
601 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(topmod
, mempath
)
605 for i
in range(steps_start
, steps_stop
):
606 for j
in range(rports
):
607 expr_id
.append(('R', i
-steps_start
, j
, 'A'))
608 expr_id
.append(('R', i
-steps_start
, j
, 'D'))
609 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "R%dA" % j
))
610 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "R%dD" % j
))
611 for j
in range(wports
):
612 expr_id
.append(('W', i
-steps_start
, j
, 'A'))
613 expr_id
.append(('W', i
-steps_start
, j
, 'D'))
614 expr_id
.append(('W', i
-steps_start
, j
, 'M'))
615 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dA" % j
))
616 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dD" % j
))
617 expr_list
.append(smt
.mem_expr(topmod
, "s%d" % i
, mempath
, "W%dM" % j
))
623 for eid
, edat
in zip(expr_id
, smt
.get_list(expr_list
)):
641 c
[f
] = smt
.bv2bin(edat
)
651 if len(wdata
) == 0 and len(rdata
) != 0:
652 wdata
= [[]] * len(rdata
)
654 assert len(rdata
) == len(wdata
)
656 for i
in range(len(wdata
)):
658 for j_data
in rdata
[i
]:
659 if j_data
["A"] == addr
:
660 data
= list(j_data
["D"])
666 for i
in reversed(range(len(tdata
))):
667 for k
in range(width
):
668 if tdata
[i
][k
] == "x":
674 tdata
.append(data
[:])
676 for j_data
in wdata
[i
]:
677 if j_data
["A"] != addr
:
683 for k
in range(width
):
688 tdata
.append(data
[:])
690 assert len(tdata
) == len(rdata
)
693 netpath
[-1] += "<%0*x>" % ((len(addr
)+3) // 4, int(addr
, 2))
694 vcd
.add_net([topmod
] + netpath
, width
)
696 for i
in range(steps_start
, steps_stop
):
697 if i
not in mem_trace_data
:
698 mem_trace_data
[i
] = list()
699 mem_trace_data
[i
].append((netpath
, "".join(tdata
[i
-steps_start
])))
701 for i
in range(steps_start
, steps_stop
):
703 value_list
= smt
.get_net_bin_list(topmod
, path_list
, "s%d" % i
)
704 for path
, value
in zip(path_list
, value_list
):
705 vcd
.set_net([topmod
] + path
, value
)
706 if i
in mem_trace_data
:
707 for path
, value
in mem_trace_data
[i
]:
708 vcd
.set_net([topmod
] + path
, value
)
710 vcd
.set_time(steps_stop
)
713 def write_vlogtb_trace(steps_start
, steps_stop
, index
):
714 filename
= vlogtbfile
.replace("%", index
)
715 print_msg("Writing trace to Verilog testbench: %s" % (filename
))
717 vlogtb_topmod
= topmod
718 vlogtb_state
= "s@@step_idx@@"
720 if vlogtbtop
is not None:
721 for item
in vlogtbtop
.split("."):
722 if item
in smt
.modinfo
[vlogtb_topmod
].cells
:
723 vlogtb_state
= "(|%s_h %s| %s)" % (vlogtb_topmod
, item
, vlogtb_state
)
724 vlogtb_topmod
= smt
.modinfo
[vlogtb_topmod
].cells
[item
]
726 print_msg("Vlog top module '%s' not found: no cell '%s' in module '%s'" % (vlogtbtop
, item
, vlogtb_topmod
))
729 with
open(filename
, "w") as f
:
730 print("`ifndef VERILATOR", file=f
)
731 print("module testbench;", file=f
)
732 print(" reg [4095:0] vcdfile;", file=f
)
733 print(" reg clock;", file=f
)
734 print("`else", file=f
)
735 print("module testbench(input clock, output reg genclock);", file=f
)
736 print(" initial genclock = 1;", file=f
)
737 print("`endif", file=f
)
739 print(" reg genclock = 1;", file=f
)
740 print(" reg [31:0] cycle = 0;", file=f
)
742 primary_inputs
= list()
745 for name
in smt
.modinfo
[vlogtb_topmod
].inputs
:
746 if name
in ["clk", "clock", "CLK", "CLOCK"]:
747 clock_inputs
.add(name
)
748 width
= smt
.modinfo
[vlogtb_topmod
].wsize
[name
]
749 primary_inputs
.append((name
, width
))
751 for name
, width
in primary_inputs
:
752 if name
in clock_inputs
:
753 print(" wire [%d:0] PI_%s = clock;" % (width
-1, name
), file=f
)
755 print(" reg [%d:0] PI_%s;" % (width
-1, name
), file=f
)
757 print(" %s UUT (" % vlogtb_topmod
, file=f
)
758 print(",\n".join(" .{name}(PI_{name})".format(name
=name
) for name
, _
in primary_inputs
), file=f
)
761 print("`ifndef VERILATOR", file=f
)
762 print(" initial begin", file=f
)
763 print(" if ($value$plusargs(\"vcd=%s\", vcdfile)) begin", file=f
)
764 print(" $dumpfile(vcdfile);", file=f
)
765 print(" $dumpvars(0, testbench);", file=f
)
766 print(" end", file=f
)
767 print(" #5 clock = 0;", file=f
)
768 print(" while (genclock) begin", file=f
)
769 print(" #5 clock = 0;", file=f
)
770 print(" #5 clock = 1;", file=f
)
771 print(" end", file=f
)
772 print(" end", file=f
)
773 print("`endif", file=f
)
775 print(" initial begin", file=f
)
777 regs
= sorted(smt
.hiernets(vlogtb_topmod
, regs_only
=True))
778 regvals
= smt
.get_net_bin_list(vlogtb_topmod
, regs
, vlogtb_state
.replace("@@step_idx@@", str(steps_start
)))
780 print("`ifndef VERILATOR", file=f
)
781 print(" #1;", file=f
)
782 print("`endif", file=f
)
783 for reg
, val
in zip(regs
, regvals
):
786 if n
.startswith("$"):
788 print(" %sUUT.%s = %d'b%s;" % ("// " if hidden_net
else "", ".".join(reg
), len(val
), val
), file=f
)
790 anyconsts
= sorted(smt
.hieranyconsts(vlogtb_topmod
))
791 for info
in anyconsts
:
792 if info
[3] is not None:
793 modstate
= smt
.net_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(steps_start
)), info
[0])
794 value
= smt
.bv2bin(smt
.get("(|%s| %s)" % (info
[1], modstate
)))
795 print(" UUT.%s = %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
797 mems
= sorted(smt
.hiermems(vlogtb_topmod
))
799 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(vlogtb_topmod
, mempath
)
801 addr_expr_list
= list()
802 data_expr_list
= list()
803 for i
in range(steps_start
, steps_stop
):
804 for j
in range(rports
):
805 addr_expr_list
.append(smt
.mem_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dA" % j
))
806 data_expr_list
.append(smt
.mem_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dD" % j
))
808 addr_list
= smt
.get_list(addr_expr_list
)
809 data_list
= smt
.get_list(data_expr_list
)
812 for addr
, data
in zip(addr_list
, data_list
):
813 addr
= smt
.bv2bin(addr
)
814 data
= smt
.bv2bin(data
)
815 if addr
not in addr_data
:
816 addr_data
[addr
] = data
818 for addr
, data
in addr_data
.items():
819 print(" UUT.%s[%d'b%s] = %d'b%s;" % (".".join(mempath
), len(addr
), addr
, len(data
), data
), file=f
)
822 anyseqs
= sorted(smt
.hieranyseqs(vlogtb_topmod
))
824 for i
in range(steps_start
, steps_stop
):
825 pi_names
= [[name
] for name
, _
in primary_inputs
if name
not in clock_inputs
]
826 pi_values
= smt
.get_net_bin_list(vlogtb_topmod
, pi_names
, vlogtb_state
.replace("@@step_idx@@", str(i
)))
828 print(" // state %d" % i
, file=f
)
831 print(" if (cycle == %d) begin" % (i
-1), file=f
)
833 for name
, val
in zip(pi_names
, pi_values
):
835 print(" PI_%s <= %d'b%s;" % (".".join(name
), len(val
), val
), file=f
)
837 print(" PI_%s = %d'b%s;" % (".".join(name
), len(val
), val
), file=f
)
840 if info
[3] is not None:
841 modstate
= smt
.net_expr(vlogtb_topmod
, vlogtb_state
.replace("@@step_idx@@", str(i
)), info
[0])
842 value
= smt
.bv2bin(smt
.get("(|%s| %s)" % (info
[1], modstate
)))
844 print(" UUT.%s <= %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
846 print(" UUT.%s = %d'b%s;" % (".".join(info
[0] + [info
[3]]), len(value
), value
), file=f
);
849 print(" end", file=f
)
853 print(" end", file=f
)
854 print(" always @(posedge clock) begin", file=f
)
856 print(" genclock <= cycle < %d;" % (steps_stop
-1), file=f
)
857 print(" cycle <= cycle + 1;", file=f
)
858 print(" end", file=f
)
860 print("endmodule", file=f
)
863 def write_constr_trace(steps_start
, steps_stop
, index
):
864 filename
= outconstr
.replace("%", index
)
865 print_msg("Writing trace to constraints file: %s" % (filename
))
867 constr_topmod
= topmod
868 constr_state
= "s@@step_idx@@"
871 if smtctop
is not None:
872 for item
in smtctop
[0].split("."):
873 assert item
in smt
.modinfo
[constr_topmod
].cells
874 constr_state
= "(|%s_h %s| %s)" % (constr_topmod
, item
, constr_state
)
875 constr_topmod
= smt
.modinfo
[constr_topmod
].cells
[item
]
877 constr_prefix
= smtctop
[1] + "."
880 steps_start
= steps_stop
- 1
882 with
open(filename
, "w") as f
:
883 primary_inputs
= list()
885 for name
in smt
.modinfo
[constr_topmod
].inputs
:
886 width
= smt
.modinfo
[constr_topmod
].wsize
[name
]
887 primary_inputs
.append((name
, width
))
889 if steps_start
== 0 or smtcinit
:
890 print("initial", file=f
)
892 print("state %d" % steps_start
, file=f
)
894 regnames
= sorted(smt
.hiernets(constr_topmod
, regs_only
=True))
895 regvals
= smt
.get_net_list(constr_topmod
, regnames
, constr_state
.replace("@@step_idx@@", str(steps_start
)))
897 for name
, val
in zip(regnames
, regvals
):
898 print("assume (= [%s%s] %s)" % (constr_prefix
, ".".join(name
), val
), file=f
)
900 mems
= sorted(smt
.hiermems(constr_topmod
))
902 abits
, width
, rports
, wports
, asyncwr
= smt
.mem_info(constr_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(constr_topmod
, constr_state
.replace("@@step_idx@@", str(i
)), mempath
, "R%dA" % j
))
909 data_expr_list
.append(smt
.mem_expr(constr_topmod
, constr_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 if addr
not in addr_data
:
917 addr_data
[addr
] = data
919 for addr
, data
in addr_data
.items():
920 print("assume (= (select [%s%s] %s) %s)" % (constr_prefix
, ".".join(mempath
), addr
, data
), file=f
)
922 for k
in range(steps_start
, steps_stop
):
925 print("state %d" % k
, file=f
)
927 pi_names
= [[name
] for name
, _
in sorted(primary_inputs
)]
928 pi_values
= smt
.get_net_list(constr_topmod
, pi_names
, constr_state
.replace("@@step_idx@@", str(k
)))
930 for name
, val
in zip(pi_names
, pi_values
):
931 print("assume (= [%s%s] %s)" % (constr_prefix
, ".".join(name
), val
), file=f
)
934 def write_trace(steps_start
, steps_stop
, index
):
935 if vcdfile
is not None:
936 write_vcd_trace(steps_start
, steps_stop
, index
)
938 if vlogtbfile
is not None:
939 write_vlogtb_trace(steps_start
, steps_stop
, index
)
941 if outconstr
is not None:
942 write_constr_trace(steps_start
, steps_stop
, index
)
945 def print_failed_asserts_worker(mod
, state
, path
, extrainfo
):
946 assert mod
in smt
.modinfo
947 found_failed_assert
= False
949 if smt
.get("(|%s_a| %s)" % (mod
, state
)) in ["true", "#b1"]:
952 for cellname
, celltype
in smt
.modinfo
[mod
].cells
.items():
953 if print_failed_asserts_worker(celltype
, "(|%s_h %s| %s)" % (mod
, cellname
, state
), path
+ "." + cellname
, extrainfo
):
954 found_failed_assert
= True
956 for assertfun
, assertinfo
in smt
.modinfo
[mod
].asserts
.items():
957 if smt
.get("(|%s| %s)" % (assertfun
, state
)) in ["false", "#b0"]:
958 print_msg("Assert failed in %s: %s%s" % (path
, assertinfo
, extrainfo
))
959 found_failed_assert
= True
961 return found_failed_assert
964 def print_failed_asserts(state
, final
=False, extrainfo
=""):
966 loc_list
, expr_list
, value_list
= get_constr_expr(constr_asserts
, state
, final
=final
, getvalues
=True)
967 found_failed_assert
= False
969 for loc
, expr
, value
in zip(loc_list
, expr_list
, value_list
):
970 if smt
.bv2int(value
) == 0:
971 print_msg("Assert %s failed: %s%s" % (loc
, expr
, extrainfo
))
972 found_failed_assert
= True
975 if print_failed_asserts_worker(topmod
, "s%d" % state
, topmod
, extrainfo
):
976 found_failed_assert
= True
978 return found_failed_assert
981 def print_anyconsts_worker(mod
, state
, path
):
982 assert mod
in smt
.modinfo
984 for cellname
, celltype
in smt
.modinfo
[mod
].cells
.items():
985 print_anyconsts_worker(celltype
, "(|%s_h %s| %s)" % (mod
, cellname
, state
), path
+ "." + cellname
)
987 for fun
, info
in smt
.modinfo
[mod
].anyconsts
.items():
989 print_msg("Value for anyconst in %s (%s): %d" % (path
, info
[0], smt
.bv2int(smt
.get("(|%s| %s)" % (fun
, state
)))))
991 print_msg("Value for anyconst %s.%s (%s): %d" % (path
, info
[1], info
[0], smt
.bv2int(smt
.get("(|%s| %s)" % (fun
, state
)))))
994 def print_anyconsts(state
):
996 print_anyconsts_worker(topmod
, "s%d" % state
, topmod
)
999 def get_cover_list(mod
, base
):
1000 assert mod
in smt
.modinfo
1005 for expr
, desc
in smt
.modinfo
[mod
].covers
.items():
1006 cover_expr
.append("(ite (|%s| %s) #b1 #b0)" % (expr
, base
))
1007 cover_desc
.append(desc
)
1009 for cell
, submod
in smt
.modinfo
[mod
].cells
.items():
1010 e
, d
= get_cover_list(submod
, "(|%s_h %s| %s)" % (mod
, cell
, base
))
1014 return cover_expr
, cover_desc
1017 asserts_antecedent_cache
= [list()]
1018 asserts_consequent_cache
= [list()]
1019 asserts_cache_dirty
= False
1021 def smt_state(step
):
1022 smt
.write("(declare-fun s%d () |%s_s|)" % (step
, topmod
))
1023 states
.append("s%d" % step
)
1025 def smt_assert(expr
):
1029 smt
.write("(assert %s)" % expr
)
1031 def smt_assert_antecedent(expr
):
1035 smt
.write("(assert %s)" % expr
)
1037 global asserts_cache_dirty
1038 asserts_cache_dirty
= True
1039 asserts_antecedent_cache
[-1].append(expr
)
1041 def smt_assert_consequent(expr
):
1045 smt
.write("(assert %s)" % expr
)
1047 global asserts_cache_dirty
1048 asserts_cache_dirty
= True
1049 asserts_consequent_cache
[-1].append(expr
)
1051 def smt_forall_assert():
1055 global asserts_cache_dirty
1056 asserts_cache_dirty
= False
1058 def make_assert_expr(asserts_cache
):
1060 for lst
in asserts_cache
:
1063 assert len(expr
) != 0
1068 expr
= "(and %s)" % (" ".join(expr
))
1071 antecedent_expr
= make_assert_expr(asserts_antecedent_cache
)
1072 consequent_expr
= make_assert_expr(asserts_consequent_cache
)
1074 states_db
= set(states
)
1075 used_states_db
= set()
1076 new_antecedent_expr
= list()
1077 new_consequent_expr
= list()
1078 assert_expr
= list()
1080 def make_new_expr(new_expr
, expr
):
1082 while cursor
< len(expr
):
1084 if expr
[cursor
] in '|"':
1085 while cursor
+l
+1 < len(expr
) and expr
[cursor
] != expr
[cursor
+l
]:
1088 elif expr
[cursor
] not in '() ':
1089 while cursor
+l
< len(expr
) and expr
[cursor
+l
] not in '|"() ':
1092 word
= expr
[cursor
:cursor
+l
]
1093 if word
in states_db
:
1094 used_states_db
.add(word
)
1097 new_expr
.append(word
)
1100 make_new_expr(new_antecedent_expr
, antecedent_expr
)
1101 make_new_expr(new_consequent_expr
, consequent_expr
)
1103 new_antecedent_expr
= ["".join(new_antecedent_expr
)]
1104 new_consequent_expr
= ["".join(new_consequent_expr
)]
1106 if states
[0] in used_states_db
:
1107 new_antecedent_expr
.append("(|%s_ex_state_eq| %s %s_)" % (topmod
, states
[0], states
[0]))
1109 if s
in used_states_db
:
1110 new_antecedent_expr
.append("(|%s_ex_input_eq| %s %s_)" % (topmod
, s
, s
))
1112 if len(new_antecedent_expr
) == 0:
1113 new_antecedent_expr
= "true"
1114 elif len(new_antecedent_expr
) == 1:
1115 new_antecedent_expr
= new_antecedent_expr
[0]
1117 new_antecedent_expr
= "(and %s)" % (" ".join(new_antecedent_expr
))
1119 if len(new_consequent_expr
) == 0:
1120 new_consequent_expr
= "true"
1121 elif len(new_consequent_expr
) == 1:
1122 new_consequent_expr
= new_consequent_expr
[0]
1124 new_consequent_expr
= "(and %s)" % (" ".join(new_consequent_expr
))
1126 assert_expr
.append("(assert (forall (")
1129 if s
in used_states_db
:
1130 assert_expr
.append("%s(%s_ |%s_s|)" % ("" if first_state
else " ", s
, topmod
))
1132 assert_expr
.append(") (=> %s %s)))" % (new_antecedent_expr
, new_consequent_expr
))
1134 smt
.write("".join(assert_expr
))
1137 global asserts_cache_dirty
1138 asserts_cache_dirty
= True
1139 asserts_antecedent_cache
.append(list())
1140 asserts_consequent_cache
.append(list())
1141 smt
.write("(push 1)")
1144 global asserts_cache_dirty
1145 asserts_cache_dirty
= True
1146 asserts_antecedent_cache
.pop()
1147 asserts_consequent_cache
.pop()
1148 smt
.write("(pop 1)")
1150 def smt_check_sat():
1151 if asserts_cache_dirty
:
1153 return smt
.check_sat()
1157 skip_counter
= step_size
1158 for step
in range(num_steps
, -1, -1):
1160 print_msg("Temporal induction not supported for exists-forall problems.")
1164 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1165 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1166 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1167 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1169 if step
== num_steps
:
1170 smt_assert("(not (and (|%s_a| s%d) %s))" % (topmod
, step
, get_constr_expr(constr_asserts
, step
)))
1173 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
, step
+1))
1174 smt_assert("(|%s_a| s%d)" % (topmod
, step
))
1175 smt_assert(get_constr_expr(constr_asserts
, step
))
1177 if step
> num_steps
-skip_steps
:
1178 print_msg("Skipping induction in step %d.." % (step
))
1182 if skip_counter
< step_size
:
1183 print_msg("Skipping induction in step %d.." % (step
))
1187 print_msg("Trying induction in step %d.." % (step
))
1189 if smt_check_sat() == "sat":
1191 print_msg("Temporal induction failed!")
1192 print_anyconsts(num_steps
)
1193 print_failed_asserts(num_steps
)
1194 write_trace(step
, num_steps
+1, '%')
1197 print_anyconsts(num_steps
)
1198 print_failed_asserts(num_steps
)
1199 write_trace(step
, num_steps
+1, "%d" % step
)
1202 print_msg("Temporal induction successful.")
1207 cover_expr
, cover_desc
= get_cover_list(topmod
, "state")
1208 cover_mask
= "1" * len(cover_desc
)
1210 if len(cover_expr
) > 1:
1211 cover_expr
= "(concat %s)" % " ".join(cover_expr
)
1212 elif len(cover_expr
) == 1:
1213 cover_expr
= cover_expr
[0]
1218 smt
.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod
, len(cover_desc
), cover_expr
))
1222 found_failed_assert
= False
1224 assert step_size
== 1
1226 while step
< num_steps
:
1228 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1229 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1230 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1234 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1236 smt_assert_antecedent("(|%s_i| s0)" % (topmod
))
1237 smt_assert_antecedent("(|%s_is| s0)" % (topmod
))
1240 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
-1, step
))
1241 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1243 while "1" in cover_mask
:
1244 print_msg("Checking cover reachability in step %d.." % (step
))
1246 smt_assert("(distinct (covers_%d s%d) #b%s)" % (coveridx
, step
, "0" * len(cover_desc
)))
1248 if smt_check_sat() == "unsat":
1252 if append_steps
> 0:
1253 for i
in range(step
+1, step
+1+append_steps
):
1254 print_msg("Appending additional step %d." % i
)
1256 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, i
))
1257 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, i
))
1258 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, i
))
1259 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, i
-1, i
))
1260 smt_assert_consequent(get_constr_expr(constr_assumes
, i
))
1261 print_msg("Re-solving with appended steps..")
1262 assert smt_check_sat() == "sat"
1264 reached_covers
= smt
.bv2bin(smt
.get("(covers_%d s%d)" % (coveridx
, step
)))
1265 assert len(reached_covers
) == len(cover_desc
)
1269 for i
in range(len(reached_covers
)):
1270 if reached_covers
[i
] == "0":
1271 new_cover_mask
.append(cover_mask
[i
])
1274 print_msg("Reached cover statement at %s in step %d." % (cover_desc
[i
], step
))
1275 new_cover_mask
.append("0")
1277 cover_mask
= "".join(new_cover_mask
)
1279 for i
in range(step
+1+append_steps
):
1280 if print_failed_asserts(i
, extrainfo
=" (step %d)" % i
):
1281 found_failed_assert
= True
1283 write_trace(0, step
+1+append_steps
, "%d" % coveridx
)
1285 if found_failed_assert
:
1290 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
))
1292 if found_failed_assert
:
1295 if "1" not in cover_mask
:
1301 if "1" in cover_mask
:
1302 for i
in range(len(cover_mask
)):
1303 if cover_mask
[i
] == "1":
1304 print_msg("Unreached cover statement at %s." % cover_desc
[i
])
1306 else: # not tempind, covermode
1309 while step
< num_steps
:
1311 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
))
1312 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
))
1313 smt_assert_consequent(get_constr_expr(constr_assumes
, step
))
1317 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1319 smt_assert_antecedent("(|%s_i| s0)" % (topmod
))
1320 smt_assert_antecedent("(|%s_is| s0)" % (topmod
))
1323 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
-1, step
))
1324 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
))
1326 if step
< skip_steps
:
1327 if assume_skipped
is not None and step
>= assume_skipped
:
1328 print_msg("Skipping step %d (and assuming pass).." % (step
))
1329 smt_assert("(|%s_a| s%d)" % (topmod
, step
))
1330 smt_assert(get_constr_expr(constr_asserts
, step
))
1332 print_msg("Skipping step %d.." % (step
))
1336 last_check_step
= step
1337 for i
in range(1, step_size
):
1338 if step
+i
< num_steps
:
1340 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, step
+i
))
1341 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, step
+i
))
1342 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, step
+i
))
1343 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, step
+i
-1, step
+i
))
1344 smt_assert_consequent(get_constr_expr(constr_assumes
, step
+i
))
1345 last_check_step
= step
+i
1349 if last_check_step
== step
:
1350 print_msg("Checking assumptions in step %d.." % (step
))
1352 print_msg("Checking assumptions in steps %d to %d.." % (step
, last_check_step
))
1354 if smt_check_sat() == "unsat":
1355 print("%s Warmup failed!" % smt
.timestamp())
1360 if last_check_step
== step
:
1361 print_msg("Checking assertions in step %d.." % (step
))
1363 print_msg("Checking assertions in steps %d to %d.." % (step
, last_check_step
))
1366 smt_assert("(not (and %s))" % " ".join(["(|%s_a| s%d)" % (topmod
, i
) for i
in range(step
, last_check_step
+1)] +
1367 [get_constr_expr(constr_asserts
, i
) for i
in range(step
, last_check_step
+1)]))
1369 if smt_check_sat() == "sat":
1370 print("%s BMC failed!" % smt
.timestamp())
1371 if append_steps
> 0:
1372 for i
in range(last_check_step
+1, last_check_step
+1+append_steps
):
1373 print_msg("Appending additional step %d." % i
)
1375 smt_assert_antecedent("(not (|%s_is| s%d))" % (topmod
, i
))
1376 smt_assert_consequent("(|%s_u| s%d)" % (topmod
, i
))
1377 smt_assert_antecedent("(|%s_h| s%d)" % (topmod
, i
))
1378 smt_assert_antecedent("(|%s_t| s%d s%d)" % (topmod
, i
-1, i
))
1379 smt_assert_consequent(get_constr_expr(constr_assumes
, i
))
1380 assert smt_check_sat() == "sat"
1381 print_anyconsts(step
)
1382 for i
in range(step
, last_check_step
+1):
1383 print_failed_asserts(i
)
1384 write_trace(0, last_check_step
+1+append_steps
, '%')
1390 if (constr_final_start
is not None) or (last_check_step
+1 != num_steps
):
1391 for i
in range(step
, last_check_step
+1):
1392 smt_assert("(|%s_a| s%d)" % (topmod
, i
))
1393 smt_assert(get_constr_expr(constr_asserts
, i
))
1395 if constr_final_start
is not None:
1396 for i
in range(step
, last_check_step
+1):
1397 if i
< constr_final_start
:
1400 print_msg("Checking final constraints in step %d.." % (i
))
1403 smt_assert_consequent(get_constr_expr(constr_assumes
, i
, final
=True))
1404 smt_assert("(not %s)" % get_constr_expr(constr_asserts
, i
, final
=True))
1406 if smt_check_sat() == "sat":
1407 print("%s BMC failed!" % smt
.timestamp())
1409 print_failed_asserts(i
, final
=True)
1410 write_trace(0, i
+1, '%')
1419 for i
in range(step
, last_check_step
+1):
1420 smt_assert("(|%s_a| s%d)" % (topmod
, i
))
1421 smt_assert(get_constr_expr(constr_asserts
, i
))
1423 print_msg("Solving for step %d.." % (last_check_step
))
1424 if smt_check_sat() != "sat":
1425 print("%s No solution found!" % smt
.timestamp())
1431 write_trace(0, last_check_step
+1, "%d" % step
)
1435 if gentrace
and retstatus
:
1437 write_trace(0, num_steps
, '%')
1443 print_msg("Status: %s" % ("PASSED" if retstatus
else "FAILED (!)"))
1444 sys
.exit(0 if retstatus
else 1)