diff options
| author | Clifford Wolf <clifford@clifford.at> | 2017-02-04 21:10:24 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2017-02-04 21:10:24 +0100 |
| commit | adbecfee66e296916074f32d2c812450a15f2ba5 (patch) | |
| tree | 4ff6b11859f5d662f27c2d78bb59573cc9f52a05 /backends | |
| parent | 0c0784b6bfa41274d6b9fcd64c4fb061489dd798 (diff) | |
| download | yosys-adbecfee66e296916074f32d2c812450a15f2ba5.tar.gz yosys-adbecfee66e296916074f32d2c812450a15f2ba5.tar.bz2 yosys-adbecfee66e296916074f32d2c812450a15f2ba5.zip | |
Improve yosys-smtbmc cover() support
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smtbmc.py | 24 |
1 files changed, 19 insertions, 5 deletions
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 |