aboutsummaryrefslogtreecommitdiffstats
path: root/backends
diff options
context:
space:
mode:
authorJannis Harder <me@jix.one>2022-06-07 17:37:04 +0200
committerJannis Harder <me@jix.one>2022-06-07 19:06:45 +0200
commitac22f1764d5a9f8dbe70f70b1acf6b7dc65c1ced (patch)
tree868aaa50b1f43b38daa915f141bdada025dfd5d2 /backends
parent5f9a97d2342f1d3956f07c88c619bc88b43c8a1f (diff)
downloadyosys-ac22f1764d5a9f8dbe70f70b1acf6b7dc65c1ced.tar.gz
yosys-ac22f1764d5a9f8dbe70f70b1acf6b7dc65c1ced.tar.bz2
yosys-ac22f1764d5a9f8dbe70f70b1acf6b7dc65c1ced.zip
smt2: emit smtlib2_comb_expr outputs after all inputs
Diffstat (limited to 'backends')
-rw-r--r--backends/smt2/smt2.cc14
1 files changed, 9 insertions, 5 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index aa865e7fa..7481e0510 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -927,6 +927,7 @@ struct Smt2Worker
}
std::string smtlib2_inputs;
+ std::vector<std::string> smtlib2_decls;
if (is_smtlib2_module) {
for (auto wire : module->wires()) {
if (!wire->port_input)
@@ -968,11 +969,12 @@ struct Smt2Worker
log_error("smtlib2_comb_expr is unsupported on multi-bit wires when -nobv is specified: wire %s.%s",
log_id(module), log_id(wire));
}
+ auto &out_decls = is_smtlib2_comb_expr ? smtlib2_decls : decls;
if (bvmode && GetSize(sig) > 1) {
std::string sig_bv = is_smtlib2_comb_expr ? smtlib2_comb_expr : 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",
+ out_decls.insert(out_decls.end(), comments.begin(), comments.end());
+ out_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), sig_bv.c_str()));
if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))",
@@ -983,16 +985,16 @@ struct Smt2Worker
sig_bool.push_back(is_smtlib2_comb_expr ? smtlib2_comb_expr : get_bool(sig[i]));
}
if (!comments.empty())
- decls.insert(decls.end(), comments.begin(), comments.end());
+ out_decls.insert(out_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",
+ out_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), 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",
+ out_decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
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))",
@@ -1003,6 +1005,8 @@ struct Smt2Worker
}
}
+ decls.insert(decls.end(), smtlib2_decls.begin(), smtlib2_decls.end());
+
if (verbose) log("=> export logic associated with the initial state\n");
vector<string> init_list;