diff options
| author | Clifford Wolf <clifford@clifford.at> | 2017-02-04 17:02:13 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2017-02-04 17:02:13 +0100 |
| commit | 6abf79eb280a645f5896f307dca7afb92d75d25e (patch) | |
| tree | 7a8d3f775f4a8c47eaf0b3e1a50561ca72b3631c /backends | |
| parent | 3928482a3c4fb71b8e6ccdcb362c030eef34a479 (diff) | |
| download | yosys-6abf79eb280a645f5896f307dca7afb92d75d25e.tar.gz yosys-6abf79eb280a645f5896f307dca7afb92d75d25e.tar.bz2 yosys-6abf79eb280a645f5896f307dca7afb92d75d25e.zip | |
Further improve cover() support
Diffstat (limited to 'backends')
| -rw-r--r-- | backends/smt2/smt2.cc | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index e0daae728..02661f1cf 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -662,9 +662,9 @@ 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, @@ -673,8 +673,10 @@ struct Smt2Worker 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++) |