diff options
| author | Clifford Wolf <clifford@clifford.at> | 2016-08-30 19:27:42 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2016-08-30 19:27:42 +0200 |
| commit | aa25a4cec66bfde84f9142b21679e82ba90ee910 (patch) | |
| tree | d409ee17068e6e41c2049b1b3339d2f49972b9f5 /backends/smt2/smt2.cc | |
| parent | 6f41e5277d1d41db7a620c73cf1b65558b55f236 (diff) | |
| download | yosys-aa25a4cec66bfde84f9142b21679e82ba90ee910.tar.gz yosys-aa25a4cec66bfde84f9142b21679e82ba90ee910.tar.bz2 yosys-aa25a4cec66bfde84f9142b21679e82ba90ee910.zip | |
Added $anyconst support to yosys-smtbmc
Diffstat (limited to 'backends/smt2/smt2.cc')
| -rw-r--r-- | backends/smt2/smt2.cc | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 9668a6425..30a6bb19c 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -420,6 +420,8 @@ struct Smt2Worker if (cell->type == "$anyconst") { registers.insert(cell); + 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("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n", get_id(module), idcounter, get_id(module), GetSize(cell->getPort("\\Y")), log_signal(cell->getPort("\\Y")))); register_bv(cell->getPort("\\Y"), idcounter++); @@ -669,7 +671,7 @@ struct Smt2Worker 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))); + 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 == "$assert") |