diff options
| author | Jim Lawson <ucbjrl@berkeley.edu> | 2019-04-01 11:09:12 -0700 |
|---|---|---|
| committer | Jim Lawson <ucbjrl@berkeley.edu> | 2019-04-01 11:09:12 -0700 |
| commit | b8dfda876795dbf08bec49ab06ac8603025d2114 (patch) | |
| tree | 35cd5485c70c17e93426d54a104018bae90ed924 /backends/smt2/smt2.cc | |
| parent | 6d2ea6fe5563205c0f565810d615c4900d4508d8 (diff) | |
| parent | 22035c20ff071ec5c30990258850ecf97de5d5b3 (diff) | |
| download | yosys-b8dfda876795dbf08bec49ab06ac8603025d2114.tar.gz yosys-b8dfda876795dbf08bec49ab06ac8603025d2114.tar.bz2 yosys-b8dfda876795dbf08bec49ab06ac8603025d2114.zip | |
Merge remote-tracking branch 'upstream/master'
Diffstat (limited to 'backends/smt2/smt2.cc')
| -rw-r--r-- | backends/smt2/smt2.cc | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 7f3cc94ca..688535f33 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -416,6 +416,7 @@ struct Smt2Worker for (char ch : expr) { if (ch == 'A') processed_expr += get_bv(sig_a); else if (ch == 'B') processed_expr += get_bv(sig_b); + else if (ch == 'P') processed_expr += get_bv(cell->getPort("\\B")); else if (ch == 'L') processed_expr += is_signed ? "a" : "l"; else if (ch == 'U') processed_expr += is_signed ? "s" : "u"; else processed_expr += ch; @@ -554,7 +555,7 @@ struct Smt2Worker if (cell->type.in("$shift", "$shiftx")) { if (cell->getParam("\\B_SIGNED").as_bool()) { - return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) " + return export_bvop(cell, stringf("(ite (bvsge P #b%0*d) " "(bvlshr A B) (bvlshr A (bvneg B)))", GetSize(cell->getPort("\\B")), 0), 's'); } else { @@ -887,8 +888,8 @@ 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 %d %s\n", cell->type.c_str() + 1, id, - cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell))); + string infostr = (cell->name[0] == '$' && cell->attributes.count("\\src")) ? cell->attributes.at("\\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->type == "$cover") decls.push_back(stringf("(define-fun |%s_%c %d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n", |