diff options
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/aiger/xaiger.cc | 18 | ||||
| -rw-r--r-- | backends/smt2/smtbmc.py | 28 |
2 files changed, 23 insertions, 23 deletions
diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 4018cc9de..46890b071 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -203,7 +203,7 @@ struct XAigerWriter // box ordering, but not individual AIG cells dict<SigBit, pool<IdString>> bit_drivers, bit_users; TopoSort<IdString, RTLIL::sort_by_id_str> toposort; - bool abc_box_seen = false; + bool abc9_box_seen = false; for (auto cell : module->selected_cells()) { if (cell->type == "$_NOT_") @@ -242,8 +242,8 @@ struct XAigerWriter log_assert(!holes_mode); RTLIL::Module* inst_module = module->design->module(cell->type); - if (inst_module && inst_module->attributes.count("\\abc_box_id")) { - abc_box_seen = true; + if (inst_module && inst_module->attributes.count("\\abc9_box_id")) { + abc9_box_seen = true; if (!holes_mode) { toposort.node(cell->name); @@ -291,10 +291,10 @@ struct XAigerWriter if (is_output) { int arrival = 0; if (port_wire) { - auto it = port_wire->attributes.find("\\abc_arrival"); + auto it = port_wire->attributes.find("\\abc9_arrival"); if (it != port_wire->attributes.end()) { if (it->second.flags != 0) - log_error("Attribute 'abc_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(port_wire), log_id(cell->type)); + log_error("Attribute 'abc9_arrival' on port '%s' of module '%s' is not an integer.\n", log_id(port_wire), log_id(cell->type)); arrival = it->second.as_int(); } } @@ -318,7 +318,7 @@ struct XAigerWriter //log_warning("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell)); } - if (abc_box_seen) { + if (abc9_box_seen) { for (auto &it : bit_users) if (bit_drivers.count(it.first)) for (auto driver_cell : bit_drivers.at(it.first)) @@ -347,7 +347,7 @@ struct XAigerWriter log_assert(cell); RTLIL::Module* box_module = module->design->module(cell->type); - if (!box_module || !box_module->attributes.count("\\abc_box_id")) + if (!box_module || !box_module->attributes.count("\\abc9_box_id")) continue; bool blackbox = box_module->get_blackbox_attribute(true /* ignore_wb */); @@ -398,7 +398,7 @@ struct XAigerWriter else { Wire *wire = module->addWire(NEW_ID, GetSize(w)); if (blackbox) - wire->set_bool_attribute(ID(abc_padding)); + wire->set_bool_attribute(ID(abc9_padding)); rhs = wire; cell->setPort(port_name, rhs); } @@ -666,7 +666,7 @@ struct XAigerWriter write_h_buffer(box_inputs); write_h_buffer(box_outputs); - write_h_buffer(box_module->attributes.at("\\abc_box_id").as_int()); + write_h_buffer(box_module->attributes.at("\\abc9_box_id").as_int()); write_h_buffer(box_count++); } diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index 445a42e0d..3d6d3e1b3 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -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) |