diff options
| author | Clifford Wolf <clifford@clifford.at> | 2016-08-30 11:26:10 +0200 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2016-08-30 11:26:10 +0200 |
| commit | 39e4faa2e4c51c9588df233c795b4e85523879cf (patch) | |
| tree | 8b1f5c13e8ad0a2e7821785dc6b03aa2a7bdc3e7 /backends/smt2 | |
| parent | 4ea7054b56c568e15ffe9ee3560fd458fabcdf00 (diff) | |
| download | yosys-39e4faa2e4c51c9588df233c795b4e85523879cf.tar.gz yosys-39e4faa2e4c51c9588df233c795b4e85523879cf.tar.bz2 yosys-39e4faa2e4c51c9588df233c795b4e85523879cf.zip | |
Added $anyconst support to smt2 back-end
Diffstat (limited to 'backends/smt2')
| -rw-r--r-- | backends/smt2/smt2.cc | 17 |
1 files changed, 17 insertions, 0 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index af048859c..43601cd24 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -403,6 +403,16 @@ struct Smt2Worker return; } + if (cell->type == "$anyconst") + { + registers.insert(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++); + recursive_cells.erase(cell); + return; + } + if (cell->type == "$and") return export_bvop(cell, "(bvand A B)"); if (cell->type == "$or") return export_bvop(cell, "(bvor A B)"); if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)"); @@ -677,6 +687,13 @@ struct Smt2Worker trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q")))); } + if (cell->type == "$anyconst") + { + std::string expr_d = get_bv(cell->getPort("\\Y")); + std::string expr_q = get_bv(cell->getPort("\\Y"), "next_state"); + trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Y")))); + } + if (cell->type == "$mem") { int arrayid = memarrays.at(cell); |