diff options
| author | Clifford Wolf <clifford@clifford.at> | 2017-02-04 18:17:08 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2017-02-04 18:17:08 +0100 |
| commit | 0c0784b6bfa41274d6b9fcd64c4fb061489dd798 (patch) | |
| tree | 9f5e0ad12f61bb2aec25b4020eabc48963538adf /backends/smt2/smt2.cc | |
| parent | 6abf79eb280a645f5896f307dca7afb92d75d25e (diff) | |
| download | yosys-0c0784b6bfa41274d6b9fcd64c4fb061489dd798.tar.gz yosys-0c0784b6bfa41274d6b9fcd64c4fb061489dd798.tar.bz2 yosys-0c0784b6bfa41274d6b9fcd64c4fb061489dd798.zip | |
Partially implement cover() support in yosys-smtbmc
Diffstat (limited to 'backends/smt2/smt2.cc')
| -rw-r--r-- | backends/smt2/smt2.cc | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 02661f1cf..932f5cd68 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -669,8 +669,12 @@ struct Smt2Worker 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 if (cell->type == "$assume") |