From a071afd938802dbb354e7e557331da488e98ec73 Mon Sep 17 00:00:00 2001 From: Iztok Jeras Date: Thu, 25 Jun 2026 01:11:02 +0200 Subject: [PATCH 01/16] documentation: avoid documentation rendering issue --- passes/sat/sat.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index accfe0399..9afd609c8 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -931,8 +931,8 @@ struct SatPass : public Pass { log("and additional constraints passed as parameters.\n"); log("\n"); log(" -all\n"); - log(" show all solutions to the problem (this can grow exponentially, use\n"); - log(" -max instead to get solutions)\n"); + log(" show all solutions to the problem (this can grow exponentially,\n"); + log(" use -max instead to get solutions)\n"); log("\n"); log(" -max \n"); log(" like -all, but limit number of solutions to \n"); From 0a5e35257e49c38bed16fdcac7530530ca30fe21 Mon Sep 17 00:00:00 2001 From: Iztok Jeras Date: Mon, 22 Jun 2026 02:44:46 +0200 Subject: [PATCH 02/16] dfflegalize: make it explicit in the documentation, that the pass operates on FFs and LATCHes --- passes/techmap/dfflegalize.cc | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/passes/techmap/dfflegalize.cc b/passes/techmap/dfflegalize.cc index 53f25c341..1f3a9ff33 100644 --- a/passes/techmap/dfflegalize.cc +++ b/passes/techmap/dfflegalize.cc @@ -67,7 +67,7 @@ enum FfInit { }; struct DffLegalizePass : public Pass { - DffLegalizePass() : Pass("dfflegalize", "convert FFs to types supported by the target") { } + DffLegalizePass() : Pass("dfflegalize", "convert FFs and LATCHes to types supported by the target") { } void help() override { // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| @@ -1071,7 +1071,7 @@ struct DffLegalizePass : public Pass { void execute(std::vector args, RTLIL::Design *design) override { - log_header(design, "Executing DFFLEGALIZE pass (convert FFs to types supported by the target).\n"); + log_header(design, "Executing DFFLEGALIZE pass (convert FFs and LATCHes to types supported by the target).\n"); for (int i = 0; i < NUM_FFTYPES; i++) { for (int j = 0; j < NUM_NEG; j++) From 23ead8ef4c947d1dbfa506c6cdb2ad60b9642bc5 Mon Sep 17 00:00:00 2001 From: Iztok Jeras Date: Mon, 22 Jun 2026 01:00:09 +0200 Subject: [PATCH 03/16] dfflibmap: fixing apparent typo in testcase --- tests/techmap/dfflibmap.ys | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/techmap/dfflibmap.ys b/tests/techmap/dfflibmap.ys index b5ba8fe63..87ecc8bc7 100644 --- a/tests/techmap/dfflibmap.ys +++ b/tests/techmap/dfflibmap.ys @@ -23,7 +23,7 @@ read_liberty -lib dfflibmap.lib equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty dfflibmap.lib -dfflibmap -prepare -liberty dffl*bmap.lib +dfflibmap -prepare -liberty dfflibmap.lib equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dfflibmap.lib design -load orig From 76ec42122b43f64e38a3eecc40b5d023419c6428 Mon Sep 17 00:00:00 2001 From: Iztok Jeras Date: Sun, 21 Jun 2026 17:21:49 +0200 Subject: [PATCH 04/16] dfflibmap: support for mapping latch cells --- passes/techmap/dfflibmap.cc | 367 ++++++++++++++++++++++++++++++++---- 1 file changed, 333 insertions(+), 34 deletions(-) diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc index b2caae460..66d82e3a4 100644 --- a/passes/techmap/dfflibmap.cc +++ b/passes/techmap/dfflibmap.cc @@ -36,7 +36,7 @@ static std::map cell_mappings; static void logmap(IdString dff) { if (cell_mappings.count(dff) == 0) { - log(" unmapped dff cell: %s\n", dff); + log(" unmapped dff/dlatch cell: %s\n", dff); } else { log(" %s %s (", cell_mappings[dff].cell_name, dff.substr(1)); bool first = true; @@ -80,6 +80,27 @@ static void logmap_all() logmap(ID($_DFFSR_PNP_)); logmap(ID($_DFFSR_PPN_)); logmap(ID($_DFFSR_PPP_)); + + logmap(ID($_DLATCH_N_)); + logmap(ID($_DLATCH_P_)); + + logmap(ID($_DLATCH_NN0_)); + logmap(ID($_DLATCH_NN1_)); + logmap(ID($_DLATCH_NP0_)); + logmap(ID($_DLATCH_NP1_)); + logmap(ID($_DLATCH_PN0_)); + logmap(ID($_DLATCH_PN1_)); + logmap(ID($_DLATCH_PP0_)); + logmap(ID($_DLATCH_PP1_)); + + logmap(ID($_DLATCHSR_NNN_)); + logmap(ID($_DLATCHSR_NNP_)); + logmap(ID($_DLATCHSR_NPN_)); + logmap(ID($_DLATCHSR_NPP_)); + logmap(ID($_DLATCHSR_PNN_)); + logmap(ID($_DLATCHSR_PNP_)); + logmap(ID($_DLATCHSR_PPN_)); + logmap(ID($_DLATCHSR_PPP_)); } static bool parse_next_state(const LibertyAst *cell, const LibertyAst *attr, std::string &data_name, bool &data_not_inverted, std::string &enable_name, bool &enable_not_inverted) @@ -234,7 +255,7 @@ static bool parse_pin(const LibertyAst *cell, const LibertyAst *attr, std::strin return false; } -static void find_cell(std::vector cells, IdString cell_type, bool clkpol, bool has_reset, bool rstpol, bool rstval, bool has_enable, bool enapol, std::vector &dont_use_cells) +static void find_cell_dff(std::vector cells, IdString cell_type, bool clkpol, bool has_reset, bool rstpol, bool rstval, bool has_enable, bool enapol, std::vector &dont_use_cells) { const LibertyAst *best_cell = nullptr; std::map best_cell_ports; @@ -362,7 +383,7 @@ static void find_cell(std::vector cells, IdString cell_type, } } -static void find_cell_sr(std::vector cells, IdString cell_type, bool clkpol, bool setpol, bool clrpol, bool has_enable, bool enapol, std::vector &dont_use_cells) +static void find_cell_dffsr(std::vector cells, IdString cell_type, bool clkpol, bool setpol, bool clrpol, bool has_enable, bool enapol, std::vector &dont_use_cells) { const LibertyAst *best_cell = nullptr; std::map best_cell_ports; @@ -494,9 +515,262 @@ static void find_cell_sr(std::vector cells, IdString cell_ty } } +static void find_cell_dlatch(std::vector cells, IdString cell_type, bool enablepol, bool has_reset, bool rstpol, bool rstval, std::vector &dont_use_cells) +{ + const LibertyAst *best_cell = nullptr; + std::map best_cell_ports; + int best_cell_pins = 0; + bool best_cell_noninv = false; + double best_cell_area = 0; + + for (auto cell : cells) + { + const LibertyAst *dn = cell->find("dont_use"); + if (dn != nullptr && dn->value == "true") + continue; + + bool dont_use = false; + for (std::string &dont_use_cell : dont_use_cells) + { + if (patmatch(dont_use_cell.c_str(), cell->args[0].c_str())) + { + dont_use = true; + break; + } + } + if (dont_use) + continue; + + const LibertyAst *latch = cell->find("latch"); + if (latch == nullptr) + continue; + + std::string cell_enable_pin, cell_rst_pin, cell_data_pin; + bool cell_enable_pol, cell_rst_pol, cell_data_pol; + + if (!parse_pin(cell, latch->find("enable"), cell_enable_pin, cell_enable_pol) || cell_enable_pol != enablepol) + continue; + if (!parse_pin(cell, latch->find("data_in"), cell_data_pin, cell_data_pol)) + continue; + + if (has_reset && !cell_data_pol) { + // data_in is negated + // we later propagate this inversion to the output, + // which requires the negation of the reset value + rstval = !rstval; + } + if (has_reset && rstval == false) { + if (!parse_pin(cell, latch->find("clear"), cell_rst_pin, cell_rst_pol) || cell_rst_pol != rstpol) + continue; + } + if (has_reset && rstval == true) { + if (!parse_pin(cell, latch->find("preset"), cell_rst_pin, cell_rst_pol) || cell_rst_pol != rstpol) + continue; + } + + std::map this_cell_ports; + this_cell_ports[cell_enable_pin] = 'E'; + if (has_reset) + this_cell_ports[cell_rst_pin] = 'R'; + this_cell_ports[cell_data_pin] = 'D'; + + double area = 0; + const LibertyAst *ar = cell->find("area"); + if (ar != nullptr && !ar->value.empty()) + area = atof(ar->value.c_str()); + + int num_pins = 0; + bool found_output = false; + bool found_noninv_output = false; + for (auto pin : cell->children) + { + if (pin->id != "pin" || pin->args.size() != 1) + continue; + + const LibertyAst *dir = pin->find("direction"); + if (dir == nullptr || dir->value == "internal") + continue; + num_pins++; + + if (dir->value == "input" && this_cell_ports.count(pin->args[0]) == 0) + goto continue_cell_loop; + + const LibertyAst *func = pin->find("function"); + if (dir->value == "output" && func != nullptr) { + std::string value = func->value; + for (size_t pos = value.find_first_of("\" \t"); pos != std::string::npos; pos = value.find_first_of("\" \t")) + value.erase(pos, 1); + if (value == latch->args[0]) { + this_cell_ports[pin->args[0]] = cell_data_pol ? 'Q' : 'q'; + if (cell_data_pol) + found_noninv_output = true; + found_output = true; + } else + if (value == latch->args[1]) { + this_cell_ports[pin->args[0]] = cell_data_pol ? 'q' : 'Q'; + if (!cell_data_pol) + found_noninv_output = true; + found_output = true; + } + } + + if (this_cell_ports.count(pin->args[0]) == 0) + this_cell_ports[pin->args[0]] = 0; + } + + if (!found_output || (best_cell != nullptr && (num_pins > best_cell_pins || (best_cell_noninv && !found_noninv_output)))) + continue; + + if (best_cell != nullptr && num_pins == best_cell_pins && area > best_cell_area) + continue; + + best_cell = cell; + best_cell_pins = num_pins; + best_cell_area = area; + best_cell_noninv = found_noninv_output; + best_cell_ports.swap(this_cell_ports); + continue_cell_loop:; + } + + if (best_cell != nullptr) { + log(" cell %s (%sinv, pins=%d, area=%.2f) is a direct match for cell type %s.\n", + best_cell->args[0].c_str(), best_cell_noninv ? "non" : "", best_cell_pins, best_cell_area, cell_type.c_str()); + cell_mappings[cell_type].cell_name = RTLIL::escape_id(best_cell->args[0]); + cell_mappings[cell_type].ports = best_cell_ports; + } +} + +static void find_cell_dlatchsr(std::vector cells, IdString cell_type, bool enablepol, bool setpol, bool clrpol, std::vector &dont_use_cells) +{ + const LibertyAst *best_cell = nullptr; + std::map best_cell_ports; + int best_cell_pins = 0; + bool best_cell_noninv = false; + double best_cell_area = 0; + + for (auto cell : cells) + { + const LibertyAst *dn = cell->find("dont_use"); + if (dn != nullptr && dn->value == "true") + continue; + + bool dont_use = false; + for (std::string &dont_use_cell : dont_use_cells) + { + if (patmatch(dont_use_cell.c_str(), cell->args[0].c_str())) + { + dont_use = true; + break; + } + } + if (dont_use) + continue; + + const LibertyAst *latch = cell->find("latch"); + if (latch == nullptr) + continue; + + std::string cell_enable_pin, cell_set_pin, cell_clr_pin, cell_data_pin; + bool cell_enable_pol, cell_set_pol, cell_clr_pol, cell_data_pol; + + if (!parse_pin(cell, latch->find("enable"), cell_enable_pin, cell_enable_pol) || cell_enable_pol != enablepol) + continue; + if (!parse_pin(cell, latch->find("data_in"), cell_data_pin, cell_data_pol)) + continue; + + if (!parse_pin(cell, latch->find("preset"), cell_set_pin, cell_set_pol)) + continue; + if (!parse_pin(cell, latch->find("clear"), cell_clr_pin, cell_clr_pol)) + continue; + if (!cell_data_pol) { + // data_in is negated + // we later propagate this inversion to the output, + // which requires the swap of set and reset + std::swap(cell_set_pin, cell_clr_pin); + std::swap(cell_set_pol, cell_clr_pol); + } + if (cell_set_pol != setpol) + continue; + if (cell_clr_pol != clrpol) + continue; + + std::map this_cell_ports; + this_cell_ports[cell_enable_pin] = 'E'; + this_cell_ports[cell_set_pin] = 'S'; + this_cell_ports[cell_clr_pin] = 'R'; + this_cell_ports[cell_data_pin] = 'D'; + + double area = 0; + const LibertyAst *ar = cell->find("area"); + if (ar != nullptr && !ar->value.empty()) + area = atof(ar->value.c_str()); + + int num_pins = 0; + bool found_output = false; + bool found_noninv_output = false; + for (auto pin : cell->children) + { + if (pin->id != "pin" || pin->args.size() != 1) + continue; + + const LibertyAst *dir = pin->find("direction"); + if (dir == nullptr || dir->value == "internal") + continue; + num_pins++; + + if (dir->value == "input" && this_cell_ports.count(pin->args[0]) == 0) + goto continue_cell_loop; + + const LibertyAst *func = pin->find("function"); + if (dir->value == "output" && func != nullptr) { + std::string value = func->value; + for (size_t pos = value.find_first_of("\" \t"); pos != std::string::npos; pos = value.find_first_of("\" \t")) + value.erase(pos, 1); + if (value == latch->args[0]) { + // next_state negation propagated to output + this_cell_ports[pin->args[0]] = cell_data_pol ? 'Q' : 'q'; + if (cell_data_pol) + found_noninv_output = true; + found_output = true; + } else + if (value == latch->args[1]) { + // next_state negation propagated to output + this_cell_ports[pin->args[0]] = cell_data_pol ? 'q' : 'Q'; + if (!cell_data_pol) + found_noninv_output = true; + found_output = true; + } + } + + if (this_cell_ports.count(pin->args[0]) == 0) + this_cell_ports[pin->args[0]] = 0; + } + + if (!found_output || (best_cell != nullptr && (num_pins > best_cell_pins || (best_cell_noninv && !found_noninv_output)))) + continue; + + if (best_cell != nullptr && num_pins == best_cell_pins && area > best_cell_area) + continue; + + best_cell = cell; + best_cell_pins = num_pins; + best_cell_area = area; + best_cell_noninv = found_noninv_output; + best_cell_ports.swap(this_cell_ports); + continue_cell_loop:; + } + + if (best_cell != nullptr) { + log(" cell %s (%sinv, pins=%d, area=%.2f) is a direct match for cell type %s.\n", + best_cell->args[0].c_str(), best_cell_noninv ? "non" : "", best_cell_pins, best_cell_area, cell_type.c_str()); + cell_mappings[cell_type].cell_name = RTLIL::escape_id(best_cell->args[0]); + cell_mappings[cell_type].ports = best_cell_ports; + } +} + static void dfflibmap(RTLIL::Design *design, RTLIL::Module *module) { - log("Mapping DFF cells in module `%s':\n", module->name); + log("Mapping DFF/DLATCH cells in module `%s':\n", module->name); dict> notmap; SigMap sigmap(module); @@ -569,19 +843,19 @@ static void dfflibmap(RTLIL::Design *design, RTLIL::Module *module) } struct DfflibmapPass : public Pass { - DfflibmapPass() : Pass("dfflibmap", "technology mapping of flip-flops") { } + DfflibmapPass() : Pass("dfflibmap", "technology mapping of flip-flops and latches") { } void help() override { log("\n"); log(" dfflibmap [-prepare] [-map-only] [-info] [-dont_use ] -liberty [selection]\n"); log("\n"); - log("Map internal flip-flop cells to the flip-flop cells in the technology\n"); - log("library specified in the given liberty files.\n"); + log("Map internal flip-flop/latch cells to the flip-flop/latch cells in the\n"); + log("technology library specified in the given liberty files.\n"); log("\n"); log("This pass may add inverters as needed. Therefore it is recommended to\n"); log("first run this pass and then map the logic paths to the target technology.\n"); log("\n"); - log("When called with -prepare, this command will convert the internal FF cells\n"); + log("When called with -prepare, this command will convert the internal FF/LATCH cells\n"); log("to the internal cell types that best match the cells found in the given\n"); log("liberty file, but won't actually map them to the target cells.\n"); log("\n"); @@ -591,7 +865,7 @@ struct DfflibmapPass : public Pass { log("\n"); log("When called with -info, this command will only print the target cell\n"); log("list, along with their associated internal cell types, and the arguments\n"); - log("that would be passed to the dfflegalize pass. The design will not be\n"); + log("that would be passed to the dfflegalize pass. The design will not be\n"); log("changed.\n"); log("\n"); log("When called with -dont_use, this command will not map to the specified cell\n"); @@ -602,7 +876,7 @@ struct DfflibmapPass : public Pass { } void execute(std::vector args, RTLIL::Design *design) override { - log_header(design, "Executing DFFLIBMAP pass (mapping DFF cells to sequential cells from liberty file).\n"); + log_header(design, "Executing DFFLIBMAP pass (mapping DFF/DLATCH cells to sequential cells from liberty file).\n"); log_push(); bool prepare_mode = false; @@ -661,40 +935,65 @@ struct DfflibmapPass : public Pass { delete f; } - find_cell(merged.cells, ID($_DFF_N_), false, false, false, false, false, false, dont_use_cells); - find_cell(merged.cells, ID($_DFF_P_), true, false, false, false, false, false, dont_use_cells); + // cells, cell_type , c_pol, has_r, r_pol, r_val, has_e, e_pol + find_cell_dff(merged.cells, ID($_DFF_N_), false, false, false, false, false, false, dont_use_cells); + find_cell_dff(merged.cells, ID($_DFF_P_), true, false, false, false, false, false, dont_use_cells); - find_cell(merged.cells, ID($_DFF_NN0_), false, true, false, false, false, false, dont_use_cells); - find_cell(merged.cells, ID($_DFF_NN1_), false, true, false, true, false, false, dont_use_cells); - find_cell(merged.cells, ID($_DFF_NP0_), false, true, true, false, false, false, dont_use_cells); - find_cell(merged.cells, ID($_DFF_NP1_), false, true, true, true, false, false, dont_use_cells); - find_cell(merged.cells, ID($_DFF_PN0_), true, true, false, false, false, false, dont_use_cells); - find_cell(merged.cells, ID($_DFF_PN1_), true, true, false, true, false, false, dont_use_cells); - find_cell(merged.cells, ID($_DFF_PP0_), true, true, true, false, false, false, dont_use_cells); - find_cell(merged.cells, ID($_DFF_PP1_), true, true, true, true, false, false, dont_use_cells); + find_cell_dff(merged.cells, ID($_DFF_NN0_), false, true, false, false, false, false, dont_use_cells); + find_cell_dff(merged.cells, ID($_DFF_NN1_), false, true, false, true, false, false, dont_use_cells); + find_cell_dff(merged.cells, ID($_DFF_NP0_), false, true, true, false, false, false, dont_use_cells); + find_cell_dff(merged.cells, ID($_DFF_NP1_), false, true, true, true, false, false, dont_use_cells); + find_cell_dff(merged.cells, ID($_DFF_PN0_), true, true, false, false, false, false, dont_use_cells); + find_cell_dff(merged.cells, ID($_DFF_PN1_), true, true, false, true, false, false, dont_use_cells); + find_cell_dff(merged.cells, ID($_DFF_PP0_), true, true, true, false, false, false, dont_use_cells); + find_cell_dff(merged.cells, ID($_DFF_PP1_), true, true, true, true, false, false, dont_use_cells); - find_cell(merged.cells, ID($_DFFE_NN_), false, false, false, false, true, false, dont_use_cells); - find_cell(merged.cells, ID($_DFFE_NP_), false, false, false, false, true, true, dont_use_cells); - find_cell(merged.cells, ID($_DFFE_PN_), true, false, false, false, true, false, dont_use_cells); - find_cell(merged.cells, ID($_DFFE_PP_), true, false, false, false, true, true, dont_use_cells); + find_cell_dff(merged.cells, ID($_DFFE_NN_), false, false, false, false, true, false, dont_use_cells); + find_cell_dff(merged.cells, ID($_DFFE_NP_), false, false, false, false, true, true, dont_use_cells); + find_cell_dff(merged.cells, ID($_DFFE_PN_), true, false, false, false, true, false, dont_use_cells); + find_cell_dff(merged.cells, ID($_DFFE_PP_), true, false, false, false, true, true, dont_use_cells); - find_cell_sr(merged.cells, ID($_DFFSR_NNN_), false, false, false, false, false, dont_use_cells); - find_cell_sr(merged.cells, ID($_DFFSR_NNP_), false, false, true, false, false, dont_use_cells); - find_cell_sr(merged.cells, ID($_DFFSR_NPN_), false, true, false, false, false, dont_use_cells); - find_cell_sr(merged.cells, ID($_DFFSR_NPP_), false, true, true, false, false, dont_use_cells); - find_cell_sr(merged.cells, ID($_DFFSR_PNN_), true, false, false, false, false, dont_use_cells); - find_cell_sr(merged.cells, ID($_DFFSR_PNP_), true, false, true, false, false, dont_use_cells); - find_cell_sr(merged.cells, ID($_DFFSR_PPN_), true, true, false, false, false, dont_use_cells); - find_cell_sr(merged.cells, ID($_DFFSR_PPP_), true, true, true, false, false, dont_use_cells); + // cells, cell_type , c_pol, s_pol, r_pol, has_e, e_pol + find_cell_dffsr(merged.cells, ID($_DFFSR_NNN_), false, false, false, false, false, dont_use_cells); + find_cell_dffsr(merged.cells, ID($_DFFSR_NNP_), false, false, true, false, false, dont_use_cells); + find_cell_dffsr(merged.cells, ID($_DFFSR_NPN_), false, true, false, false, false, dont_use_cells); + find_cell_dffsr(merged.cells, ID($_DFFSR_NPP_), false, true, true, false, false, dont_use_cells); + find_cell_dffsr(merged.cells, ID($_DFFSR_PNN_), true, false, false, false, false, dont_use_cells); + find_cell_dffsr(merged.cells, ID($_DFFSR_PNP_), true, false, true, false, false, dont_use_cells); + find_cell_dffsr(merged.cells, ID($_DFFSR_PPN_), true, true, false, false, false, dont_use_cells); + find_cell_dffsr(merged.cells, ID($_DFFSR_PPP_), true, true, true, false, false, dont_use_cells); - log(" final dff cell mappings:\n"); + // cells, cell_type , e_pol, has_r, r_pol, r_val + find_cell_dlatch(merged.cells, ID($_DLATCH_N_), false, false, false, false, dont_use_cells); + find_cell_dlatch(merged.cells, ID($_DLATCH_P_), true, false, false, false, dont_use_cells); + + find_cell_dlatch(merged.cells, ID($_DLATCH_NN0_), false, true, false, false, dont_use_cells); + find_cell_dlatch(merged.cells, ID($_DLATCH_NN1_), false, true, false, true, dont_use_cells); + find_cell_dlatch(merged.cells, ID($_DLATCH_NP0_), false, true, true, false, dont_use_cells); + find_cell_dlatch(merged.cells, ID($_DLATCH_NP1_), false, true, true, true, dont_use_cells); + find_cell_dlatch(merged.cells, ID($_DLATCH_PN0_), true, true, false, false, dont_use_cells); + find_cell_dlatch(merged.cells, ID($_DLATCH_PN1_), true, true, false, true, dont_use_cells); + find_cell_dlatch(merged.cells, ID($_DLATCH_PP0_), true, true, true, false, dont_use_cells); + find_cell_dlatch(merged.cells, ID($_DLATCH_PP1_), true, true, true, true, dont_use_cells); + + // cells, cell_type , e_pol, s_pol, r_pol + find_cell_dlatchsr(merged.cells, ID($_DLATCHSR_NNN_), false, false, false, dont_use_cells); + find_cell_dlatchsr(merged.cells, ID($_DLATCHSR_NNP_), false, false, true, dont_use_cells); + find_cell_dlatchsr(merged.cells, ID($_DLATCHSR_NPN_), false, true, false, dont_use_cells); + find_cell_dlatchsr(merged.cells, ID($_DLATCHSR_NPP_), false, true, true, dont_use_cells); + find_cell_dlatchsr(merged.cells, ID($_DLATCHSR_PNN_), true, false, false, dont_use_cells); + find_cell_dlatchsr(merged.cells, ID($_DLATCHSR_PNP_), true, false, true, dont_use_cells); + find_cell_dlatchsr(merged.cells, ID($_DLATCHSR_PPN_), true, true, false, dont_use_cells); + find_cell_dlatchsr(merged.cells, ID($_DLATCHSR_PPP_), true, true, true, dont_use_cells); + + log(" final dff/dlatch cell mappings:\n"); logmap_all(); if (!map_only_mode) { std::string dfflegalize_cmd = "dfflegalize"; for (auto it : cell_mappings) dfflegalize_cmd += stringf(" -cell %s 01", it.first); - dfflegalize_cmd += " t:$_DFF* t:$_SDFF*"; + dfflegalize_cmd += " t:$_DFF* t:$_SDFF* t:$_DLATCH*"; if (info_mode) { log("dfflegalize command line: %s\n", dfflegalize_cmd); } else { From 65f9d017ec889da39c0782b835f1bccb870cbfbc Mon Sep 17 00:00:00 2001 From: Iztok Jeras Date: Sat, 27 Jun 2026 02:00:10 +0200 Subject: [PATCH 05/16] dfflibmap: recommend running opt_merge pass after dfflibmap --- passes/techmap/dfflibmap.cc | 2 ++ 1 file changed, 2 insertions(+) diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc index 66d82e3a4..6a5fbe204 100644 --- a/passes/techmap/dfflibmap.cc +++ b/passes/techmap/dfflibmap.cc @@ -854,6 +854,8 @@ struct DfflibmapPass : public Pass { log("\n"); log("This pass may add inverters as needed. Therefore it is recommended to\n"); log("first run this pass and then map the logic paths to the target technology.\n"); + log("Since inverters are added for each technology cell, an opt_merge pass\n"); + log("would reduce the redundancy.\n"); log("\n"); log("When called with -prepare, this command will convert the internal FF/LATCH cells\n"); log("to the internal cell types that best match the cells found in the given\n"); From 4f9b34615162f005ec7197d81c018bea14ddc037 Mon Sep 17 00:00:00 2001 From: Iztok Jeras Date: Tue, 23 Jun 2026 23:15:23 +0200 Subject: [PATCH 06/16] dfflibmap: simpler handling of cells with inverted data input polarity --- passes/techmap/dfflibmap.cc | 21 ++++----------------- 1 file changed, 4 insertions(+), 17 deletions(-) diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc index 6a5fbe204..516043db7 100644 --- a/passes/techmap/dfflibmap.cc +++ b/passes/techmap/dfflibmap.cc @@ -293,18 +293,11 @@ static void find_cell_dff(std::vector cells, IdString cell_t if (!parse_next_state(cell, ff->find("next_state"), cell_next_pin, cell_next_pol, cell_enable_pin, cell_enable_pol) || (has_enable && (cell_enable_pin.empty() || cell_enable_pol != enapol))) continue; - bool cell_rstval = rstval; - if (has_reset && !cell_next_pol) { - // next_state is negated - // we later propagate this inversion to the output, - // which requires the negation of the reset value - cell_rstval = !rstval; - } - if (has_reset && cell_rstval == false) { + if (has_reset && rstval != cell_next_pol) { if (!parse_pin(cell, ff->find("clear"), cell_rst_pin, cell_rst_pol) || cell_rst_pol != rstpol) continue; } - if (has_reset && cell_rstval == true) { + if (has_reset && rstval == cell_next_pol) { if (!parse_pin(cell, ff->find("preset"), cell_rst_pin, cell_rst_pol) || cell_rst_pol != rstpol) continue; } @@ -553,17 +546,11 @@ static void find_cell_dlatch(std::vector cells, IdString cel if (!parse_pin(cell, latch->find("data_in"), cell_data_pin, cell_data_pol)) continue; - if (has_reset && !cell_data_pol) { - // data_in is negated - // we later propagate this inversion to the output, - // which requires the negation of the reset value - rstval = !rstval; - } - if (has_reset && rstval == false) { + if (has_reset && rstval != cell_data_pol) { if (!parse_pin(cell, latch->find("clear"), cell_rst_pin, cell_rst_pol) || cell_rst_pol != rstpol) continue; } - if (has_reset && rstval == true) { + if (has_reset && rstval == cell_data_pol) { if (!parse_pin(cell, latch->find("preset"), cell_rst_pin, cell_rst_pol) || cell_rst_pol != rstpol) continue; } From 4a6ae2fdd4434719db1df9157f21fd789a26f3b9 Mon Sep 17 00:00:00 2001 From: Iztok Jeras Date: Wed, 24 Jun 2026 04:22:39 +0200 Subject: [PATCH 07/16] frontends/liberty: support all \$_LATCH* type cells (copy/modify from FF code) --- frontends/liberty/liberty.cc | 127 ++++++++++++++++++----------------- 1 file changed, 66 insertions(+), 61 deletions(-) diff --git a/frontends/liberty/liberty.cc b/frontends/liberty/liberty.cc index 96db2f640..6e804efab 100644 --- a/frontends/liberty/liberty.cc +++ b/frontends/liberty/liberty.cc @@ -225,13 +225,13 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node) if (child->id == "preset") preset_sig = parse_func_expr(module, child->value.c_str()); - for (auto& [id, var] : {pair{"clear_preset_var1", &clear_preset_var1}, {"clear_preset_var2", &clear_preset_var2}}) + for (auto& [id, var] : {pair{"clear_preset_var1", &clear_preset_var1}, {"clear_preset_var2", &clear_preset_var2}}) { if (child->id == id) { if (child->value.size() != 1) log_error("Unexpected length of clear_preset_var* value %s in FF cell %s\n", child->value, name); *var = child->value[0]; } - + } } if (clk_sig.size() == 0 || data_sig.size() == 0) @@ -325,7 +325,10 @@ static bool create_latch(RTLIL::Module *module, const LibertyAst *node, bool fla auto [iq_sig, iqn_sig] = find_latch_ff_wires(module, node); RTLIL::SigSpec enable_sig, data_sig, clear_sig, preset_sig; bool enable_polarity = true, clear_polarity = true, preset_polarity = true; + const std::string name = module->name.unescape(); + std::optional clear_preset_var1; + std::optional clear_preset_var2; for (auto child : node->children) { if (child->id == "enable") enable_sig = parse_func_expr(module, child->value.c_str()); @@ -335,13 +338,21 @@ static bool create_latch(RTLIL::Module *module, const LibertyAst *node, bool fla clear_sig = parse_func_expr(module, child->value.c_str()); if (child->id == "preset") preset_sig = parse_func_expr(module, child->value.c_str()); + + for (auto& [id, var] : {pair{"clear_preset_var1", &clear_preset_var1}, {"clear_preset_var2", &clear_preset_var2}}) { + if (child->id == id) { + if (child->value.size() != 1) + log_error("Unexpected length of clear_preset_var* value %s in LATCH cell %s\n", child->value, name); + *var = child->value[0]; + } + } } if (enable_sig.size() == 0 || data_sig.size() == 0) { if (!flag_ignore_miss_data_latch) - log_error("Latch cell %s has no data_in and/or enable attribute.\n", module); + log_error("LATCH cell %s has no data_in and/or enable attribute.\n", name); else - log("Ignored latch cell %s with no data_in and/or enable attribute.\n", module); + log("Ignored LATCH cell %s with no data_in and/or enable attribute.\n", name); return false; } @@ -369,71 +380,65 @@ static bool create_latch(RTLIL::Module *module, const LibertyAst *node, bool fla } } - RTLIL::Cell *cell = module->addCell(NEW_ID, ID($_NOT_)); - cell->setPort(ID::A, iq_sig); - cell->setPort(ID::Y, iqn_sig); - - if (clear_sig.size() == 1) - { - RTLIL::SigSpec clear_negative = clear_sig; - RTLIL::SigSpec clear_enable = clear_sig; - - if (clear_polarity == true || clear_polarity != enable_polarity) - { - RTLIL::Cell *inv = module->addCell(NEW_ID, ID($_NOT_)); - inv->setPort(ID::A, clear_sig); - inv->setPort(ID::Y, module->addWire(NEW_ID)); - - if (clear_polarity == true) - clear_negative = inv->getPort(ID::Y); - if (clear_polarity != enable_polarity) - clear_enable = inv->getPort(ID::Y); + for (auto& [out_sig, cp_var, neg] : {tuple{iq_sig, clear_preset_var1, false}, {iqn_sig, clear_preset_var2, true}}) { + SigSpec q_sig = out_sig; + if (neg) { + q_sig = module->addWire(NEW_ID, out_sig.as_wire()); + module->addNotGate(NEW_ID, q_sig, out_sig); } - RTLIL::Cell *data_gate = module->addCell(NEW_ID, ID($_AND_)); - data_gate->setPort(ID::A, data_sig); - data_gate->setPort(ID::B, clear_negative); - data_gate->setPort(ID::Y, data_sig = module->addWire(NEW_ID)); + RTLIL::Cell* cell = module->addCell(NEW_ID, ""); + cell->setPort(ID::D, data_sig); + cell->setPort(ID::Q, q_sig); + cell->setPort(ID::E, enable_sig); - RTLIL::Cell *enable_gate = module->addCell(NEW_ID, enable_polarity ? ID($_OR_) : ID($_AND_)); - enable_gate->setPort(ID::A, enable_sig); - enable_gate->setPort(ID::B, clear_enable); - enable_gate->setPort(ID::Y, enable_sig = module->addWire(NEW_ID)); - } - - if (preset_sig.size() == 1) - { - RTLIL::SigSpec preset_positive = preset_sig; - RTLIL::SigSpec preset_enable = preset_sig; - - if (preset_polarity == false || preset_polarity != enable_polarity) - { - RTLIL::Cell *inv = module->addCell(NEW_ID, ID($_NOT_)); - inv->setPort(ID::A, preset_sig); - inv->setPort(ID::Y, module->addWire(NEW_ID)); - - if (preset_polarity == false) - preset_positive = inv->getPort(ID::Y); - if (preset_polarity != enable_polarity) - preset_enable = inv->getPort(ID::Y); + if (clear_sig.size() == 0 && preset_sig.size() == 0) { + cell->type = stringf("$_DLATCH_%c_", enable_polarity ? 'P' : 'N'); } - RTLIL::Cell *data_gate = module->addCell(NEW_ID, ID($_OR_)); - data_gate->setPort(ID::A, data_sig); - data_gate->setPort(ID::B, preset_positive); - data_gate->setPort(ID::Y, data_sig = module->addWire(NEW_ID)); + if (clear_sig.size() == 1 && preset_sig.size() == 0) { + cell->type = stringf("$_DLATCH_%c%c0_", enable_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N'); + cell->setPort(ID::R, clear_sig); + } - RTLIL::Cell *enable_gate = module->addCell(NEW_ID, enable_polarity ? ID($_OR_) : ID($_AND_)); - enable_gate->setPort(ID::A, enable_sig); - enable_gate->setPort(ID::B, preset_enable); - enable_gate->setPort(ID::Y, enable_sig = module->addWire(NEW_ID)); + if (clear_sig.size() == 0 && preset_sig.size() == 1) { + cell->type = stringf("$_DLATCH_%c%c1_", enable_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N'); + cell->setPort(ID::R, preset_sig); + } + + if (clear_sig.size() == 1 && preset_sig.size() == 1) { + cell->type = stringf("$_DLATCHSR_%c%c%c_", enable_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N'); + + SigBit s_sig = preset_sig; + SigBit r_sig = clear_sig; + if (cp_var && *cp_var != 'X') { + // Either set or reset dominates + bool set_dominates; + if (*cp_var == 'L') { + set_dominates = neg; + } else if (*cp_var == 'H') { + set_dominates = !neg; + } else { + log_error("LATCH cell %s has unsupported clear&preset behavior \'%c\'.\n", name, *cp_var); + } + log_debug("cell %s variable %d cp_var %c set dominates? %d\n", name, (int)neg + 1, *cp_var, set_dominates); + // S&R priority is well-defined now + if (set_dominates) { + r_sig = module->AndnotGate(NEW_ID, r_sig, s_sig); + } else { + s_sig = module->AndnotGate(NEW_ID, s_sig, r_sig); + } + } else { + log_debug("cell %s variable %d undef c&p behavior\n", name, (int)neg + 1); + } + + cell->setPort(ID::S, s_sig); + cell->setPort(ID::R, r_sig); + } + + log_assert(!cell->type.empty()); } - cell = module->addCell(NEW_ID, stringf("$_DLATCH_%c_", enable_polarity ? 'P' : 'N')); - cell->setPort(ID::D, data_sig); - cell->setPort(ID::Q, iq_sig); - cell->setPort(ID::E, enable_sig); - return true; } From e78f85f33a41425c9e818c38bdd615f9d88805c2 Mon Sep 17 00:00:00 2001 From: Iztok Jeras Date: Sun, 21 Jun 2026 22:29:21 +0200 Subject: [PATCH 08/16] dlatchlibmap: fixing failing test 'liberty/dff.lib' by updating the golden log output --- tests/liberty/dff.log.ok | 66 +++++++++++++++++++++++++--------------- 1 file changed, 42 insertions(+), 24 deletions(-) diff --git a/tests/liberty/dff.log.ok b/tests/liberty/dff.log.ok index be187181d..509d3464c 100644 --- a/tests/liberty/dff.log.ok +++ b/tests/liberty/dff.log.ok @@ -1,29 +1,47 @@ -- Running command `dfflibmap -info -liberty dff.lib' -- -1. Executing DFFLIBMAP pass (mapping DFF cells to sequential cells from liberty file). +1. Executing DFFLIBMAP pass (mapping DFF/DLATCH cells to sequential cells from liberty file). cell dff (noninv, pins=3, area=1.00) is a direct match for cell type $_DFF_P_. - final dff cell mappings: - unmapped dff cell: $_DFF_N_ + final dff/dlatch cell mappings: + unmapped dff/dlatch cell: $_DFF_N_ \dff _DFF_P_ (.CLK( C), .D( D), .Q( Q)); - unmapped dff cell: $_DFF_NN0_ - unmapped dff cell: $_DFF_NN1_ - unmapped dff cell: $_DFF_NP0_ - unmapped dff cell: $_DFF_NP1_ - unmapped dff cell: $_DFF_PN0_ - unmapped dff cell: $_DFF_PN1_ - unmapped dff cell: $_DFF_PP0_ - unmapped dff cell: $_DFF_PP1_ - unmapped dff cell: $_DFFE_NN_ - unmapped dff cell: $_DFFE_NP_ - unmapped dff cell: $_DFFE_PN_ - unmapped dff cell: $_DFFE_PP_ - unmapped dff cell: $_DFFSR_NNN_ - unmapped dff cell: $_DFFSR_NNP_ - unmapped dff cell: $_DFFSR_NPN_ - unmapped dff cell: $_DFFSR_NPP_ - unmapped dff cell: $_DFFSR_PNN_ - unmapped dff cell: $_DFFSR_PNP_ - unmapped dff cell: $_DFFSR_PPN_ - unmapped dff cell: $_DFFSR_PPP_ -dfflegalize command line: dfflegalize -cell $_DFF_P_ 01 t:$_DFF* t:$_SDFF* + unmapped dff/dlatch cell: $_DFF_NN0_ + unmapped dff/dlatch cell: $_DFF_NN1_ + unmapped dff/dlatch cell: $_DFF_NP0_ + unmapped dff/dlatch cell: $_DFF_NP1_ + unmapped dff/dlatch cell: $_DFF_PN0_ + unmapped dff/dlatch cell: $_DFF_PN1_ + unmapped dff/dlatch cell: $_DFF_PP0_ + unmapped dff/dlatch cell: $_DFF_PP1_ + unmapped dff/dlatch cell: $_DFFE_NN_ + unmapped dff/dlatch cell: $_DFFE_NP_ + unmapped dff/dlatch cell: $_DFFE_PN_ + unmapped dff/dlatch cell: $_DFFE_PP_ + unmapped dff/dlatch cell: $_DFFSR_NNN_ + unmapped dff/dlatch cell: $_DFFSR_NNP_ + unmapped dff/dlatch cell: $_DFFSR_NPN_ + unmapped dff/dlatch cell: $_DFFSR_NPP_ + unmapped dff/dlatch cell: $_DFFSR_PNN_ + unmapped dff/dlatch cell: $_DFFSR_PNP_ + unmapped dff/dlatch cell: $_DFFSR_PPN_ + unmapped dff/dlatch cell: $_DFFSR_PPP_ + unmapped dff/dlatch cell: $_DLATCH_N_ + unmapped dff/dlatch cell: $_DLATCH_P_ + unmapped dff/dlatch cell: $_DLATCH_NN0_ + unmapped dff/dlatch cell: $_DLATCH_NN1_ + unmapped dff/dlatch cell: $_DLATCH_NP0_ + unmapped dff/dlatch cell: $_DLATCH_NP1_ + unmapped dff/dlatch cell: $_DLATCH_PN0_ + unmapped dff/dlatch cell: $_DLATCH_PN1_ + unmapped dff/dlatch cell: $_DLATCH_PP0_ + unmapped dff/dlatch cell: $_DLATCH_PP1_ + unmapped dff/dlatch cell: $_DLATCHSR_NNN_ + unmapped dff/dlatch cell: $_DLATCHSR_NNP_ + unmapped dff/dlatch cell: $_DLATCHSR_NPN_ + unmapped dff/dlatch cell: $_DLATCHSR_NPP_ + unmapped dff/dlatch cell: $_DLATCHSR_PNN_ + unmapped dff/dlatch cell: $_DLATCHSR_PNP_ + unmapped dff/dlatch cell: $_DLATCHSR_PPN_ + unmapped dff/dlatch cell: $_DLATCHSR_PPP_ +dfflegalize command line: dfflegalize -cell $_DFF_P_ 01 t:$_DFF* t:$_SDFF* t:$_DLATCH* From 3fdbbf70eac139217cf42372f89f0e599c896bd8 Mon Sep 17 00:00:00 2001 From: Iztok Jeras Date: Mon, 22 Jun 2026 01:08:39 +0200 Subject: [PATCH 09/16] dlatchlibmap: making a copy of test files dfflibmap* to dlatchlibmap* --- tests/techmap/dlatchlibmap-sim.v | 31 ++ tests/techmap/dlatchlibmap.lib | 79 ++++++ tests/techmap/dlatchlibmap.ys | 99 +++++++ .../techmap/dlatchlibmap_dlatch_not_data.lib | 24 ++ tests/techmap/dlatchlibmap_dlatchn.lib | 47 +++ .../dlatchlibmap_dlatchsr_mixedpol.lib | 35 +++ .../dlatchlibmap_dlatchsr_not_data.lib | 28 ++ .../dlatchlibmap_dlatchsr_not_data_l.lib | 33 +++ tests/techmap/dlatchlibmap_dlatchsr_r.lib | 33 +++ tests/techmap/dlatchlibmap_dlatchsr_s.lib | 33 +++ tests/techmap/dlatchlibmap_dlatchsr_x.lib | 33 +++ tests/techmap/dlatchlibmap_formal.ys | 268 ++++++++++++++++++ tests/techmap/dlatchlibmap_proc_formal.ys | 100 +++++++ 13 files changed, 843 insertions(+) create mode 100644 tests/techmap/dlatchlibmap-sim.v create mode 100644 tests/techmap/dlatchlibmap.lib create mode 100644 tests/techmap/dlatchlibmap.ys create mode 100644 tests/techmap/dlatchlibmap_dlatch_not_data.lib create mode 100644 tests/techmap/dlatchlibmap_dlatchn.lib create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_mixedpol.lib create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_not_data.lib create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_not_data_l.lib create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_r.lib create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_s.lib create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_x.lib create mode 100644 tests/techmap/dlatchlibmap_formal.ys create mode 100644 tests/techmap/dlatchlibmap_proc_formal.ys diff --git a/tests/techmap/dlatchlibmap-sim.v b/tests/techmap/dlatchlibmap-sim.v new file mode 100644 index 000000000..42006a211 --- /dev/null +++ b/tests/techmap/dlatchlibmap-sim.v @@ -0,0 +1,31 @@ +module dffn(input CLK, D, output reg Q, output QN); + +always @(negedge CLK) + Q <= D; + +assign QN = ~Q; + +endmodule + +module dffsr(input CLK, D, CLEAR, PRESET, output reg Q, output QN); + +always @(posedge CLK, posedge CLEAR, posedge PRESET) + if (CLEAR) + Q <= 0; + else if (PRESET) + Q <= 1; + else + Q <= D; + +assign QN = ~Q; + +endmodule + +module dffe(input CLK, EN, D, output reg Q, output QN); + +always @(negedge CLK) + if (EN) Q <= D; + +assign QN = ~Q; + +endmodule diff --git a/tests/techmap/dlatchlibmap.lib b/tests/techmap/dlatchlibmap.lib new file mode 100644 index 000000000..54a44a296 --- /dev/null +++ b/tests/techmap/dlatchlibmap.lib @@ -0,0 +1,79 @@ +library(test) { + /* D-type flip-flop with asynchronous reset and preset */ + cell (dffn) { + area : 6; + ff("IQ", "IQN") { + next_state : "D"; + clocked_on : "!CLK"; + } + pin(D) { + direction : input; + } + pin(CLK) { + direction : input; + } + pin(Q) { + direction: output; + function : "IQ"; + } + pin(QN) { + direction: output; + function : "IQN"; + } + } + cell (dffsr) { + area : 6; + ff("IQ", "IQN") { + next_state : "D"; + clocked_on : "CLK"; + clear : "CLEAR"; + preset : "PRESET"; + clear_preset_var1 : L; + clear_preset_var2 : L; + } + pin(D) { + direction : input; + } + pin(CLK) { + direction : input; + } + pin(CLEAR) { + direction : input; + } + pin(PRESET) { + direction : input; + } + pin(Q) { + direction: output; + function : "IQ"; + } + pin(QN) { + direction: output; + function : "IQN"; + } + } + cell (dffe) { + area : 6; + ff("IQ", "IQN") { + next_state : "(D EN) | (IQ !EN)"; + clocked_on : "!CLK"; + } + pin(D) { + direction : input; + } + pin(EN) { + direction : input; + } + pin(CLK) { + direction : input; + } + pin(Q) { + direction: output; + function : "IQ"; + } + pin(QN) { + direction: output; + function : "IQN"; + } + } +} diff --git a/tests/techmap/dlatchlibmap.ys b/tests/techmap/dlatchlibmap.ys new file mode 100644 index 000000000..87ecc8bc7 --- /dev/null +++ b/tests/techmap/dlatchlibmap.ys @@ -0,0 +1,99 @@ +read_verilog -icells < Date: Mon, 22 Jun 2026 01:12:09 +0200 Subject: [PATCH 10/16] dlatchlibmap: modified copies of dfflibmap* test files for dlatchlibmap tests --- tests/techmap/dlatchlibmap-sim.v | 28 +--- tests/techmap/dlatchlibmap.lib | 52 ++----- tests/techmap/dlatchlibmap.ys | 97 ++++++------ .../techmap/dlatchlibmap_dlatch_not_data.lib | 12 +- tests/techmap/dlatchlibmap_dlatchn.lib | 35 +---- .../dlatchlibmap_dlatchsr_mixedpol.lib | 17 +- .../dlatchlibmap_dlatchsr_not_data.lib | 12 +- .../dlatchlibmap_dlatchsr_not_data_l.lib | 15 +- tests/techmap/dlatchlibmap_dlatchsr_r.lib | 15 +- tests/techmap/dlatchlibmap_dlatchsr_s.lib | 15 +- tests/techmap/dlatchlibmap_dlatchsr_x.lib | 15 +- tests/techmap/dlatchlibmap_formal.ys | 146 ++++++++---------- tests/techmap/dlatchlibmap_proc_formal.ys | 52 ++----- 13 files changed, 207 insertions(+), 304 deletions(-) diff --git a/tests/techmap/dlatchlibmap-sim.v b/tests/techmap/dlatchlibmap-sim.v index 42006a211..03a2e4817 100644 --- a/tests/techmap/dlatchlibmap-sim.v +++ b/tests/techmap/dlatchlibmap-sim.v @@ -1,30 +1,18 @@ -module dffn(input CLK, D, output reg Q, output QN); +module dlatchn(input ENA, D, output reg Q, output QN); -always @(negedge CLK) - Q <= D; +always @* + if (~ENA) Q <= D; assign QN = ~Q; endmodule -module dffsr(input CLK, D, CLEAR, PRESET, output reg Q, output QN); +module dlatchsr(input ENA, D, CLEAR, PRESET, output reg Q, output QN); -always @(posedge CLK, posedge CLEAR, posedge PRESET) - if (CLEAR) - Q <= 0; - else if (PRESET) - Q <= 1; - else - Q <= D; - -assign QN = ~Q; - -endmodule - -module dffe(input CLK, EN, D, output reg Q, output QN); - -always @(negedge CLK) - if (EN) Q <= D; +always @* + if (CLEAR) Q <= 1'b0; + else if (PRESET) Q <= 1'b1; + else if (ENA) Q <= D; assign QN = ~Q; diff --git a/tests/techmap/dlatchlibmap.lib b/tests/techmap/dlatchlibmap.lib index 54a44a296..1e4f0bc99 100644 --- a/tests/techmap/dlatchlibmap.lib +++ b/tests/techmap/dlatchlibmap.lib @@ -1,16 +1,17 @@ library(test) { - /* D-type flip-flop with asynchronous reset and preset */ - cell (dffn) { + /* D-type latch with reset and preset */ + cell (dlatchn) { area : 6; - ff("IQ", "IQN") { - next_state : "D"; - clocked_on : "!CLK"; + latch("IQ", "IQN") { + data_in : "D"; + enable : "!ENA"; } pin(D) { direction : input; } - pin(CLK) { + pin(ENA) { direction : input; + clock : true; } pin(Q) { direction: output; @@ -21,21 +22,22 @@ library(test) { function : "IQN"; } } - cell (dffsr) { + cell (dlatchsr) { area : 6; - ff("IQ", "IQN") { - next_state : "D"; - clocked_on : "CLK"; - clear : "CLEAR"; - preset : "PRESET"; + latch("IQ", "IQN") { + data_in : "D"; + enable : "ENA"; + clear : "CLEAR"; + preset : "PRESET"; clear_preset_var1 : L; clear_preset_var2 : L; } pin(D) { direction : input; } - pin(CLK) { + pin(ENA) { direction : input; + clock : true; } pin(CLEAR) { direction : input; @@ -52,28 +54,4 @@ library(test) { function : "IQN"; } } - cell (dffe) { - area : 6; - ff("IQ", "IQN") { - next_state : "(D EN) | (IQ !EN)"; - clocked_on : "!CLK"; - } - pin(D) { - direction : input; - } - pin(EN) { - direction : input; - } - pin(CLK) { - direction : input; - } - pin(Q) { - direction: output; - function : "IQ"; - } - pin(QN) { - direction: output; - function : "IQN"; - } - } } diff --git a/tests/techmap/dlatchlibmap.ys b/tests/techmap/dlatchlibmap.ys index 87ecc8bc7..fa0ce65be 100644 --- a/tests/techmap/dlatchlibmap.ys +++ b/tests/techmap/dlatchlibmap.ys @@ -1,15 +1,14 @@ read_verilog -icells < Date: Tue, 23 Jun 2026 23:18:12 +0200 Subject: [PATCH 11/16] dfflibmap: updated dlatchlibmap tests so they pass --- tests/techmap/dlatchlibmap.ys | 23 ++++++++++++++--------- tests/techmap/dlatchlibmap_formal.ys | 8 ++------ 2 files changed, 16 insertions(+), 15 deletions(-) diff --git a/tests/techmap/dlatchlibmap.ys b/tests/techmap/dlatchlibmap.ys index fa0ce65be..dd1a943e1 100644 --- a/tests/techmap/dlatchlibmap.ys +++ b/tests/techmap/dlatchlibmap.ys @@ -29,7 +29,7 @@ design -load orig dfflibmap -liberty dlatchlibmap.lib clean -select -assert-count 5 t:$_NOT_ +select -assert-count 4 t:$_NOT_ select -assert-count 1 t:dlatchn select -assert-count 4 t:dlatchsr select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i @@ -37,7 +37,7 @@ select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i design -load orig dfflibmap -prepare -liberty dlatchlibmap.lib -select -assert-count 11 t:$_NOT_ +select -assert-count 9 t:$_NOT_ select -assert-count 1 t:$_DLATCH_N_ select -assert-count 4 t:$_DLATCHSR_PPP_ select -assert-none t:$_DLATCH_N_ t:$_DLATCHSR_PPP_ t:$_NOT_ %% %n t:* %i @@ -45,16 +45,20 @@ select -assert-none t:$_DLATCH_N_ t:$_DLATCHSR_PPP_ t:$_NOT_ %% %n t:* %i design -load orig dfflibmap -map-only -liberty dlatchlibmap.lib -select -assert-count 6 t:$_NOT_ +select -assert-count 5 t:$_NOT_ select -assert-count 0 t:dlatchn select -assert-count 1 t:dlatchsr +select -assert-count 1 t:$_DLATCH_P_ +select -assert-count 1 t:$_DLATCH_PP0_ +select -assert-count 1 t:$_DLATCH_PP1_ +select -assert-count 1 t:$_DLATCHSR_NNN_ design -load orig dfflibmap -prepare -liberty dlatchlibmap.lib dfflibmap -map-only -liberty dlatchlibmap.lib clean -select -assert-count 5 t:$_NOT_ +select -assert-count 4 t:$_NOT_ select -assert-count 1 t:dlatchn select -assert-count 4 t:dlatchsr select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i @@ -64,7 +68,7 @@ dfflibmap -prepare -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatc dfflibmap -map-only -liberty dlatchlibmap_dlatchn.lib -liberty dlatchlibmap_dlatchsr_r.lib clean -select -assert-count 5 t:$_NOT_ +select -assert-count 4 t:$_NOT_ select -assert-count 1 t:dlatchn select -assert-count 4 t:dlatchsr select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i @@ -79,14 +83,15 @@ select -assert-count 5 t:dlatchsr design -load orig dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr clean + # We have one more _NOT_ than with the regular dlatchsr -select -assert-count 6 t:$_NOT_ +select -assert-count 5 t:$_NOT_ select -assert-count 1 t:dlatchn select -assert-count 4 t:dlatchsr_mixedpol # The additional NOT is on latch2. -# Originally, latch2.R is an active high "set". -# dlatchsr_mixedpol has functionally swapped labels due to the next_state inversion, -# so we use its CLEAR port for the "set", +# Originally, latch2.R is an active high "preset". +# dlatchsr_mixedpol has functionally swapped labels due to the data_in inversion, +# so we use its CLEAR port for the "preset", # but we have to invert it because the CLEAR pin is active low. # latch2.CLEAR = !R select -assert-count 1 c:latch2 %x:+[CLEAR] %ci t:$_NOT_ %i diff --git a/tests/techmap/dlatchlibmap_formal.ys b/tests/techmap/dlatchlibmap_formal.ys index 8a6410156..135bfdc1a 100644 --- a/tests/techmap/dlatchlibmap_formal.ys +++ b/tests/techmap/dlatchlibmap_formal.ys @@ -122,10 +122,6 @@ $_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0])); $_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1])); $_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2])); -// TODO: this comment is just a copy from 'dfflibmap_formal.ys' -// Formal checking of directly instantiated DLATCHSR doesn't work at the moment -// likely due to an equiv_induct -set-assumes assume bug #5196 - // no assume when mapping to unset clear_preset_var $_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3])); $_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4])); @@ -199,7 +195,7 @@ read_verilog < Date: Sat, 27 Jun 2026 00:59:03 +0200 Subject: [PATCH 12/16] dfflibmap: collected copies of the same code into a function --- passes/techmap/dfflibmap.cc | 291 ++++++++---------------------------- 1 file changed, 63 insertions(+), 228 deletions(-) diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc index 516043db7..77d4499fa 100644 --- a/passes/techmap/dfflibmap.cc +++ b/passes/techmap/dfflibmap.cc @@ -255,6 +255,65 @@ static bool parse_pin(const LibertyAst *cell, const LibertyAst *attr, std::strin return false; } +void find_better_cell(const LibertyAst *cell, const LibertyAst &storage, bool data_pol, const LibertyAst *&best, double &best_area, int &best_pins, bool &best_noninv, std::map &this_ports, std::map &best_ports) +{ + double area = 0; + const LibertyAst *ar = cell->find("area"); + if (ar != nullptr && !ar->value.empty()) + area = atof(ar->value.c_str()); + + int num_pins = 0; + bool found_output = false; + bool found_noninv_output = false; + for (auto pin : cell->children) + { + if (pin->id != "pin" || pin->args.size() != 1) + continue; + + const LibertyAst *dir = pin->find("direction"); + if (dir == nullptr || dir->value == "internal") + continue; + num_pins++; + + if (dir->value == "input" && this_ports.count(pin->args[0]) == 0) + return; + + const LibertyAst *func = pin->find("function"); + if (dir->value == "output" && func != nullptr) { + std::string value = func->value; + for (size_t pos = value.find_first_of("\" \t"); pos != std::string::npos; pos = value.find_first_of("\" \t")) + value.erase(pos, 1); + if (value == storage.args[0]) { + this_ports[pin->args[0]] = data_pol ? 'Q' : 'q'; + if (data_pol) + found_noninv_output = true; + found_output = true; + } else + if (value == storage.args[1]) { + this_ports[pin->args[0]] = data_pol ? 'q' : 'Q'; + if (!data_pol) + found_noninv_output = true; + found_output = true; + } + } + + if (this_ports.count(pin->args[0]) == 0) + this_ports[pin->args[0]] = 0; + } + + if (!found_output || (best != nullptr && (num_pins > best_pins || (best_noninv && !found_noninv_output)))) + return; + + if (best != nullptr && num_pins == best_pins && area > best_area) + return; + + best = cell; + best_pins = num_pins; + best_area = area; + best_noninv = found_noninv_output; + best_ports.swap(this_ports); +} + static void find_cell_dff(std::vector cells, IdString cell_type, bool clkpol, bool has_reset, bool rstpol, bool rstval, bool has_enable, bool enapol, std::vector &dont_use_cells) { const LibertyAst *best_cell = nullptr; @@ -310,62 +369,7 @@ static void find_cell_dff(std::vector cells, IdString cell_t this_cell_ports[cell_enable_pin] = 'E'; this_cell_ports[cell_next_pin] = 'D'; - double area = 0; - const LibertyAst *ar = cell->find("area"); - if (ar != nullptr && !ar->value.empty()) - area = atof(ar->value.c_str()); - - int num_pins = 0; - bool found_output = false; - bool found_noninv_output = false; - for (auto pin : cell->children) - { - if (pin->id != "pin" || pin->args.size() != 1) - continue; - - const LibertyAst *dir = pin->find("direction"); - if (dir == nullptr || dir->value == "internal") - continue; - num_pins++; - - if (dir->value == "input" && this_cell_ports.count(pin->args[0]) == 0) - goto continue_cell_loop; - - const LibertyAst *func = pin->find("function"); - if (dir->value == "output" && func != nullptr) { - std::string value = func->value; - for (size_t pos = value.find_first_of("\" \t"); pos != std::string::npos; pos = value.find_first_of("\" \t")) - value.erase(pos, 1); - if (value == ff->args[0]) { - this_cell_ports[pin->args[0]] = cell_next_pol ? 'Q' : 'q'; - if (cell_next_pol) - found_noninv_output = true; - found_output = true; - } else - if (value == ff->args[1]) { - this_cell_ports[pin->args[0]] = cell_next_pol ? 'q' : 'Q'; - if (!cell_next_pol) - found_noninv_output = true; - found_output = true; - } - } - - if (this_cell_ports.count(pin->args[0]) == 0) - this_cell_ports[pin->args[0]] = 0; - } - - if (!found_output || (best_cell != nullptr && (num_pins > best_cell_pins || (best_cell_noninv && !found_noninv_output)))) - continue; - - if (best_cell != nullptr && num_pins == best_cell_pins && area > best_cell_area) - continue; - - best_cell = cell; - best_cell_pins = num_pins; - best_cell_area = area; - best_cell_noninv = found_noninv_output; - best_cell_ports.swap(this_cell_ports); - continue_cell_loop:; + find_better_cell(cell, *ff, cell_next_pol, best_cell, best_cell_area, best_cell_pins, best_cell_noninv, this_cell_ports, best_cell_ports); } if (best_cell != nullptr) { @@ -440,64 +444,7 @@ static void find_cell_dffsr(std::vector cells, IdString cell this_cell_ports[cell_enable_pin] = 'E'; this_cell_ports[cell_next_pin] = 'D'; - double area = 0; - const LibertyAst *ar = cell->find("area"); - if (ar != nullptr && !ar->value.empty()) - area = atof(ar->value.c_str()); - - int num_pins = 0; - bool found_output = false; - bool found_noninv_output = false; - for (auto pin : cell->children) - { - if (pin->id != "pin" || pin->args.size() != 1) - continue; - - const LibertyAst *dir = pin->find("direction"); - if (dir == nullptr || dir->value == "internal") - continue; - num_pins++; - - if (dir->value == "input" && this_cell_ports.count(pin->args[0]) == 0) - goto continue_cell_loop; - - const LibertyAst *func = pin->find("function"); - if (dir->value == "output" && func != nullptr) { - std::string value = func->value; - for (size_t pos = value.find_first_of("\" \t"); pos != std::string::npos; pos = value.find_first_of("\" \t")) - value.erase(pos, 1); - if (value == ff->args[0]) { - // next_state negation propagated to output - this_cell_ports[pin->args[0]] = cell_next_pol ? 'Q' : 'q'; - if (cell_next_pol) - found_noninv_output = true; - found_output = true; - } else - if (value == ff->args[1]) { - // next_state negation propagated to output - this_cell_ports[pin->args[0]] = cell_next_pol ? 'q' : 'Q'; - if (!cell_next_pol) - found_noninv_output = true; - found_output = true; - } - } - - if (this_cell_ports.count(pin->args[0]) == 0) - this_cell_ports[pin->args[0]] = 0; - } - - if (!found_output || (best_cell != nullptr && (num_pins > best_cell_pins || (best_cell_noninv && !found_noninv_output)))) - continue; - - if (best_cell != nullptr && num_pins == best_cell_pins && area > best_cell_area) - continue; - - best_cell = cell; - best_cell_pins = num_pins; - best_cell_area = area; - best_cell_noninv = found_noninv_output; - best_cell_ports.swap(this_cell_ports); - continue_cell_loop:; + find_better_cell(cell, *ff, cell_next_pol, best_cell, best_cell_area, best_cell_pins, best_cell_noninv, this_cell_ports, best_cell_ports); } if (best_cell != nullptr) { @@ -561,62 +508,7 @@ static void find_cell_dlatch(std::vector cells, IdString cel this_cell_ports[cell_rst_pin] = 'R'; this_cell_ports[cell_data_pin] = 'D'; - double area = 0; - const LibertyAst *ar = cell->find("area"); - if (ar != nullptr && !ar->value.empty()) - area = atof(ar->value.c_str()); - - int num_pins = 0; - bool found_output = false; - bool found_noninv_output = false; - for (auto pin : cell->children) - { - if (pin->id != "pin" || pin->args.size() != 1) - continue; - - const LibertyAst *dir = pin->find("direction"); - if (dir == nullptr || dir->value == "internal") - continue; - num_pins++; - - if (dir->value == "input" && this_cell_ports.count(pin->args[0]) == 0) - goto continue_cell_loop; - - const LibertyAst *func = pin->find("function"); - if (dir->value == "output" && func != nullptr) { - std::string value = func->value; - for (size_t pos = value.find_first_of("\" \t"); pos != std::string::npos; pos = value.find_first_of("\" \t")) - value.erase(pos, 1); - if (value == latch->args[0]) { - this_cell_ports[pin->args[0]] = cell_data_pol ? 'Q' : 'q'; - if (cell_data_pol) - found_noninv_output = true; - found_output = true; - } else - if (value == latch->args[1]) { - this_cell_ports[pin->args[0]] = cell_data_pol ? 'q' : 'Q'; - if (!cell_data_pol) - found_noninv_output = true; - found_output = true; - } - } - - if (this_cell_ports.count(pin->args[0]) == 0) - this_cell_ports[pin->args[0]] = 0; - } - - if (!found_output || (best_cell != nullptr && (num_pins > best_cell_pins || (best_cell_noninv && !found_noninv_output)))) - continue; - - if (best_cell != nullptr && num_pins == best_cell_pins && area > best_cell_area) - continue; - - best_cell = cell; - best_cell_pins = num_pins; - best_cell_area = area; - best_cell_noninv = found_noninv_output; - best_cell_ports.swap(this_cell_ports); - continue_cell_loop:; + find_better_cell(cell, *latch, cell_data_pol, best_cell, best_cell_area, best_cell_pins, best_cell_noninv, this_cell_ports, best_cell_ports); } if (best_cell != nullptr) { @@ -687,64 +579,7 @@ static void find_cell_dlatchsr(std::vector cells, IdString c this_cell_ports[cell_clr_pin] = 'R'; this_cell_ports[cell_data_pin] = 'D'; - double area = 0; - const LibertyAst *ar = cell->find("area"); - if (ar != nullptr && !ar->value.empty()) - area = atof(ar->value.c_str()); - - int num_pins = 0; - bool found_output = false; - bool found_noninv_output = false; - for (auto pin : cell->children) - { - if (pin->id != "pin" || pin->args.size() != 1) - continue; - - const LibertyAst *dir = pin->find("direction"); - if (dir == nullptr || dir->value == "internal") - continue; - num_pins++; - - if (dir->value == "input" && this_cell_ports.count(pin->args[0]) == 0) - goto continue_cell_loop; - - const LibertyAst *func = pin->find("function"); - if (dir->value == "output" && func != nullptr) { - std::string value = func->value; - for (size_t pos = value.find_first_of("\" \t"); pos != std::string::npos; pos = value.find_first_of("\" \t")) - value.erase(pos, 1); - if (value == latch->args[0]) { - // next_state negation propagated to output - this_cell_ports[pin->args[0]] = cell_data_pol ? 'Q' : 'q'; - if (cell_data_pol) - found_noninv_output = true; - found_output = true; - } else - if (value == latch->args[1]) { - // next_state negation propagated to output - this_cell_ports[pin->args[0]] = cell_data_pol ? 'q' : 'Q'; - if (!cell_data_pol) - found_noninv_output = true; - found_output = true; - } - } - - if (this_cell_ports.count(pin->args[0]) == 0) - this_cell_ports[pin->args[0]] = 0; - } - - if (!found_output || (best_cell != nullptr && (num_pins > best_cell_pins || (best_cell_noninv && !found_noninv_output)))) - continue; - - if (best_cell != nullptr && num_pins == best_cell_pins && area > best_cell_area) - continue; - - best_cell = cell; - best_cell_pins = num_pins; - best_cell_area = area; - best_cell_noninv = found_noninv_output; - best_cell_ports.swap(this_cell_ports); - continue_cell_loop:; + find_better_cell(cell, *latch, cell_data_pol, best_cell, best_cell_area, best_cell_pins, best_cell_noninv, this_cell_ports, best_cell_ports); } if (best_cell != nullptr) { From 6b44f4321e2eddab4fddd296f1dfab6018a11e7b Mon Sep 17 00:00:00 2001 From: Iztok Jeras Date: Sat, 27 Jun 2026 01:27:38 +0200 Subject: [PATCH 13/16] dfflibmap: picking first instead of last cell with smallest area In a standard cell library cells are usually ordered from weakest to strongest. Sometimes the two weakest cells have the same area. Previously the stroner (last) of the two was selected, now the weaker (first is selected). --- passes/techmap/dfflibmap.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc index 77d4499fa..193f45c27 100644 --- a/passes/techmap/dfflibmap.cc +++ b/passes/techmap/dfflibmap.cc @@ -304,7 +304,7 @@ void find_better_cell(const LibertyAst *cell, const LibertyAst &storage, bool da if (!found_output || (best != nullptr && (num_pins > best_pins || (best_noninv && !found_noninv_output)))) return; - if (best != nullptr && num_pins == best_pins && area > best_area) + if (best != nullptr && num_pins == best_pins && area >= best_area) return; best = cell; From 92d4f60977495e8af29273bf6c6f8bef64a98887 Mon Sep 17 00:00:00 2001 From: Iztok Jeras Date: Wed, 15 Jul 2026 05:23:30 +0200 Subject: [PATCH 14/16] dlatchlibmap: added more formal testscases --- tests/techmap/dlatchlibmap.ys | 10 +++ tests/techmap/dlatchlibmap_dlatchsr_h.lib | 34 +++++++++ tests/techmap/dlatchlibmap_dlatchsr_l.lib | 34 +++++++++ .../dlatchlibmap_dlatchsr_mixedpol-sim.v | 10 +++ tests/techmap/dlatchlibmap_formal.ys | 76 +++++++++++++++++++ tests/techmap/dlatchlibmap_proc_formal.ys | 47 +++++++++++- 6 files changed, 209 insertions(+), 2 deletions(-) create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_h.lib create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_l.lib create mode 100644 tests/techmap/dlatchlibmap_dlatchsr_mixedpol-sim.v diff --git a/tests/techmap/dlatchlibmap.ys b/tests/techmap/dlatchlibmap.ys index dd1a943e1..f4ba8dc7d 100644 --- a/tests/techmap/dlatchlibmap.ys +++ b/tests/techmap/dlatchlibmap.ys @@ -25,6 +25,8 @@ equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -prepare -libert dfflibmap -prepare -liberty dlatchlibmap.lib equiv_opt -map dlatchlibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dlatchlibmap.lib +################################################################## + design -load orig dfflibmap -liberty dlatchlibmap.lib clean @@ -73,6 +75,8 @@ select -assert-count 1 t:dlatchn select -assert-count 4 t:dlatchsr select -assert-none t:dlatchn t:dlatchsr t:$_NOT_ %% %n t:* %i +################################################################## + design -load orig dfflibmap -liberty dlatchlibmap.lib -dont_use *latchn clean @@ -80,6 +84,12 @@ clean select -assert-count 0 t:dlatchn select -assert-count 5 t:dlatchsr +################################################################## + +design -load orig +read_liberty -lib dlatchlibmap.lib dlatchlibmap_dlatchsr_mixedpol.lib +equiv_opt -map dlatchlibmap-sim.v -map dlatchlibmap_dlatchsr_mixedpol-sim.v -assert -multiclock dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr + design -load orig dfflibmap -liberty dlatchlibmap.lib -liberty dlatchlibmap_dlatchsr_mixedpol.lib -dont_use dlatchsr clean diff --git a/tests/techmap/dlatchlibmap_dlatchsr_h.lib b/tests/techmap/dlatchlibmap_dlatchsr_h.lib new file mode 100644 index 000000000..c9582cc96 --- /dev/null +++ b/tests/techmap/dlatchlibmap_dlatchsr_h.lib @@ -0,0 +1,34 @@ +library(test) { + cell (dlatchsr) { + area : 6; + latch("IQ", "IQN") { + data_in : "D"; + enable : "ENA"; + clear : "CLEAR"; + preset : "PRESET"; + clear_preset_var1 : H; + clear_preset_var2 : H; + } + pin(D) { + direction : input; + } + pin(ENA) { + direction : input; + clock : true; + } + pin(CLEAR) { + direction : input; + } + pin(PRESET) { + direction : input; + } + pin(Q) { + direction: output; + function : "IQ"; + } + pin(QN) { + direction: output; + function : "IQN"; + } + } +} diff --git a/tests/techmap/dlatchlibmap_dlatchsr_l.lib b/tests/techmap/dlatchlibmap_dlatchsr_l.lib new file mode 100644 index 000000000..7d438f612 --- /dev/null +++ b/tests/techmap/dlatchlibmap_dlatchsr_l.lib @@ -0,0 +1,34 @@ +library(test) { + cell (dlatchsr) { + area : 6; + latch("IQ", "IQN") { + data_in : "D"; + enable : "ENA"; + clear : "CLEAR"; + preset : "PRESET"; + clear_preset_var1 : L; + clear_preset_var2 : L; + } + pin(D) { + direction : input; + } + pin(ENA) { + direction : input; + clock : true; + } + pin(CLEAR) { + direction : input; + } + pin(PRESET) { + direction : input; + } + pin(Q) { + direction: output; + function : "IQ"; + } + pin(QN) { + direction: output; + function : "IQN"; + } + } +} diff --git a/tests/techmap/dlatchlibmap_dlatchsr_mixedpol-sim.v b/tests/techmap/dlatchlibmap_dlatchsr_mixedpol-sim.v new file mode 100644 index 000000000..0be00d357 --- /dev/null +++ b/tests/techmap/dlatchlibmap_dlatchsr_mixedpol-sim.v @@ -0,0 +1,10 @@ +module dlatchsr_mixedpol(input ENA, D, CLEAR, PRESET, output reg Q, output QN); + + always @* + if (PRESET) Q <= 1'b1; + else if (~CLEAR) Q <= 1'b0; + else if (ENA) Q <= ~D; + + assign QN = ~Q; + +endmodule diff --git a/tests/techmap/dlatchlibmap_formal.ys b/tests/techmap/dlatchlibmap_formal.ys index 135bfdc1a..7a0ca60c3 100644 --- a/tests/techmap/dlatchlibmap_formal.ys +++ b/tests/techmap/dlatchlibmap_formal.ys @@ -84,6 +84,82 @@ $_DLATCH_P_ latch0 (.E(E), .D(D), .Q(Q[0])); $_DLATCH_PP0_ latch1 (.E(E), .D(D), .R(R), .Q(Q[1])); $_DLATCH_PP1_ latch2 (.E(E), .D(D), .R(R), .Q(Q[2])); +assume property (~R || ~S); +$_DLATCHSR_PPP_ latch3 (.E(E), .D(D), .R( R), .S( S), .Q(Q[3])); +$_DLATCHSR_NNN_ latch4 (.E(E), .D(D), .R(~R), .S(~S), .Q(Q[4])); + +assign Q[9:5] = ~Q[4:0]; + +endmodule + +EOT + +proc +opt +read_liberty dlatchlibmap_dlatchsr_l.lib + +copy top top_unmapped +dfflibmap -liberty dlatchlibmap_dlatchsr_l.lib top + +clk2fflogic +flatten +opt_clean -purge +miter -equiv -make_assert -flatten top_unmapped top miter +hierarchy -top miter +# Prove that this is equivalent with the assumption +sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter +# Prove that this is NOT equivalent WITHOUT the assumption +sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter + +################################################################## + +design -reset +read_verilog -sv -icells < Date: Wed, 15 Jul 2026 06:08:54 +0200 Subject: [PATCH 15/16] dfflibmap: extended tests with same testcases as dlatchmap --- tests/techmap/dfflibmap.ys | 11 +++ tests/techmap/dfflibmap_dffsr_h.lib | 34 ++++++++ tests/techmap/dfflibmap_dffsr_l.lib | 34 ++++++++ tests/techmap/dfflibmap_dffsr_mixedpol-sim.v | 10 +++ tests/techmap/dfflibmap_dffsr_r.lib | 1 + tests/techmap/dfflibmap_dffsr_s.lib | 1 + tests/techmap/dfflibmap_dffsr_x.lib | 1 + tests/techmap/dfflibmap_formal.ys | 80 +++++++++++++++++++ tests/techmap/dfflibmap_proc_formal.ys | 83 ++++++++++++++------ 9 files changed, 229 insertions(+), 26 deletions(-) create mode 100644 tests/techmap/dfflibmap_dffsr_h.lib create mode 100644 tests/techmap/dfflibmap_dffsr_l.lib create mode 100644 tests/techmap/dfflibmap_dffsr_mixedpol-sim.v diff --git a/tests/techmap/dfflibmap.ys b/tests/techmap/dfflibmap.ys index 87ecc8bc7..499907d10 100644 --- a/tests/techmap/dfflibmap.ys +++ b/tests/techmap/dfflibmap.ys @@ -26,6 +26,8 @@ equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -prepare -liberty d dfflibmap -prepare -liberty dfflibmap.lib equiv_opt -map dfflibmap-sim.v -assert -multiclock dfflibmap -map-only -liberty dfflibmap.lib +################################################################## + design -load orig dfflibmap -liberty dfflibmap.lib clean @@ -74,6 +76,8 @@ select -assert-count 1 t:dffe select -assert-count 4 t:dffsr select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i +################################################################## + design -load orig dfflibmap -liberty dfflibmap.lib -dont_use *ffn clean @@ -82,6 +86,13 @@ select -assert-count 0 t:dffn select -assert-count 5 t:dffsr select -assert-count 1 t:dffe +################################################################## + +design -load orig +read_liberty -lib dfflibmap.lib dfflibmap_dffsr_mixedpol.lib +stat +equiv_opt -map dfflibmap-sim.v -map dfflibmap_dffsr_mixedpol-sim.v -assert -multiclock dfflibmap -liberty dfflibmap.lib -liberty dfflibmap_dffsr_mixedpol.lib -dont_use dffsr + design -load orig dfflibmap -liberty dfflibmap.lib -liberty dfflibmap_dffsr_mixedpol.lib -dont_use dffsr clean diff --git a/tests/techmap/dfflibmap_dffsr_h.lib b/tests/techmap/dfflibmap_dffsr_h.lib new file mode 100644 index 000000000..a49f23a35 --- /dev/null +++ b/tests/techmap/dfflibmap_dffsr_h.lib @@ -0,0 +1,34 @@ +library(test) { + cell (dffsr) { + area : 6; + ff("IQ", "IQN") { + next_state : "D"; + clocked_on : "CLK"; + clear : "CLEAR"; + preset : "PRESET"; + clear_preset_var1 : H; + clear_preset_var2 : H; + } + pin(D) { + direction : input; + } + pin(CLK) { + direction : input; + clock : true; + } + pin(CLEAR) { + direction : input; + } + pin(PRESET) { + direction : input; + } + pin(Q) { + direction: output; + function : "IQ"; + } + pin(QN) { + direction: output; + function : "IQN"; + } + } +} diff --git a/tests/techmap/dfflibmap_dffsr_l.lib b/tests/techmap/dfflibmap_dffsr_l.lib new file mode 100644 index 000000000..10c3480a0 --- /dev/null +++ b/tests/techmap/dfflibmap_dffsr_l.lib @@ -0,0 +1,34 @@ +library(test) { + cell (dffsr) { + area : 6; + ff("IQ", "IQN") { + next_state : "D"; + clocked_on : "CLK"; + clear : "CLEAR"; + preset : "PRESET"; + clear_preset_var1 : L; + clear_preset_var2 : L; + } + pin(D) { + direction : input; + } + pin(CLK) { + direction : input; + clock : true; + } + pin(CLEAR) { + direction : input; + } + pin(PRESET) { + direction : input; + } + pin(Q) { + direction: output; + function : "IQ"; + } + pin(QN) { + direction: output; + function : "IQN"; + } + } +} diff --git a/tests/techmap/dfflibmap_dffsr_mixedpol-sim.v b/tests/techmap/dfflibmap_dffsr_mixedpol-sim.v new file mode 100644 index 000000000..9babda0b5 --- /dev/null +++ b/tests/techmap/dfflibmap_dffsr_mixedpol-sim.v @@ -0,0 +1,10 @@ +module dffsr_mixedpol(input CLK, D, CLEAR, PRESET, output reg Q, output QN); + + always @(posedge CLK, negedge CLEAR, posedge PRESET) + if (PRESET) Q <= 1'b1; + else if (~CLEAR) Q <= 1'b0; + else Q <= ~D; + + assign QN = ~Q; + +endmodule diff --git a/tests/techmap/dfflibmap_dffsr_r.lib b/tests/techmap/dfflibmap_dffsr_r.lib index f36e200a0..433748375 100644 --- a/tests/techmap/dfflibmap_dffsr_r.lib +++ b/tests/techmap/dfflibmap_dffsr_r.lib @@ -14,6 +14,7 @@ library(test) { } pin(CLK) { direction : input; + clock : true; } pin(CLEAR) { direction : input; diff --git a/tests/techmap/dfflibmap_dffsr_s.lib b/tests/techmap/dfflibmap_dffsr_s.lib index cf930f3c7..da9919286 100644 --- a/tests/techmap/dfflibmap_dffsr_s.lib +++ b/tests/techmap/dfflibmap_dffsr_s.lib @@ -14,6 +14,7 @@ library(test) { } pin(CLK) { direction : input; + clock : true; } pin(CLEAR) { direction : input; diff --git a/tests/techmap/dfflibmap_dffsr_x.lib b/tests/techmap/dfflibmap_dffsr_x.lib index 91d702412..3c7f625c3 100644 --- a/tests/techmap/dfflibmap_dffsr_x.lib +++ b/tests/techmap/dfflibmap_dffsr_x.lib @@ -14,6 +14,7 @@ library(test) { } pin(CLK) { direction : input; + clock : true; } pin(CLEAR) { direction : input; diff --git a/tests/techmap/dfflibmap_formal.ys b/tests/techmap/dfflibmap_formal.ys index afa2c4d9d..7f44c0d23 100644 --- a/tests/techmap/dfflibmap_formal.ys +++ b/tests/techmap/dfflibmap_formal.ys @@ -88,6 +88,86 @@ $_DFF_P_ ff0 (.C(C), .D(D), .Q(Q[0])); $_DFF_PP0_ ff1 (.C(C), .D(D), .R(R), .Q(Q[1])); $_DFF_PP1_ ff2 (.C(C), .D(D), .R(R), .Q(Q[2])); +assume property (~R || ~S); +$_DFFSR_PPP_ ff3 (.C(C), .D(D), .R(R), .S(S), .Q(Q[3])); +$_DFFSR_NNN_ ff4 (.C(C), .D(D), .R(~R), .S(~S), .Q(Q[4])); + +$_DFFE_PP_ ff5 (.C(C), .D(D), .E(E), .Q(Q[5])); + +assign Q[11:6] = ~Q[5:0]; + +endmodule + +EOT + +proc +opt +read_liberty dfflibmap_dffsr_l.lib + +copy top top_unmapped +dfflibmap -liberty dfflibmap_dffsr_l.lib top + +clk2fflogic +flatten +opt_clean -purge +miter -equiv -make_assert -flatten top_unmapped top miter +hierarchy -top miter +# Prove that this is equivalent with the assumption +sat -verify -prove-asserts -set-assumes -enable_undef -set-init-undef -show-public -seq 3 miter +# Prove that this is NOT equivalent WITHOUT the assumption +sat -falsify -prove-asserts -enable_undef -set-init-undef -seq 3 miter + +################################################################## + +design -reset +read_verilog -sv -icells < Date: Wed, 15 Jul 2026 06:19:52 +0200 Subject: [PATCH 16/16] dfflibmap: added warning about clear/preset priority mismatch --- passes/techmap/dfflibmap.cc | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc index 193f45c27..53969546c 100644 --- a/passes/techmap/dfflibmap.cc +++ b/passes/techmap/dfflibmap.cc @@ -679,6 +679,10 @@ struct DfflibmapPass : public Pass { log("Since inverters are added for each technology cell, an opt_merge pass\n"); log("would reduce the redundancy.\n"); log("\n"); + log("WARNING: This pass does not handle asynchronous clear/preset priority,\n"); + log("if there is a mismatch between the priority in RTL and the cell in the technology library.\n"); + log("If the RTL is able to drive both simultaneously, this will result in an equivalence mismatch.\n"); + log("\n"); log("When called with -prepare, this command will convert the internal FF/LATCH cells\n"); log("to the internal cell types that best match the cells found in the given\n"); log("liberty file, but won't actually map them to the target cells.\n");