diff options
| author | Clifford Wolf <clifford@clifford.at> | 2018-11-01 11:40:58 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2018-11-01 11:40:58 +0100 |
| commit | b6781c6f4ba20ba14d1649a993fc09691921de2b (patch) | |
| tree | cc35a9173c9674ce420343d990f9cbec25359ac1 | |
| parent | b4d82aa2450e042f884c5921407605dab5cfc190 (diff) | |
| download | yosys-b6781c6f4ba20ba14d1649a993fc09691921de2b.tar.gz yosys-b6781c6f4ba20ba14d1649a993fc09691921de2b.tar.bz2 yosys-b6781c6f4ba20ba14d1649a993fc09691921de2b.zip | |
Add support for signed $shift/$shiftx in smt2 back-end
Signed-off-by: Clifford Wolf <clifford@clifford.at>
| -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 e2777ae04..418f8d766 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -554,7 +554,9 @@ struct Smt2Worker if (cell->type.in("$shift", "$shiftx")) { if (cell->getParam("\\B_SIGNED").as_bool()) { - /* FIXME */ + return export_bvop(cell, stringf("(ite (bvsge B #b%0*d) " + "(bvlshr A B) (bvlshr A (bvneg B)))", + GetSize(cell->getPort("\\B")), 0), 's'); } else { return export_bvop(cell, "(bvlshr A B)", 's'); } |