diff options
Diffstat (limited to 'backends/smt2/smt2.cc')
| -rw-r--r-- | backends/smt2/smt2.cc | 31 |
1 files changed, 21 insertions, 10 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index a79c0bd99..4a53ce6d5 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -824,38 +824,49 @@ struct Smt2Worker is_register = true; if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) { RTLIL::SigSpec sig = sigmap(wire); + std::vector<std::string> comments; if (wire->port_input) - decls.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width)); + comments.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width)); if (wire->port_output) - decls.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width)); + comments.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width)); if (is_register) - decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width)); + comments.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width)); if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) - decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width)); + comments.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width)); if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig))) - decls.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire), + comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire), clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : "")); if (bvmode && GetSize(sig) > 1) { + std::string sig_bv = get_bv(sig); + if (!comments.empty()) + decls.insert(decls.end(), comments.begin(), comments.end()); decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n", - get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str())); + get_id(module), get_id(wire), get_id(module), GetSize(sig), sig_bv.c_str())); if (wire->port_input) ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", get_id(module), get_id(wire), get_id(module), get_id(wire))); } else { - for (int i = 0; i < GetSize(sig); i++) + std::vector<std::string> sig_bool; + for (int i = 0; i < GetSize(sig); i++) { + sig_bool.push_back(get_bool(sig[i])); + } + if (!comments.empty()) + decls.insert(decls.end(), comments.begin(), comments.end()); + for (int i = 0; i < GetSize(sig); i++) { if (GetSize(sig) > 1) { decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n", - get_id(module), get_id(wire), i, get_id(module), get_bool(sig[i]).c_str())); + get_id(module), get_id(wire), i, get_id(module), sig_bool[i].c_str())); if (wire->port_input) ex_input_eq.push_back(stringf(" (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))", get_id(module), get_id(wire), i, get_id(module), get_id(wire), i)); } else { decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n", - get_id(module), get_id(wire), get_id(module), get_bool(sig[i]).c_str())); + get_id(module), get_id(wire), get_id(module), sig_bool[i].c_str())); if (wire->port_input) ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", get_id(module), get_id(wire), get_id(module), get_id(wire))); } + } } } } @@ -1392,7 +1403,7 @@ struct Smt2Backend : public Backend { log(" the given option as a `(set-option ...)` command in the SMT-LIBv2.\n"); log("\n"); log("[1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David\n"); - log("R. Cok's tutorial: http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf\n"); + log("R. Cok's tutorial: https://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf\n"); log("\n"); log("---------------------------------------------------------------------------\n"); log("\n"); |