riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Merge pull request #2349 from nmoroze/smt2-bugfix 

Ensure smt2 comments are associated with accessors
This commit is contained in:
clairexen 2020-08-22 12:28:39 +02:00 committed by GitHub
parent dc20d9e842 91682d189e
commit 0f81e27898
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
1 changed files with 20 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

29
backends/smt2/smt2.cc
View File

@ -824,34 +824,44 @@ struct Smt2Worker
is_register = true; is_register = true;
if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) { if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) {
RTLIL::SigSpec sig = sigmap(wire); RTLIL::SigSpec sig = sigmap(wire);
std::vector<std::string> comments;
if (wire->port_input) 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) 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) 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] == '\\')) 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))) 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" : "")); clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
if (bvmode && GetSize(sig) > 1) { 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", 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) if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", 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))); get_id(module), get_id(wire), get_id(module), get_id(wire)));
} else { } 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) { if (GetSize(sig) > 1) {
decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n", 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) if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))", 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)); get_id(module), get_id(wire), i, get_id(module), get_id(wire), i));
} else { } else {
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n", 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) if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))", 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))); get_id(module), get_id(wire), get_id(module), get_id(wire)));
@ -859,6 +869,7 @@ struct Smt2Worker
} }
} }
} }
}
if (verbose) log("=> export logic associated with the initial state\n"); if (verbose) log("=> export logic associated with the initial state\n");