From 26644ea779e5a371b057da6270501e8649e9589f Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Mon, 2 Oct 2023 11:07:02 +0200 Subject: [PATCH 1/3] equiv_simple: Drop hollow conditional All the listed flip-flop types would be known cells, so the extra part of the conditional is without effect. --- passes/equiv/equiv_simple.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index 7621341a7..bea8876cc 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -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)) From dbf11da50a8364d1961c5b203058b518b47dff1c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Mon, 2 Oct 2023 11:08:50 +0200 Subject: [PATCH 2/3] equiv_simple: Do not special-case flip-flop types in cone expansion If there's an asynchronous flip-flop type, it will be caught by not having a synchronous SAT model later on. Otherwise we can support all flip-flops. --- passes/equiv/equiv_simple.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index bea8876cc..33b34fdbf 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -60,7 +60,7 @@ struct EquivSimpleWorker for (auto &conn : cell->connections()) if (yosys_celltypes.cell_input(cell->type, conn.first)) for (auto bit : sigmap(conn.second)) { - if (cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_), ID($ff), ID($_FF_))) { + if (RTLIL::builtin_ff_cell_types().count(cell->type)) { if (!conn.first.in(ID::CLK, ID::C)) next_seed.insert(bit); } else From 1f1f43edd9d7393978fb5c49de834291ace61d36 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Martin=20Povi=C5=A1er?= Date: Mon, 2 Oct 2023 11:10:20 +0200 Subject: [PATCH 3/3] equiv_simple: Fix seed handling in non-short mode --- passes/equiv/equiv_simple.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/passes/equiv/equiv_simple.cc b/passes/equiv/equiv_simple.cc index 33b34fdbf..2c9d82914 100644 --- a/passes/equiv/equiv_simple.cc +++ b/passes/equiv/equiv_simple.cc @@ -133,11 +133,9 @@ struct EquivSimpleWorker for (auto bit_a : seed_a) find_input_cone(next_seed_a, full_cells_cone_a, full_bits_cone_a, no_stop_cells, no_stop_bits, nullptr, bit_a); - next_seed_a.clear(); for (auto bit_b : seed_b) find_input_cone(next_seed_b, full_cells_cone_b, full_bits_cone_b, no_stop_cells, no_stop_bits, nullptr, bit_b); - next_seed_b.clear(); pool short_cells_cone_a, short_cells_cone_b; pool short_bits_cone_a, short_bits_cone_b; @@ -145,10 +143,12 @@ struct EquivSimpleWorker if (short_cones) { + next_seed_a.clear(); for (auto bit_a : seed_a) find_input_cone(next_seed_a, short_cells_cone_a, short_bits_cone_a, full_cells_cone_b, full_bits_cone_b, &input_bits, bit_a); next_seed_a.swap(seed_a); + next_seed_b.clear(); for (auto bit_b : seed_b) find_input_cone(next_seed_b, short_cells_cone_b, short_bits_cone_b, full_cells_cone_a, full_bits_cone_a, &input_bits, bit_b); next_seed_b.swap(seed_b);