From 6abf79eb280a645f5896f307dca7afb92d75d25e Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 4 Feb 2017 17:02:13 +0100 Subject: Further improve cover() support --- backends/smt2/smt2.cc | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'backends') 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 assert_list, assume_list; + vector 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++) -- cgit v1.2.3