From adbecfee66e296916074f32d2c812450a15f2ba5 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 4 Feb 2017 21:10:24 +0100 Subject: Improve yosys-smtbmc cover() support --- backends/smt2/smtbmc.py | 24 +++++++++++++++++++----- 1 file changed, 19 insertions(+), 5 deletions(-) (limited to 'backends') diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 880aa64fa..16ba543e7 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -821,6 +821,7 @@ if tempind: elif covermode: cover_expr, cover_desc = get_cover_list(topmod, "state") + cover_mask = "1" * len(cover_desc) if len(cover_expr) > 1: cover_expr = "(concat %s)" % " ".join(cover_expr) @@ -851,7 +852,7 @@ elif covermode: smt.write("(assert (|%s_t| s%d s%d))" % (topmod, step-1, step)) smt.write("(assert (not (|%s_is| s%d)))" % (topmod, step)) - while True: + while "1" in cover_mask: print_msg("Checking cover reachability in step %d.." % (step)) smt.write("(push 1)") smt.write("(assert (distinct (covers_%d s%d) #b%s))" % (coveridx, step, "0" * len(cover_desc))) @@ -861,24 +862,37 @@ elif covermode: break reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step))) + assert len(reached_covers) == len(cover_desc) + + new_cover_mask = [] for i in range(len(reached_covers)): if reached_covers[i] == "0": + new_cover_mask.append(cover_mask[i]) continue - print_msg(" reached cover statement %s." % cover_desc[i]) + print_msg("Reached cover statement at %s in step %d." % (cover_desc[i], step)) + new_cover_mask.append("0") write_trace(0, step+1, "%d" % coveridx) - # TBD - assert False + cover_mask = "".join(new_cover_mask) - if len(cover_desc) == 0: + coveridx += 1 + smt.write("(pop 1)") + 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)) + + if "1" not in cover_mask: retstatus = True break step += 1 + if "1" in cover_mask: + for i in range(len(cover_mask)): + if cover_mask[i] == "1": + print_msg("Unreached cover statement at %s." % cover_desc[i]) + else: # not tempind, covermode step = 0 retstatus = True -- cgit v1.2.3 t class='txt' type='search' size='10' name='q' value=''/>

path: root/keyboards/handwired/atreus50/keymaps/ajp10304/rules.mk

blob: fc5d9ba1aa55506ad1c1353aedd727b63027e027 (plain)