diff options
| author | Noah Moroze <noahmoroze@gmail.com> | 2020-08-20 16:00:05 -0400 |
|---|---|---|
| committer | Noah Moroze <noahmoroze@gmail.com> | 2020-08-20 16:00:05 -0400 |
| commit | 91682d189e55923114726b797968ef939777000c (patch) | |
| tree | 9426d0ecd58fa34c58c536fb43e335889d243fe7 /backends | |
| parent | 87b9ee330d5fa6f7ddcbe1bcc3a582c40541330c (diff) | |
| download | yosys-91682d189e55923114726b797968ef939777000c.tar.gz yosys-91682d189e55923114726b797968ef939777000c.tar.bz2 yosys-91682d189e55923114726b797968ef939777000c.zip | |
Ensure smt2 comments are associated with accessors
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smt2.cc | 29 |
1 files changed, 20 insertions, 9 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index a79c0bd99..0423b977a 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))); } + } } } } |