diff options
Diffstat (limited to 'backends/smt2/smt2.cc')
| -rw-r--r-- | backends/smt2/smt2.cc | 16 |
1 files changed, 11 insertions, 5 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index e0daae728..932f5cd68 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -662,19 +662,25 @@ struct Smt2Worker if (verbose) log("=> export logic driving asserts\n"); - vector<string> assert_list, assume_list; + vector<string> assert_list, assume_list, cover_list; for (auto cell : module->cells()) - if (cell->type.in("$assert", "$assume")) { + if (cell->type.in("$assert", "$assume", "$cover")) { string name_a = get_bool(cell->getPort("\\A")); string name_en = get_bool(cell->getPort("\\EN")); decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter, cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell))); - decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n", - get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell))); + if (cell->type == "$cover") + decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n", + get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell))); + else + decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n", + get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell))); if (cell->type == "$assert") assert_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++)); - else + else if (cell->type == "$assume") assume_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++)); + else if (cell->type == "$cover") + cover_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++)); } for (int iter = 1; !registers.empty(); iter++) |