From 8ebba8a35f0a5dbf3a044ab84575edfc46c99d77 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Wed, 12 Oct 2016 01:18:39 +0200 Subject: [PATCH] Added $ff and $_FF_ cell types --- backends/blif/blif.cc | 6 ++++++ backends/smt2/smt2.cc | 10 +++++----- frontends/blif/blifparse.cc | 12 ++++++++---- kernel/celltypes.h | 3 +++ kernel/rtlil.cc | 25 ++++++++++++++++++++++++ kernel/rtlil.h | 2 ++ kernel/satgen.h | 2 +- manual/CHAPTER_CellLib.tex | 4 ++++ passes/sat/miter.cc | 38 ++++++++++++++++++++++++++++++------- passes/techmap/simplemap.cc | 20 ++++++++++++++++++- techlibs/common/simlib.v | 13 +++++++++++++ techlibs/common/techmap.v | 2 +- 12 files changed, 118 insertions(+), 19 deletions(-) diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc index 6a379e67f..0dc17c92a 100644 --- a/backends/blif/blif.cc +++ b/backends/blif/blif.cc @@ -315,6 +315,12 @@ struct BlifDumper continue; } + if (!config->icells_mode && cell->type == "$_FF_") { + f << stringf(".latch %s %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")), + cstr_init(cell->getPort("\\Q"))); + continue; + } + if (!config->icells_mode && cell->type == "$_DFF_N_") { f << stringf(".latch %s %s fe %s%s\n", cstr(cell->getPort("\\D")), cstr(cell->getPort("\\Q")), cstr(cell->getPort("\\C")), cstr_init(cell->getPort("\\Q"))); diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 9a25f3a23..487f5befb 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -379,7 +379,7 @@ struct Smt2Worker return; } - if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_") + if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_")) { registers.insert(cell); decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) Bool) ; %s\n", @@ -407,7 +407,7 @@ struct Smt2Worker if (bvmode) { - if (cell->type == "$dff") + if (cell->type.in("$ff", "$dff")) { registers.insert(cell); decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n", @@ -596,7 +596,7 @@ struct Smt2Worker pool reg_bits; for (auto cell : module->cells()) - if (cell->type.in("$_DFF_P_", "$_DFF_N_", "$dff")) { + if (cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_P_", "$_DFF_N_")) { // not using sigmap -- we want the net directly at the dff output for (auto bit : cell->getPort("\\Q")) reg_bits.insert(bit); @@ -674,14 +674,14 @@ struct Smt2Worker for (auto cell : this_regs) { - if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_") + if (cell->type.in("$_FF_", "$_DFF_P_", "$_DFF_N_")) { std::string expr_d = get_bool(cell->getPort("\\D")); std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state"); trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell), log_signal(cell->getPort("\\Q")))); } - if (cell->type == "$dff") + if (cell->type.in("$ff", "$dff")) { std::string expr_d = get_bv(cell->getPort("\\D")); std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state"); diff --git a/frontends/blif/blifparse.cc b/frontends/blif/blifparse.cc index 3717a1e5e..f154f7c04 100644 --- a/frontends/blif/blifparse.cc +++ b/frontends/blif/blifparse.cc @@ -256,9 +256,13 @@ void parse_blif(RTLIL::Design *design, std::istream &f, std::string dff_name, bo cell = module->addDlatch(NEW_ID, blif_wire(clock), blif_wire(d), blif_wire(q), false); else { no_latch_clock: - cell = module->addCell(NEW_ID, dff_name); - cell->setPort("\\D", blif_wire(d)); - cell->setPort("\\Q", blif_wire(q)); + if (dff_name.empty()) { + cell = module->addFf(NEW_ID, blif_wire(d), blif_wire(q)); + } else { + cell = module->addCell(NEW_ID, dff_name); + cell->setPort("\\D", blif_wire(d)); + cell->setPort("\\Q", blif_wire(q)); + } } obj_attributes = &cell->attributes; @@ -477,7 +481,7 @@ struct BlifFrontend : public Frontend { } extra_args(f, filename, args, argidx); - parse_blif(design, *f, "\\DFF", true, sop_mode); + parse_blif(design, *f, "", true, sop_mode); } } BlifFrontend; diff --git a/kernel/celltypes.h b/kernel/celltypes.h index 900c12d01..8e3f86f69 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -130,6 +130,7 @@ struct CellTypes IdString CTRL_IN = "\\CTRL_IN", CTRL_OUT = "\\CTRL_OUT"; setup_type("$sr", {SET, CLR}, {Q}); + setup_type("$ff", {D}, {Q}); setup_type("$dff", {CLK, D}, {Q}); setup_type("$dffe", {CLK, EN, D}, {Q}); setup_type("$dffsr", {CLK, SET, CLR, D}, {Q}); @@ -184,6 +185,8 @@ struct CellTypes for (auto c2 : list_np) setup_type(stringf("$_SR_%c%c_", c1, c2), {S, R}, {Q}); + setup_type("$_FF_", {D}, {Q}); + for (auto c1 : list_np) setup_type(stringf("$_DFF_%c_", c1), {C, D}, {Q}); diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index 32efe4f0d..b0cda67b4 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -866,6 +866,13 @@ namespace { return; } + if (cell->type == "$ff") { + port("\\D", param("\\WIDTH")); + port("\\Q", param("\\WIDTH")); + check_expected(); + return; + } + if (cell->type == "$dff") { param_bool("\\CLK_POLARITY"); port("\\CLK", 1); @@ -1069,6 +1076,7 @@ namespace { if (cell->type == "$_SR_PN_") { check_gate("SRQ"); return; } if (cell->type == "$_SR_PP_") { check_gate("SRQ"); return; } + if (cell->type == "$_FF_") { check_gate("DQ"); return; } if (cell->type == "$_DFF_N_") { check_gate("DQC"); return; } if (cell->type == "$_DFF_P_") { check_gate("DQC"); return; } @@ -1830,6 +1838,15 @@ RTLIL::Cell* RTLIL::Module::addSr(RTLIL::IdString name, RTLIL::SigSpec sig_set, return cell; } +RTLIL::Cell* RTLIL::Module::addFf(RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q) +{ + RTLIL::Cell *cell = addCell(name, "$ff"); + cell->parameters["\\WIDTH"] = sig_q.size(); + cell->setPort("\\D", sig_d); + cell->setPort("\\Q", sig_q); + return cell; +} + RTLIL::Cell* RTLIL::Module::addDff(RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity) { RTLIL::Cell *cell = addCell(name, "$dff"); @@ -1912,6 +1929,14 @@ RTLIL::Cell* RTLIL::Module::addDlatchsr(RTLIL::IdString name, RTLIL::SigSpec sig return cell; } +RTLIL::Cell* RTLIL::Module::addFfGate(RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q) +{ + RTLIL::Cell *cell = addCell(name, "$_FF_"); + cell->setPort("\\D", sig_d); + cell->setPort("\\Q", sig_q); + return cell; +} + RTLIL::Cell* RTLIL::Module::addDffGate(RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity) { RTLIL::Cell *cell = addCell(name, stringf("$_DFF_%c_", clk_polarity ? 'P' : 'N')); diff --git a/kernel/rtlil.h b/kernel/rtlil.h index a426e0bdd..058f6acf4 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -1008,6 +1008,7 @@ public: RTLIL::Cell* addEquiv (RTLIL::IdString name, RTLIL::SigSpec sig_a, RTLIL::SigSpec sig_b, RTLIL::SigSpec sig_y); RTLIL::Cell* addSr (RTLIL::IdString name, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, RTLIL::SigSpec sig_q, bool set_polarity = true, bool clr_polarity = true); + RTLIL::Cell* addFf (RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q); RTLIL::Cell* addDff (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true); RTLIL::Cell* addDffe (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_en, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true, bool en_polarity = true); RTLIL::Cell* addDffsr (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, @@ -1032,6 +1033,7 @@ public: RTLIL::Cell* addAoi4Gate (RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d, RTLIL::SigBit sig_y); RTLIL::Cell* addOai4Gate (RTLIL::IdString name, RTLIL::SigBit sig_a, RTLIL::SigBit sig_b, RTLIL::SigBit sig_c, RTLIL::SigBit sig_d, RTLIL::SigBit sig_y); + RTLIL::Cell* addFfGate (RTLIL::IdString name, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q); RTLIL::Cell* addDffGate (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true); RTLIL::Cell* addDffeGate (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_en, RTLIL::SigSpec sig_d, RTLIL::SigSpec sig_q, bool clk_polarity = true, bool en_polarity = true); RTLIL::Cell* addDffsrGate (RTLIL::IdString name, RTLIL::SigSpec sig_clk, RTLIL::SigSpec sig_set, RTLIL::SigSpec sig_clr, diff --git a/kernel/satgen.h b/kernel/satgen.h index 0a65b490c..792bb3ed7 100644 --- a/kernel/satgen.h +++ b/kernel/satgen.h @@ -1293,7 +1293,7 @@ struct SatGen return true; } - if (timestep > 0 && (cell->type == "$dff" || cell->type == "$_DFF_N_" || cell->type == "$_DFF_P_")) + if (timestep > 0 && cell->type.in("$ff", "$dff", "$_FF_", "$_DFF_N_", "$_DFF_P_")) { if (timestep == 1) { diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex index bd73ae23c..7778fe8fd 100644 --- a/manual/CHAPTER_CellLib.tex +++ b/manual/CHAPTER_CellLib.tex @@ -436,6 +436,10 @@ Add information about {\tt \$lut} and {\tt \$sop} cells. Add information about {\tt \$alu}, {\tt \$macc}, {\tt \$fa}, and {\tt \$lcu} cells. \end{fixme} +\begin{fixme} +Add information about {\tt \$ff} and {\tt \$\_FF\_} cells. +\end{fixme} + \begin{fixme} Add information about {\tt \$dffe}, {\tt \$dffsr}, {\tt \$dlatch}, and {\tt \$dlatchsr} cells. \end{fixme} diff --git a/passes/sat/miter.cc b/passes/sat/miter.cc index 4854e19bf..341a6bac8 100644 --- a/passes/sat/miter.cc +++ b/passes/sat/miter.cc @@ -312,18 +312,42 @@ void create_miter_assert(struct Pass *that, std::vector args, RTLIL log_pop(); } - SigSpec or_signals; + SigSpec assert_signals, assume_signals; vector cell_list = module->cells(); - for (auto cell : cell_list) { + for (auto cell : cell_list) + { + if (!cell->type.in("$assert", "$assume")) + continue; + + SigBit is_active = module->Nex(NEW_ID, cell->getPort("\\A"), State::S1); + SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort("\\EN"), State::S1); + if (cell->type == "$assert") { - SigBit is_active = module->Nex(NEW_ID, cell->getPort("\\A"), State::S1); - SigBit is_enabled = module->Eqx(NEW_ID, cell->getPort("\\EN"), State::S1); - or_signals.append(module->And(NEW_ID, is_active, is_enabled)); - module->remove(cell); + assert_signals.append(module->And(NEW_ID, is_active, is_enabled)); + } else { + assume_signals.append(module->And(NEW_ID, is_active, is_enabled)); } + + module->remove(cell); } - module->addReduceOr(NEW_ID, or_signals, trigger); + if (assume_signals.empty()) + { + module->addReduceOr(NEW_ID, assert_signals, trigger); + } + else + { + Wire *assume_q = module->addWire(NEW_ID); + assume_q->attributes["\\init"] = State::S1; + assume_signals.append(assume_q); + + SigSpec assume_nok = module->ReduceOr(NEW_ID, assume_signals); + SigSpec assume_ok = module->Not(NEW_ID, assume_nok); + module->addFf(NEW_ID, assume_ok, assume_q); + + SigSpec assert_fail = module->ReduceOr(NEW_ID, assert_signals); + module->addAnd(NEW_ID, assert_fail, assume_ok, trigger); + } if (flag_flatten) { log_push(); diff --git a/passes/techmap/simplemap.cc b/passes/techmap/simplemap.cc index 0fb647344..c6b932bdc 100644 --- a/passes/techmap/simplemap.cc +++ b/passes/techmap/simplemap.cc @@ -388,6 +388,23 @@ void simplemap_sr(RTLIL::Module *module, RTLIL::Cell *cell) } } +void simplemap_ff(RTLIL::Module *module, RTLIL::Cell *cell) +{ + int width = cell->parameters.at("\\WIDTH").as_int(); + + RTLIL::SigSpec sig_d = cell->getPort("\\D"); + RTLIL::SigSpec sig_q = cell->getPort("\\Q"); + + std::string gate_type = "$_FF_"; + + for (int i = 0; i < width; i++) { + RTLIL::Cell *gate = module->addCell(NEW_ID, gate_type); + gate->add_strpool_attribute("\\src", cell->get_strpool_attribute("\\src")); + gate->setPort("\\D", sig_d[i]); + gate->setPort("\\Q", sig_q[i]); + } +} + void simplemap_dff(RTLIL::Module *module, RTLIL::Cell *cell) { int width = cell->parameters.at("\\WIDTH").as_int(); @@ -532,6 +549,7 @@ void simplemap_get_mappers(std::map args, RTLIL::Design *design) diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v index 922a47cab..db818269b 100644 --- a/techlibs/common/simlib.v +++ b/techlibs/common/simlib.v @@ -1383,6 +1383,19 @@ endmodule `endif // -------------------------------------------------------- +module \$ff (D, Q); + +parameter WIDTH = 0; + +input [WIDTH-1:0] D; +output [WIDTH-1:0] Q; + +assign D = Q; + +endmodule + +// -------------------------------------------------------- + module \$dff (CLK, D, Q); parameter WIDTH = 0; diff --git a/techlibs/common/techmap.v b/techlibs/common/techmap.v index 90c4ed7eb..d7ec3947e 100644 --- a/techlibs/common/techmap.v +++ b/techlibs/common/techmap.v @@ -64,7 +64,7 @@ module _90_simplemap_various; endmodule (* techmap_simplemap *) -(* techmap_celltype = "$sr $dff $dffe $adff $dffsr $dlatch" *) +(* techmap_celltype = "$sr $ff $dff $dffe $adff $dffsr $dlatch" *) module _90_simplemap_registers; endmodule -- 2.30.2