mirror of
https://github.com/YosysHQ/yosys
synced 2025-04-25 10:05:33 +00:00
write_btor: support $buf
* treated the same as $pos
This commit is contained in:
parent
2de9f00368
commit
9047290683
1 changed files with 3 additions and 3 deletions
|
@ -508,7 +508,7 @@ struct BtorWorker
|
||||||
goto okay;
|
goto okay;
|
||||||
}
|
}
|
||||||
|
|
||||||
if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos)))
|
if (cell->type.in(ID($not), ID($neg), ID($_NOT_), ID($pos), ID($buf)))
|
||||||
{
|
{
|
||||||
string btor_op;
|
string btor_op;
|
||||||
if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not";
|
if (cell->type.in(ID($not), ID($_NOT_))) btor_op = "not";
|
||||||
|
@ -520,9 +520,9 @@ struct BtorWorker
|
||||||
int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
|
int nid_a = get_sig_nid(cell->getPort(ID::A), width, a_signed);
|
||||||
SigSpec sig = sigmap(cell->getPort(ID::Y));
|
SigSpec sig = sigmap(cell->getPort(ID::Y));
|
||||||
|
|
||||||
// the $pos cell just passes through, all other cells need an actual operation applied
|
// the $pos/$buf cells just pass through, all other cells need an actual operation applied
|
||||||
int nid = nid_a;
|
int nid = nid_a;
|
||||||
if (cell->type != ID($pos))
|
if (!cell->type.in(ID($pos), ID($buf)))
|
||||||
{
|
{
|
||||||
log_assert(!btor_op.empty());
|
log_assert(!btor_op.empty());
|
||||||
int sid = get_bv_sid(width);
|
int sid = get_bv_sid(width);
|
||||||
|
|
Loading…
Add table
Add a link
Reference in a new issue