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

Merge pull request #748 from makaimann/add-btor-ops 

Add btor ops for $mul, $div, $mod and $concat
This commit is contained in:
Clifford Wolf 2018-12-18 19:59:29 +01:00 committed by GitHub
parent eddf075d93 abf5930a33
commit 2d73e1b60a
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 38 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

40
backends/btor/btor.cc
View File

@ -133,12 +133,13 @@ struct BtorWorker
cell_recursion_guard.insert(cell); cell_recursion_guard.insert(cell);
btorf_push(log_id(cell)); btorf_push(log_id(cell));
if (cell->type.in("$add", "$sub", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr", "$shift", "$shiftx", if (cell->type.in("$add", "$sub", "$mul", "$and", "$or", "$xor", "$xnor", "$shl", "$sshl", "$shr", "$sshr", "$shift", "$shiftx",
"$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_")) "$concat", "$_AND_", "$_NAND_", "$_OR_", "$_NOR_", "$_XOR_", "$_XNOR_"))
{ {
string btor_op; string btor_op;
if (cell->type == "$add") btor_op = "add"; if (cell->type == "$add") btor_op = "add";
if (cell->type == "$sub") btor_op = "sub"; if (cell->type == "$sub") btor_op = "sub";
if (cell->type == "$mul") btor_op = "mul";
if (cell->type.in("$shl", "$sshl")) btor_op = "sll"; if (cell->type.in("$shl", "$sshl")) btor_op = "sll";
if (cell->type == "$shr") btor_op = "srl"; if (cell->type == "$shr") btor_op = "srl";
if (cell->type == "$sshr") btor_op = "sra"; if (cell->type == "$sshr") btor_op = "sra";
@ -146,6 +147,7 @@ struct BtorWorker
if (cell->type.in("$and", "$_AND_")) btor_op = "and"; if (cell->type.in("$and", "$_AND_")) btor_op = "and";
if (cell->type.in("$or", "$_OR_")) btor_op = "or"; if (cell->type.in("$or", "$_OR_")) btor_op = "or";
if (cell->type.in("$xor", "$_XOR_")) btor_op = "xor"; if (cell->type.in("$xor", "$_XOR_")) btor_op = "xor";
if (cell->type == "$concat") btor_op = "concat";
if (cell->type == "$_NAND_") btor_op = "nand"; if (cell->type == "$_NAND_") btor_op = "nand";
if (cell->type == "$_NOR_") btor_op = "nor"; if (cell->type == "$_NOR_") btor_op = "nor";
if (cell->type.in("$xnor", "$_XNOR_")) btor_op = "xnor"; if (cell->type.in("$xnor", "$_XNOR_")) btor_op = "xnor";
@ -214,6 +216,40 @@ struct BtorWorker
goto okay; goto okay;
} }
if (cell->type.in("$div", "$mod"))
{
string btor_op;
if (cell->type == "$div") btor_op = "div";
if (cell->type == "$mod") btor_op = "rem";
log_assert(!btor_op.empty());
int width = GetSize(cell->getPort("\\Y"));
width = std::max(width, GetSize(cell->getPort("\\A")));
width = std::max(width, GetSize(cell->getPort("\\B")));
bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
int sid = get_bv_sid(width);
int nid = next_nid++;
btorf("%d %c%s %d %d %d\n", nid, a_signed || b_signed ? 's' : 'u', btor_op.c_str(), sid, nid_a, nid_b);
SigSpec sig = sigmap(cell->getPort("\\Y"));
if (GetSize(sig) < width) {
int sid = get_bv_sid(GetSize(sig));
int nid2 = next_nid++;
btorf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig)-1);
nid = nid2;
}
add_nid_sig(nid, sig);
goto okay;
}
if (cell->type.in("$_ANDNOT_", "$_ORNOT_")) if (cell->type.in("$_ANDNOT_", "$_ORNOT_"))
{ {
int sid = get_bv_sid(1); int sid = get_bv_sid(1);

0
backends/btor/test_cells.sh Normal file → Executable file
View File