diff --git a/docs/source/cell/gate_reg_ff.rst b/docs/source/cell/gate_reg_ff.rst index 2a31a3f09..2689c9def 100644 --- a/docs/source/cell/gate_reg_ff.rst +++ b/docs/source/cell/gate_reg_ff.rst @@ -154,6 +154,10 @@ to the following Verilog code template, where ``RST_EDGE`` is ``posedge`` if ``RST_LVL`` if ``1``, ``negedge`` otherwise, and ``SET_EDGE`` is ``posedge`` if ``SET_LVL`` if ``1``, ``negedge`` otherwise. +When both set and reset are active, the state and output is undefined. The Verilog +code model does not correspond to this due to limitations +of synthesizable Verilog. + .. code-block:: verilog :force: @@ -187,6 +191,10 @@ types relate to the following Verilog code template, where ``RST_EDGE`` is ``posedge`` if ``RST_LVL`` if ``1``, ``negedge`` otherwise, and ``SET_EDGE`` is ``posedge`` if ``SET_LVL`` if ``1``, ``negedge`` otherwise. +When both set and reset are active, the state and output is undefined. The Verilog +code model does not correspond to this due to limitations +of synthesizable Verilog. + .. code-block:: verilog :force: diff --git a/docs/source/cell/word_reg.rst b/docs/source/cell/word_reg.rst index 25c82b8e6..c5b369b33 100644 --- a/docs/source/cell/word_reg.rst +++ b/docs/source/cell/word_reg.rst @@ -78,6 +78,7 @@ D-type flip-flops with asynchronous set and reset are represented by `$dffsr` cells. As the `$dff` cells they have ``CLK``, ``D`` and ``Q`` ports. In addition they also have multi-bit ``SET`` and ``CLR`` input ports and the corresponding polarity parameters, like `$sr` cells. +When both set and reset are active, the state and output is undefined. D-type flip-flops with enable are represented by `$dffe`, `$adffe`, `$aldffe`, `$dffsre`, `$sdffe`, and `$sdffce` cells, which are enhanced variants of `$dff`, diff --git a/frontends/liberty/liberty.cc b/frontends/liberty/liberty.cc index 0aa1cee09..a006ae649 100644 --- a/frontends/liberty/liberty.cc +++ b/frontends/liberty/liberty.cc @@ -20,6 +20,7 @@ #include "passes/techmap/libparse.h" #include "kernel/register.h" #include "kernel/log.h" +#include YOSYS_NAMESPACE_BEGIN @@ -210,7 +211,10 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node) auto [iq_sig, iqn_sig] = find_latch_ff_wires(module, node); RTLIL::SigSpec clk_sig, data_sig, clear_sig, preset_sig; bool clk_polarity = true, clear_polarity = true, preset_polarity = true; + const std::string name = RTLIL::unescape_id(module->name); + std::optional clear_preset_var1; + std::optional clear_preset_var2; for (auto child : node->children) { if (child->id == "clocked_on") clk_sig = parse_func_expr(module, child->value.c_str()); @@ -220,10 +224,18 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node) 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 FF cell %s\n", child->value, name); + *var = child->value[0]; + } + } if (clk_sig.size() == 0 || data_sig.size() == 0) - log_error("FF cell %s has no next_state and/or clocked_on attribute.\n", RTLIL::unescape_id(module->name)); + log_error("FF cell %s has no next_state and/or clocked_on attribute.\n", name); for (bool rerun_invert_rollback = true; rerun_invert_rollback;) { @@ -248,36 +260,64 @@ static void create_ff(RTLIL::Module *module, const LibertyAst *node) } } - RTLIL::Cell *cell = module->addCell(NEW_ID, ID($_NOT_)); - cell->setPort(ID::A, iq_sig); - cell->setPort(ID::Y, iqn_sig); + 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); + } - cell = module->addCell(NEW_ID, ""); - cell->setPort(ID::D, data_sig); - cell->setPort(ID::Q, iq_sig); - cell->setPort(ID::C, clk_sig); + RTLIL::Cell* cell = module->addCell(NEW_ID, ""); + cell->setPort(ID::D, data_sig); + cell->setPort(ID::Q, q_sig); + cell->setPort(ID::C, clk_sig); - if (clear_sig.size() == 0 && preset_sig.size() == 0) { - cell->type = stringf("$_DFF_%c_", clk_polarity ? 'P' : 'N'); + if (clear_sig.size() == 0 && preset_sig.size() == 0) { + cell->type = stringf("$_DFF_%c_", clk_polarity ? 'P' : 'N'); + } + + if (clear_sig.size() == 1 && preset_sig.size() == 0) { + cell->type = stringf("$_DFF_%c%c0_", clk_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N'); + cell->setPort(ID::R, clear_sig); + } + + if (clear_sig.size() == 0 && preset_sig.size() == 1) { + cell->type = stringf("$_DFF_%c%c1_", clk_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("$_DFFSR_%c%c%c_", clk_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("FF 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()); } - - if (clear_sig.size() == 1 && preset_sig.size() == 0) { - cell->type = stringf("$_DFF_%c%c0_", clk_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N'); - cell->setPort(ID::R, clear_sig); - } - - if (clear_sig.size() == 0 && preset_sig.size() == 1) { - cell->type = stringf("$_DFF_%c%c1_", clk_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("$_DFFSR_%c%c%c_", clk_polarity ? 'P' : 'N', preset_polarity ? 'P' : 'N', clear_polarity ? 'P' : 'N'); - cell->setPort(ID::S, preset_sig); - cell->setPort(ID::R, clear_sig); - } - - log_assert(!cell->type.empty()); } static bool create_latch(RTLIL::Module *module, const LibertyAst *node, bool flag_ignore_miss_data_latch) @@ -797,3 +837,4 @@ skip_cell:; YOSYS_NAMESPACE_END + diff --git a/passes/sat/async2sync.cc b/passes/sat/async2sync.cc index eb3b154b2..086dd5278 100644 --- a/passes/sat/async2sync.cc +++ b/passes/sat/async2sync.cc @@ -157,6 +157,7 @@ struct Async2syncPass : public Pass { SigSpec sig_set = ff.sig_set; SigSpec sig_clr = ff.sig_clr; + SigSpec sig_clr_inv = ff.sig_clr; if (!ff.pol_set) { if (!ff.is_fine) @@ -166,24 +167,42 @@ struct Async2syncPass : public Pass { } if (ff.pol_clr) { + if (!ff.is_fine) + sig_clr_inv = module->Not(NEW_ID, sig_clr); + else + sig_clr_inv = module->NotGate(NEW_ID, sig_clr); + } else { if (!ff.is_fine) sig_clr = module->Not(NEW_ID, sig_clr); else sig_clr = module->NotGate(NEW_ID, sig_clr); } + // At this point, sig_set and sig_clr are now unconditionally + // active-high, and sig_clr_inv is inverted sig_clr + + SigSpec set_and_clr; + if (!ff.is_fine) + set_and_clr = module->And(NEW_ID, sig_set, sig_clr); + else + set_and_clr = module->AndGate(NEW_ID, sig_set, sig_clr); + if (!ff.is_fine) { SigSpec tmp = module->Or(NEW_ID, ff.sig_d, sig_set); - module->addAnd(NEW_ID, tmp, sig_clr, new_d); + tmp = module->And(NEW_ID, tmp, sig_clr_inv); + module->addBwmux(NEW_ID, tmp, Const(State::Sx, ff.width), set_and_clr, new_d); tmp = module->Or(NEW_ID, new_q, sig_set); - module->addAnd(NEW_ID, tmp, sig_clr, ff.sig_q); + tmp = module->And(NEW_ID, tmp, sig_clr_inv); + module->addBwmux(NEW_ID, tmp, Const(State::Sx, ff.width), set_and_clr, ff.sig_q); } else { SigSpec tmp = module->OrGate(NEW_ID, ff.sig_d, sig_set); - module->addAndGate(NEW_ID, tmp, sig_clr, new_d); + tmp = module->AndGate(NEW_ID, tmp, sig_clr_inv); + module->addMuxGate(NEW_ID, tmp, State::Sx, set_and_clr, new_d); tmp = module->OrGate(NEW_ID, new_q, sig_set); - module->addAndGate(NEW_ID, tmp, sig_clr, ff.sig_q); + tmp = module->AndGate(NEW_ID, tmp, sig_clr_inv); + module->addMuxGate(NEW_ID, tmp, State::Sx, set_and_clr, ff.sig_q); } ff.sig_d = new_d; diff --git a/passes/sat/clk2fflogic.cc b/passes/sat/clk2fflogic.cc index dd94dd0d7..b75c8aab1 100644 --- a/passes/sat/clk2fflogic.cc +++ b/passes/sat/clk2fflogic.cc @@ -123,10 +123,14 @@ struct Clk2fflogicPass : public Pass { return module->Mux(NEW_ID, a, b, s); } SigSpec bitwise_sr(Module *module, SigSpec a, SigSpec s, SigSpec r, bool is_fine) { - if (is_fine) - return module->AndGate(NEW_ID, module->OrGate(NEW_ID, a, s), module->NotGate(NEW_ID, r)); - else - return module->And(NEW_ID, module->Or(NEW_ID, a, s), module->Not(NEW_ID, r)); + if (is_fine) { + return module->MuxGate(NEW_ID, module->AndGate(NEW_ID, module->OrGate(NEW_ID, a, s), module->NotGate(NEW_ID, r)), RTLIL::State::Sx, module->AndGate(NEW_ID, s, r)); + } else { + std::vector y; + for (int i = 0; i < a.size(); i++) + y.push_back(module->MuxGate(NEW_ID, module->AndGate(NEW_ID, module->OrGate(NEW_ID, a[i], s[i]), module->NotGate(NEW_ID, r[i])), RTLIL::State::Sx, module->AndGate(NEW_ID, s[i], r[i]))); + return y; + } } void execute(std::vector args, RTLIL::Design *design) override { diff --git a/techlibs/common/simcells.v b/techlibs/common/simcells.v index 1a113447e..3c38ca8b9 100644 --- a/techlibs/common/simcells.v +++ b/techlibs/common/simcells.v @@ -1613,6 +1613,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 0 0 - | x //- - - 0 - | 0 //- - 0 - - | 1 //- \ - - d | d @@ -1641,6 +1642,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 0 1 - | x //- - - 1 - | 0 //- - 0 - - | 1 //- \ - - d | d @@ -1669,6 +1671,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 1 0 - | x //- - - 0 - | 0 //- - 1 - - | 1 //- \ - - d | d @@ -1697,6 +1700,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 1 1 - | x //- - - 1 - | 0 //- - 1 - - | 1 //- \ - - d | d @@ -1725,6 +1729,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 0 0 - | x //- - - 0 - | 0 //- - 0 - - | 1 //- / - - d | d @@ -1753,6 +1758,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 0 1 - | x //- - - 1 - | 0 //- - 0 - - | 1 //- / - - d | d @@ -1781,6 +1787,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 1 0 - | x //- - - 0 - | 0 //- - 1 - - | 1 //- / - - d | d @@ -1809,6 +1816,7 @@ endmodule //- //- Truth table: C S R D | Q //- ---------+--- +//- - 1 1 - | x //- - - 1 - | 0 //- - 1 - - | 1 //- / - - d | d @@ -1837,6 +1845,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 0 - - | x //- - - 0 - - | 0 //- - 0 - - - | 1 //- \ - - 0 d | d @@ -1865,6 +1874,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 0 - - | x //- - - 0 - - | 0 //- - 0 - - - | 1 //- \ - - 1 d | d @@ -1893,6 +1903,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 1 - - | x //- - - 1 - - | 0 //- - 0 - - - | 1 //- \ - - 0 d | d @@ -1921,6 +1932,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 1 - - | x //- - - 1 - - | 0 //- - 0 - - - | 1 //- \ - - 1 d | d @@ -1949,6 +1961,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 0 - - | x //- - - 0 - - | 0 //- - 1 - - - | 1 //- \ - - 0 d | d @@ -1977,6 +1990,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 0 - - | x //- - - 0 - - | 0 //- - 1 - - - | 1 //- \ - - 1 d | d @@ -2005,6 +2019,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 1 - - | x //- - - 1 - - | 0 //- - 1 - - - | 1 //- \ - - 0 d | d @@ -2033,6 +2048,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 1 - - | x //- - - 1 - - | 0 //- - 1 - - - | 1 //- \ - - 1 d | d @@ -2061,6 +2077,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 0 - - | x //- - - 0 - - | 0 //- - 0 - - - | 1 //- / - - 0 d | d @@ -2089,6 +2106,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 0 - - | x //- - - 0 - - | 0 //- - 0 - - - | 1 //- / - - 1 d | d @@ -2117,6 +2135,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 1 - - | x //- - - 1 - - | 0 //- - 0 - - - | 1 //- / - - 0 d | d @@ -2145,6 +2164,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 0 1 - - | x //- - - 1 - - | 0 //- - 0 - - - | 1 //- / - - 1 d | d @@ -2173,6 +2193,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 0 - - | x //- - - 0 - - | 0 //- - 1 - - - | 1 //- / - - 0 d | d @@ -2201,6 +2222,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 0 - - | x //- - - 0 - - | 0 //- - 1 - - - | 1 //- / - - 1 d | d @@ -2229,6 +2251,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 1 - - | x //- - - 1 - - | 0 //- - 1 - - - | 1 //- / - - 0 d | d @@ -2257,6 +2280,7 @@ endmodule //- //- Truth table: C S R E D | Q //- -----------+--- +//- - 1 1 - - | x //- - - 1 - - | 0 //- - 1 - - - | 1 //- / - - 1 d | d diff --git a/tests/techmap/dfflibmap.ys b/tests/techmap/dfflibmap.ys index 303daee48..b5ba8fe63 100644 --- a/tests/techmap/dfflibmap.ys +++ b/tests/techmap/dfflibmap.ys @@ -64,8 +64,8 @@ select -assert-count 1 t:dffe select -assert-none t:dffn t:dffsr t:dffe t:$_NOT_ %% %n t:* %i design -load orig -dfflibmap -prepare -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr.lib -dfflibmap -map-only -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr.lib +dfflibmap -prepare -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib +dfflibmap -map-only -liberty dfflibmap_dffn_dffe.lib -liberty dfflibmap_dffsr_r.lib clean select -assert-count 5 t:$_NOT_ diff --git a/tests/techmap/dfflibmap_dffr_not_next.lib b/tests/techmap/dfflibmap_dffsr_not_next_l.lib similarity index 100% rename from tests/techmap/dfflibmap_dffr_not_next.lib rename to tests/techmap/dfflibmap_dffsr_not_next_l.lib diff --git a/tests/techmap/dfflibmap_dffsr.lib b/tests/techmap/dfflibmap_dffsr_r.lib similarity index 92% rename from tests/techmap/dfflibmap_dffsr.lib rename to tests/techmap/dfflibmap_dffsr_r.lib index e735dae1a..f36e200a0 100644 --- a/tests/techmap/dfflibmap_dffsr.lib +++ b/tests/techmap/dfflibmap_dffsr_r.lib @@ -7,8 +7,8 @@ library(test) { clear : "CLEAR"; preset : "PRESET"; clear_preset_var1 : L; - clear_preset_var2 : L; - } + clear_preset_var2 : H; + } pin(D) { direction : input; } @@ -28,6 +28,6 @@ library(test) { pin(QN) { direction: output; function : "IQN"; - } + } } } diff --git a/tests/techmap/dfflibmap_dffsr_s.lib b/tests/techmap/dfflibmap_dffsr_s.lib new file mode 100644 index 000000000..cf930f3c7 --- /dev/null +++ b/tests/techmap/dfflibmap_dffsr_s.lib @@ -0,0 +1,33 @@ +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 : 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"; + } + } +} diff --git a/tests/techmap/dfflibmap_dffsr_x.lib b/tests/techmap/dfflibmap_dffsr_x.lib new file mode 100644 index 000000000..91d702412 --- /dev/null +++ b/tests/techmap/dfflibmap_dffsr_x.lib @@ -0,0 +1,33 @@ +library(test) { + cell (dffsr) { + area : 6; + ff("IQ", "IQN") { + next_state : "D"; + clocked_on : "CLK"; + clear : "CLEAR"; + preset : "PRESET"; + clear_preset_var1 : X; + clear_preset_var2 : X; + } + 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"; + } + } +} diff --git a/tests/techmap/dfflibmap_formal.ys b/tests/techmap/dfflibmap_formal.ys index 71a52a261..e5e61cd62 100644 --- a/tests/techmap/dfflibmap_formal.ys +++ b/tests/techmap/dfflibmap_formal.ys @@ -8,13 +8,132 @@ $_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])); -// Formal checking of directly instantiated DFFSR doesn't work at the moment -// likely due to an equiv_induct assume bug #5196 +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])); -// // Workaround for DFFSR bug #5194 -// 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_s.lib + +copy top top_unmapped +dfflibmap -liberty dfflibmap_dffsr_s.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 <