mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-24 01:25:33 +00:00
Code Activity

Merge remote-tracking branch 'origin/master' into xaig_dff

Browse source
This commit is contained in:
Eddie Hung 2019-10-03 10:55:23 -07:00
commit 549d6ea467
20 changed files with 374 additions and 86 deletions
Download patch file Download diff file Expand all files Collapse all files

15
backends/btor/btor.cc
View file

@ -569,7 +569,7 @@ struct BtorWorker
int nid_init_val = -1;
if (!initval.is_fully_undef())
nid_init_val = get_sig_nid(initval);
nid_init_val = get_sig_nid(initval, -1, false, true);
int sid = get_bv_sid(GetSize(sig_q));
int nid = next_nid++;
@ -681,7 +681,7 @@ struct BtorWorker
{
if (verbose)
btorf("; initval = %s\n", log_signal(firstword));
nid_init_val = get_sig_nid(firstword);
nid_init_val = get_sig_nid(firstword, -1, false, true);
}
else
{
@ -693,8 +693,8 @@ struct BtorWorker
if (thisword.is_fully_undef())
continue;
Const thisaddr(i, abits);
int nid_thisword = get_sig_nid(thisword);
int nid_thisaddr = get_sig_nid(thisaddr);
int nid_thisword = get_sig_nid(thisword, -1, false, true);
int nid_thisaddr = get_sig_nid(thisaddr, -1, false, true);
int last_nid_init_val = nid_init_val;
nid_init_val = next_nid++;
if (verbose)
@ -792,7 +792,7 @@ struct BtorWorker
cell_recursion_guard.erase(cell);
}
int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false)
int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false, bool is_init = false)
{
int nid = -1;
sigmap.apply(sig);
@ -823,7 +823,10 @@ struct BtorWorker
int sid = get_bv_sid(GetSize(sig));
int nid_input = next_nid++;
btorf("%d input %d\n", nid_input, sid);
if (is_init)
btorf("%d state %d\n", nid_input, sid);
else
btorf("%d input %d\n", nid_input, sid);
int nid_masked_input;
if (sig_mask_undef.is_fully_ones()) {

28
backends/smt2/smtbmc.py
View file

@ -1256,7 +1256,7 @@ def smt_check_sat():
return smt.check_sat()
if tempind:
retstatus = False
retstatus = "FAILED"
skip_counter = step_size
for step in range(num_steps, -1, -1):
if smt.forall:
@ -1303,7 +1303,7 @@ if tempind:
else:
print_msg("Temporal induction successful.")
retstatus = True
retstatus = "PASSED"
break
elif covermode:
@ -1321,7 +1321,7 @@ elif covermode:
smt.write("(define-fun covers_0 ((state |%s_s|)) (_ BitVec %d) %s)" % (topmod, len(cover_desc), cover_expr))
step = 0
retstatus = False
retstatus = "FAILED"
found_failed_assert = False
assert step_size == 1
@ -1365,7 +1365,7 @@ elif covermode:
if smt_check_sat() == "unsat":
print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
found_failed_assert = True
retstatus = False
retstatus = "FAILED"
break
reached_covers = smt.bv2bin(smt.get("(covers_%d s%d)" % (coveridx, step)))
@ -1400,7 +1400,7 @@ elif covermode:
break
if "1" not in cover_mask:
retstatus = True
retstatus = "PASSED"
break
step += 1
@ -1412,7 +1412,7 @@ elif covermode:
else: # not tempind, covermode
step = 0
retstatus = True
retstatus = "PASSED"
while step < num_steps:
smt_state(step)
smt_assert_consequent("(|%s_u| s%d)" % (topmod, step))
@ -1459,8 +1459,8 @@ else: # not tempind, covermode
print_msg("Checking assumptions in steps %d to %d.." % (step, last_check_step))
if smt_check_sat() == "unsat":
print("%s Warmup failed!" % smt.timestamp())
retstatus = False
print("%s Assumptions are unsatisfiable!" % smt.timestamp())
retstatus = "PREUNSAT"
break
if not final_only:
@ -1487,13 +1487,13 @@ else: # not tempind, covermode
print_msg("Re-solving with appended steps..")
if smt_check_sat() == "unsat":
print("%s Cannot appended steps without violating assumptions!" % smt.timestamp())
retstatus = False
retstatus = "FAILED"
break
print_anyconsts(step)
for i in range(step, last_check_step+1):
print_failed_asserts(i)
write_trace(0, last_check_step+1+append_steps, '%')
retstatus = False
retstatus = "FAILED"
break
smt_pop()
@ -1519,7 +1519,7 @@ else: # not tempind, covermode
print_anyconsts(i)
print_failed_asserts(i, final=True)
write_trace(0, i+1, '%')
retstatus = False
retstatus = "FAILED"
break
smt_pop()
@ -1534,7 +1534,7 @@ else: # not tempind, covermode
print_msg("Solving for step %d.." % (last_check_step))
if smt_check_sat() != "sat":
print("%s No solution found!" % smt.timestamp())
retstatus = False
retstatus = "FAILED"
break
elif dumpall:
@ -1551,5 +1551,5 @@ else: # not tempind, covermode
smt.write("(exit)")
smt.wait()
print_msg("Status: %s" % ("PASSED" if retstatus else "FAILED (!)"))
sys.exit(0 if retstatus else 1)
print_msg("Status: %s" % retstatus)
sys.exit(0 if retstatus == "PASSED" else 1)