riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

Added $anyconst support to smt2 back-end

This commit is contained in:
Clifford Wolf 2016-08-30 11:26:10 +02:00
parent 4ea7054b56
commit 39e4faa2e4
1 changed files with 17 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
backends/smt2/smt2.cc
View File

@ -403,6 +403,16 @@ struct Smt2Worker
return; 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 == "$and") return export_bvop(cell, "(bvand A B)");
if (cell->type == "$or") return export_bvop(cell, "(bvor A B)"); if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
if (cell->type == "$xor") return export_bvop(cell, "(bvxor 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")))); 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") if (cell->type == "$mem")
{ {
int arrayid = memarrays.at(cell); int arrayid = memarrays.at(cell);