diff options
Diffstat (limited to 'backends/smt2/smt2.cc')
| -rw-r--r-- | backends/smt2/smt2.cc | 40 |
1 files changed, 35 insertions, 5 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index f44827942..ed6f3aff9 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -649,6 +649,27 @@ struct Smt2Worker return export_bvop(cell, "(bvurem A B)", 'd'); } } + // "div" = flooring division + if (cell->type == ID($divfloor)) { + if (cell->getParam(ID::A_SIGNED).as_bool()) { + // bvsdiv is truncating division, so we can't use it here. + int width = max(GetSize(cell->getPort(ID::A)), GetSize(cell->getPort(ID::B))); + width = max(width, GetSize(cell->getPort(ID::Y))); + auto expr = stringf("(let (" + "(a_neg (bvslt A #b%0*d)) " + "(b_neg (bvslt B #b%0*d))) " + "(let ((abs_a (ite a_neg (bvneg A) A)) " + "(abs_b (ite b_neg (bvneg B) B))) " + "(let ((u (bvudiv abs_a abs_b)) " + "(adj (ite (= #b%0*d (bvurem abs_a abs_b)) #b%0*d #b%0*d))) " + "(ite (= a_neg b_neg) u " + "(bvneg (bvadd u adj))))))", + width, 0, width, 0, width, 0, width, 0, width, 1); + return export_bvop(cell, expr, 'd'); + } else { + return export_bvop(cell, "(bvudiv A B)", 'd'); + } + } if (cell->type.in(ID($reduce_and), ID($reduce_or), ID($reduce_bool)) && 2*GetSize(cell->getPort(ID::A).chunks()) < GetSize(cell->getPort(ID::A))) { @@ -860,7 +881,7 @@ struct Smt2Worker log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smt2`.\n", log_id(cell->type), log_id(module), log_id(cell)); } - if (cell->type.in(ID($adff), ID($adffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF") { + if (cell->type.in(ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF" || cell->type.str().substr(0, 7) == "$_ALDFF") { log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smt2`.\n", log_id(cell->type), log_id(module), log_id(cell)); } @@ -985,8 +1006,10 @@ struct Smt2Worker string name_a = get_bool(cell->getPort(ID::A)); string name_en = get_bool(cell->getPort(ID::EN)); - string infostr = (cell->name[0] == '$' && cell->attributes.count(ID::src)) ? cell->attributes.at(ID::src).decode_string() : get_id(cell); - decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, infostr.c_str())); + if (cell->name[0] == '$' && cell->attributes.count(ID::src)) + decls.push_back(stringf("; yosys-smt2-%s %d %s %s\n", cell->type.c_str() + 1, id, get_id(cell), cell->attributes.at(ID::src).decode_string().c_str())); + else + decls.push_back(stringf("; yosys-smt2-%s %d %s\n", cell->type.c_str() + 1, id, get_id(cell))); if (cell->type == ID($cover)) decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n", @@ -1183,10 +1206,12 @@ struct Smt2Worker data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))", data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str()); + string empty_mask(mem->width, '0'); + decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) " - "(store (|%s#%d#%d| state) %s %s)) ; %s\n", + "(ite (= %s #b%s) (|%s#%d#%d| state) (store (|%s#%d#%d| state) %s %s))) ; %s\n", get_id(module), arrayid, i+1, get_id(module), abits, mem->width, - get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid))); + mask.c_str(), empty_mask.c_str(), get_id(module), arrayid, i, get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid))); } } @@ -1531,6 +1556,11 @@ struct Smt2Backend : public Backend { log_header(design, "Executing SMT2 backend.\n"); + log_push(); + Pass::call(design, "bmuxmap"); + Pass::call(design, "demuxmap"); + log_pop(); + size_t argidx; for (argidx = 1; argidx < args.size(); argidx++) { |