Skip to content

Commit

Permalink
equiv_simple: Drop hollow conditional
Browse files Browse the repository at this point in the history 
All the listed flip-flop types would be known cells, so the extra part
of the conditional is without effect.
  • Loading branch information
@povik
povik committed Oct 3, 2023
1 parent 493685b commit 26644ea
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion passes/equiv/equiv_simple.cc
View file
Original file line number Diff line number Diff line change
Expand Up @@ -364,7 +364,7 @@ struct EquivSimplePass : public Pass {
unproven_cells_counter, GetSize(unproven_equiv_cells), log_id(module));

for (auto cell : module->cells()) {
if (!ct.cell_known(cell->type) && !cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_), ID($ff), ID($_FF_)))
if (!ct.cell_known(cell->type))
continue;
for (auto &conn : cell->connections())
if (yosys_celltypes.cell_output(cell->type, conn.first))
Expand Down

7 comments on commit 26644ea

@ArkadyKlimov
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It seems like ct does not contain these ff cells, see the definition above:

CellTypes ct;
ct.setup_internals();
ct.setup_stdcells();

Perhaps we also need to add

ct.setup_internals_ff();

or it might be better to use && ! RTLIL::builtin_ff_cell_types().count(cell->type) instead, just like in line 63.
As I checked, in the current version, all such cells do not appear in the bit2driver.

@povik
Copy link
Member Author

@povik povik commented on 26644ea Feb 20, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But the check that was removed is in negation, so those FF types not being in ct is consistent with the conditional being hollow, no?

@povik
Copy link
Member Author

@povik povik commented on 26644ea Feb 20, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, sorry, wrote too soon, scratch that. I will look into it again later.

@povik
Copy link
Member Author

@povik povik commented on 26644ea Feb 21, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

@ArkadyKlimov, by the way, I see you are trying out LEC with Yosys, make sure you look at EQY, which is the recommended tool for that: https://github.com/YosysHQ/eqy

@povik
Copy link
Member Author

@povik povik commented on 26644ea Feb 21, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Better link here: https://yosyshq.readthedocs.io/projects/eqy/en/latest/

@ArkadyKlimov
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks for the information, I didn't know about that. But why eqy? As far as I could understand, it is just an add-on, a front-end, perhaps more friendly, over yosys itself and, possibly, other tools (SMT solvers, ABC, etc.) But will it really be easier to deal with?

@povik
Copy link
Member Author

@povik povik commented on 26644ea Feb 23, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

But why eqy?

EQY is meant to be a full-fledged tool that users can use to perform LEC on their designs. It's better maintained, scales better on large designs (due to partitioning), and allows for different proof strategies. It doesn't rely on the equiv_* passes which are part of Yosys, those are more of a tool for internal Yosys testing.

Please sign in to comment.