yosys/passes/sat/clk2fflogic.cc

274 lines
10 KiB
C++
Raw Normal View History

2016-10-14 07:55:07 -05:00
/*
* yosys -- Yosys Open SYnthesis Suite
*
* Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
2016-10-14 07:55:07 -05:00
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
* copyright notice and this permission notice appear in all copies.
*
* THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
* WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
* MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
* ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
* WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
* ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
* OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
*
*/
#include "kernel/yosys.h"
#include "kernel/sigtools.h"
2020-07-18 20:25:41 -05:00
#include "kernel/ffinit.h"
#include "kernel/ff.h"
2020-10-16 18:39:22 -05:00
#include "kernel/mem.h"
2016-10-14 07:55:07 -05:00
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
struct SampledSig {
SigSpec sampled, current;
SigSpec &operator[](bool get_current) { return get_current ? current : sampled; }
};
2016-10-14 07:55:07 -05:00
struct Clk2fflogicPass : public Pass {
Clk2fflogicPass() : Pass("clk2fflogic", "convert clocked FFs to generic $ff cells") { }
2020-06-18 18:34:52 -05:00
void help() override
2016-10-14 07:55:07 -05:00
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log(" clk2fflogic [options] [selection]\n");
log("\n");
log("This command replaces clocked flip-flops with generic $ff cells that use the\n");
log("implicit global clock. This is useful for formal verification of designs with\n");
log("multiple clocks.\n");
log("\n");
log("This pass assumes negative hold time for the async FF inputs. For example when\n");
log("a reset deasserts with the clock edge, then the FF output will still drive the\n");
log("reset value in the next cycle regardless of the data-in value at the time of\n");
log("the clock edge.\n");
log("\n");
2016-10-14 07:55:07 -05:00
}
// Active-high sampled and current value of a level-triggered control signal. Initial sampled values is low/non-asserted.
SampledSig sample_control(Module *module, SigSpec sig, bool polarity, bool is_fine) {
if (!polarity) {
if (is_fine)
sig = module->NotGate(NEW_ID, sig);
else
sig = module->Not(NEW_ID, sig);
}
std::string sig_str = log_signal(sig);
sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end());
Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig));
sampled_sig->attributes[ID::init] = RTLIL::Const(State::S0, GetSize(sig));
if (is_fine)
module->addFfGate(NEW_ID, sig, sampled_sig);
else
module->addFf(NEW_ID, sig, sampled_sig);
return {sampled_sig, sig};
}
// Active-high trigger signal for an edge-triggered control signal. Initial values is low/non-edge.
SigSpec sample_control_edge(Module *module, SigSpec sig, bool polarity, bool is_fine) {
std::string sig_str = log_signal(sig);
sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end());
Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig));
sampled_sig->attributes[ID::init] = RTLIL::Const(polarity ? State::S1 : State::S0, GetSize(sig));
if (is_fine)
module->addFfGate(NEW_ID, sig, sampled_sig);
else
module->addFf(NEW_ID, sig, sampled_sig);
return module->Eqx(NEW_ID, {sampled_sig, sig}, polarity ? SigSpec {State::S0, State::S1} : SigSpec {State::S1, State::S0});
}
// Sampled and current value of a data signal.
Use clk2fflogic attr on cells to track original FF names in witnesses This makes clk2fflogic add an attr to $ff cells that carry the state of the emulated async FF. The $ff output doesn't have any async updates that happened in the current cycle, but the $ff input does, so the $ff input corresponds to the async FF's output in the original design. Hence this patch also makes the following changes to passes besides clk2fflogic (but only for FFs with the clk2fflogic attr set): * opt_clean treats the input as a register name (instead of the output) * rename -witness ensures that the input has a public name * the formal backends (smt2, btor, aiger) will use the input's name for the initial state of the FF in witness files * when sim reads a yw witness that assigns an initial value to the input signal, the state update is redirected to the output This ensures that yosys witness files for clk2fflogic designs have useful and stable public signal names. It also makes it possible to simulate a clk2fflogic witness on the original design (with some limitations when the original design is already using $ff cells). It might seem like setting the output of a clk2fflogic FF to update the input's initial value might not work in general, but it works fine for these reasons: * Witnesses for FFs are only present in the initial cycle, so we do not care about any later cycles. * The logic that clk2fflogic generates loops the output of the genreated FF back to the input, with muxes in between to apply any edge or level sensitive updates. So when there are no active updates in the current gclk cycle, there is a combinational path from the output back to the input. * The logic clk2fflogic generates makes sure that an edge sensitive update cannot be active in the first cycle (i.e. the past initial value is assumed to be whatever it needs to be to avoid an edge). * When a level sensitive update is active in the first gclk cycle, it is actively driving the output for the whole gclk cycle, so ignoring any witness initialization is the correct behavior.
2023-05-25 05:48:02 -05:00
SampledSig sample_data(Module *module, SigSpec sig, RTLIL::Const init, bool is_fine, bool set_attribute = false) {
std::string sig_str = log_signal(sig);
sig_str.erase(std::remove(sig_str.begin(), sig_str.end(), ' '), sig_str.end());
Use clk2fflogic attr on cells to track original FF names in witnesses This makes clk2fflogic add an attr to $ff cells that carry the state of the emulated async FF. The $ff output doesn't have any async updates that happened in the current cycle, but the $ff input does, so the $ff input corresponds to the async FF's output in the original design. Hence this patch also makes the following changes to passes besides clk2fflogic (but only for FFs with the clk2fflogic attr set): * opt_clean treats the input as a register name (instead of the output) * rename -witness ensures that the input has a public name * the formal backends (smt2, btor, aiger) will use the input's name for the initial state of the FF in witness files * when sim reads a yw witness that assigns an initial value to the input signal, the state update is redirected to the output This ensures that yosys witness files for clk2fflogic designs have useful and stable public signal names. It also makes it possible to simulate a clk2fflogic witness on the original design (with some limitations when the original design is already using $ff cells). It might seem like setting the output of a clk2fflogic FF to update the input's initial value might not work in general, but it works fine for these reasons: * Witnesses for FFs are only present in the initial cycle, so we do not care about any later cycles. * The logic that clk2fflogic generates loops the output of the genreated FF back to the input, with muxes in between to apply any edge or level sensitive updates. So when there are no active updates in the current gclk cycle, there is a combinational path from the output back to the input. * The logic clk2fflogic generates makes sure that an edge sensitive update cannot be active in the first cycle (i.e. the past initial value is assumed to be whatever it needs to be to avoid an edge). * When a level sensitive update is active in the first gclk cycle, it is actively driving the output for the whole gclk cycle, so ignoring any witness initialization is the correct behavior.
2023-05-25 05:48:02 -05:00
Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig));
sampled_sig->attributes[ID::init] = init;
Use clk2fflogic attr on cells to track original FF names in witnesses This makes clk2fflogic add an attr to $ff cells that carry the state of the emulated async FF. The $ff output doesn't have any async updates that happened in the current cycle, but the $ff input does, so the $ff input corresponds to the async FF's output in the original design. Hence this patch also makes the following changes to passes besides clk2fflogic (but only for FFs with the clk2fflogic attr set): * opt_clean treats the input as a register name (instead of the output) * rename -witness ensures that the input has a public name * the formal backends (smt2, btor, aiger) will use the input's name for the initial state of the FF in witness files * when sim reads a yw witness that assigns an initial value to the input signal, the state update is redirected to the output This ensures that yosys witness files for clk2fflogic designs have useful and stable public signal names. It also makes it possible to simulate a clk2fflogic witness on the original design (with some limitations when the original design is already using $ff cells). It might seem like setting the output of a clk2fflogic FF to update the input's initial value might not work in general, but it works fine for these reasons: * Witnesses for FFs are only present in the initial cycle, so we do not care about any later cycles. * The logic that clk2fflogic generates loops the output of the genreated FF back to the input, with muxes in between to apply any edge or level sensitive updates. So when there are no active updates in the current gclk cycle, there is a combinational path from the output back to the input. * The logic clk2fflogic generates makes sure that an edge sensitive update cannot be active in the first cycle (i.e. the past initial value is assumed to be whatever it needs to be to avoid an edge). * When a level sensitive update is active in the first gclk cycle, it is actively driving the output for the whole gclk cycle, so ignoring any witness initialization is the correct behavior.
2023-05-25 05:48:02 -05:00
Cell *cell;
if (is_fine)
Use clk2fflogic attr on cells to track original FF names in witnesses This makes clk2fflogic add an attr to $ff cells that carry the state of the emulated async FF. The $ff output doesn't have any async updates that happened in the current cycle, but the $ff input does, so the $ff input corresponds to the async FF's output in the original design. Hence this patch also makes the following changes to passes besides clk2fflogic (but only for FFs with the clk2fflogic attr set): * opt_clean treats the input as a register name (instead of the output) * rename -witness ensures that the input has a public name * the formal backends (smt2, btor, aiger) will use the input's name for the initial state of the FF in witness files * when sim reads a yw witness that assigns an initial value to the input signal, the state update is redirected to the output This ensures that yosys witness files for clk2fflogic designs have useful and stable public signal names. It also makes it possible to simulate a clk2fflogic witness on the original design (with some limitations when the original design is already using $ff cells). It might seem like setting the output of a clk2fflogic FF to update the input's initial value might not work in general, but it works fine for these reasons: * Witnesses for FFs are only present in the initial cycle, so we do not care about any later cycles. * The logic that clk2fflogic generates loops the output of the genreated FF back to the input, with muxes in between to apply any edge or level sensitive updates. So when there are no active updates in the current gclk cycle, there is a combinational path from the output back to the input. * The logic clk2fflogic generates makes sure that an edge sensitive update cannot be active in the first cycle (i.e. the past initial value is assumed to be whatever it needs to be to avoid an edge). * When a level sensitive update is active in the first gclk cycle, it is actively driving the output for the whole gclk cycle, so ignoring any witness initialization is the correct behavior.
2023-05-25 05:48:02 -05:00
cell = module->addFfGate(NEW_ID, sig, sampled_sig);
else
Use clk2fflogic attr on cells to track original FF names in witnesses This makes clk2fflogic add an attr to $ff cells that carry the state of the emulated async FF. The $ff output doesn't have any async updates that happened in the current cycle, but the $ff input does, so the $ff input corresponds to the async FF's output in the original design. Hence this patch also makes the following changes to passes besides clk2fflogic (but only for FFs with the clk2fflogic attr set): * opt_clean treats the input as a register name (instead of the output) * rename -witness ensures that the input has a public name * the formal backends (smt2, btor, aiger) will use the input's name for the initial state of the FF in witness files * when sim reads a yw witness that assigns an initial value to the input signal, the state update is redirected to the output This ensures that yosys witness files for clk2fflogic designs have useful and stable public signal names. It also makes it possible to simulate a clk2fflogic witness on the original design (with some limitations when the original design is already using $ff cells). It might seem like setting the output of a clk2fflogic FF to update the input's initial value might not work in general, but it works fine for these reasons: * Witnesses for FFs are only present in the initial cycle, so we do not care about any later cycles. * The logic that clk2fflogic generates loops the output of the genreated FF back to the input, with muxes in between to apply any edge or level sensitive updates. So when there are no active updates in the current gclk cycle, there is a combinational path from the output back to the input. * The logic clk2fflogic generates makes sure that an edge sensitive update cannot be active in the first cycle (i.e. the past initial value is assumed to be whatever it needs to be to avoid an edge). * When a level sensitive update is active in the first gclk cycle, it is actively driving the output for the whole gclk cycle, so ignoring any witness initialization is the correct behavior.
2023-05-25 05:48:02 -05:00
cell = module->addFf(NEW_ID, sig, sampled_sig);
if (set_attribute) {
for (auto &chunk : sig.chunks())
if (chunk.wire != nullptr)
chunk.wire->set_bool_attribute(ID::keep);
cell->set_bool_attribute(ID(clk2fflogic));
}
return {sampled_sig, sig};
}
SigSpec mux(Module *module, SigSpec a, SigSpec b, SigSpec s, bool is_fine) {
if (is_fine)
return module->MuxGate(NEW_ID, a, b, s);
else
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));
}
2020-06-18 18:34:52 -05:00
void execute(std::vector<std::string> args, RTLIL::Design *design) override
2016-10-14 07:55:07 -05:00
{
// bool flag_noinit = false;
log_header(design, "Executing CLK2FFLOGIC pass (convert clocked FFs to generic $ff cells).\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
// if (args[argidx] == "-noinit") {
// flag_noinit = true;
// continue;
// }
break;
}
extra_args(args, argidx, design);
for (auto module : design->selected_modules())
{
SigMap sigmap(module);
2020-07-18 20:25:41 -05:00
FfInitVals initvals(&sigmap, module);
2016-10-14 07:55:07 -05:00
2020-10-16 18:39:22 -05:00
for (auto &mem : Mem::get_selected_memories(module))
2016-10-14 07:55:07 -05:00
{
2020-10-16 18:39:22 -05:00
for (int i = 0; i < GetSize(mem.rd_ports); i++) {
auto &port = mem.rd_ports[i];
if (port.clk_enable)
log_error("Read port %d of memory %s.%s is clocked. This is not supported by \"clk2fflogic\"! "
"Call \"memory\" with -nordff to avoid this error.\n", i, log_id(mem.memid), log_id(module));
}
2017-12-13 19:07:31 -06:00
2020-10-16 18:39:22 -05:00
for (int i = 0; i < GetSize(mem.wr_ports); i++)
{
auto &port = mem.wr_ports[i];
2017-12-13 19:07:31 -06:00
2020-10-16 18:39:22 -05:00
if (!port.clk_enable)
continue;
2017-12-13 19:07:31 -06:00
2020-10-16 18:39:22 -05:00
log("Modifying write port %d on memory %s.%s: CLK=%s, A=%s, D=%s\n",
i, log_id(module), log_id(mem.memid), log_signal(port.clk),
log_signal(port.addr), log_signal(port.data));
2017-12-13 19:07:31 -06:00
Wire *past_clk = module->addWire(NEW_ID_SUFFIX(stringf("%s#%d#past_clk#%s", log_id(mem.memid), i, log_signal(port.clk))));
2020-10-16 18:39:22 -05:00
past_clk->attributes[ID::init] = port.clk_polarity ? State::S1 : State::S0;
module->addFf(NEW_ID, port.clk, past_clk);
2017-12-13 19:07:31 -06:00
2020-10-16 18:39:22 -05:00
SigSpec clock_edge_pattern;
2017-12-13 19:07:31 -06:00
2020-10-16 18:39:22 -05:00
if (port.clk_polarity) {
clock_edge_pattern.append(State::S0);
clock_edge_pattern.append(State::S1);
} else {
clock_edge_pattern.append(State::S1);
clock_edge_pattern.append(State::S0);
}
2017-12-13 19:07:31 -06:00
2020-10-16 18:39:22 -05:00
SigSpec clock_edge = module->Eqx(NEW_ID, {port.clk, SigSpec(past_clk)}, clock_edge_pattern);
2017-12-13 19:07:31 -06:00
SigSpec en_q = module->addWire(NEW_ID_SUFFIX(stringf("%s#%d#en_q", log_id(mem.memid), i)), GetSize(port.en));
2020-10-16 18:39:22 -05:00
module->addFf(NEW_ID, port.en, en_q);
2017-12-13 19:07:31 -06:00
SigSpec addr_q = module->addWire(NEW_ID_SUFFIX(stringf("%s#%d#addr_q", log_id(mem.memid), i)), GetSize(port.addr));
2020-10-16 18:39:22 -05:00
module->addFf(NEW_ID, port.addr, addr_q);
2017-12-13 19:07:31 -06:00
SigSpec data_q = module->addWire(NEW_ID_SUFFIX(stringf("%s#%d#data_q", log_id(mem.memid), i)), GetSize(port.data));
2020-10-16 18:39:22 -05:00
module->addFf(NEW_ID, port.data, data_q);
2017-12-13 19:07:31 -06:00
2020-10-16 18:39:22 -05:00
port.clk = State::S0;
port.en = module->Mux(NEW_ID, Const(0, GetSize(en_q)), en_q, clock_edge);
port.addr = addr_q;
port.data = data_q;
2017-12-13 19:07:31 -06:00
2020-10-16 18:39:22 -05:00
port.clk_enable = false;
port.clk_polarity = false;
2017-12-13 12:14:34 -06:00
}
2020-10-16 18:39:22 -05:00
mem.emit();
}
for (auto cell : vector<Cell*>(module->selected_cells()))
{
2020-07-18 20:25:41 -05:00
SigSpec qval;
if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
FfData ff(&initvals, cell);
2018-02-26 05:20:28 -06:00
if (ff.has_gclk) {
2020-07-18 20:25:41 -05:00
// Already a $ff or $_FF_ cell.
continue;
2018-02-26 05:20:28 -06:00
}
if (ff.has_clk) {
log("Replacing %s.%s (%s): CLK=%s, D=%s, Q=%s\n",
log_id(module), log_id(cell), log_id(cell->type),
log_signal(ff.sig_clk), log_signal(ff.sig_d), log_signal(ff.sig_q));
} else if (ff.has_aload) {
log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n",
log_id(module), log_id(cell), log_id(cell->type),
log_signal(ff.sig_aload), log_signal(ff.sig_ad), log_signal(ff.sig_q));
} else {
// $sr.
log("Replacing %s.%s (%s): SET=%s, CLR=%s, Q=%s\n",
log_id(module), log_id(cell), log_id(cell->type),
log_signal(ff.sig_set), log_signal(ff.sig_clr), log_signal(ff.sig_q));
}
ff.remove();
if (ff.has_clk)
ff.unmap_ce_srst();
2016-10-14 07:55:07 -05:00
Use clk2fflogic attr on cells to track original FF names in witnesses This makes clk2fflogic add an attr to $ff cells that carry the state of the emulated async FF. The $ff output doesn't have any async updates that happened in the current cycle, but the $ff input does, so the $ff input corresponds to the async FF's output in the original design. Hence this patch also makes the following changes to passes besides clk2fflogic (but only for FFs with the clk2fflogic attr set): * opt_clean treats the input as a register name (instead of the output) * rename -witness ensures that the input has a public name * the formal backends (smt2, btor, aiger) will use the input's name for the initial state of the FF in witness files * when sim reads a yw witness that assigns an initial value to the input signal, the state update is redirected to the output This ensures that yosys witness files for clk2fflogic designs have useful and stable public signal names. It also makes it possible to simulate a clk2fflogic witness on the original design (with some limitations when the original design is already using $ff cells). It might seem like setting the output of a clk2fflogic FF to update the input's initial value might not work in general, but it works fine for these reasons: * Witnesses for FFs are only present in the initial cycle, so we do not care about any later cycles. * The logic that clk2fflogic generates loops the output of the genreated FF back to the input, with muxes in between to apply any edge or level sensitive updates. So when there are no active updates in the current gclk cycle, there is a combinational path from the output back to the input. * The logic clk2fflogic generates makes sure that an edge sensitive update cannot be active in the first cycle (i.e. the past initial value is assumed to be whatever it needs to be to avoid an edge). * When a level sensitive update is active in the first gclk cycle, it is actively driving the output for the whole gclk cycle, so ignoring any witness initialization is the correct behavior.
2023-05-25 05:48:02 -05:00
auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine, true).sampled;
2016-10-14 07:55:07 -05:00
if (ff.has_clk) {
// The init value for the sampled d is never used, so we can set it to fixed zero, reducing uninit'd FFs
auto sampled_d = sample_data(module, ff.sig_d, RTLIL::Const(State::S0, ff.width), ff.is_fine);
auto clk_edge = sample_control_edge(module, ff.sig_clk, ff.pol_clk, ff.is_fine);
next_q = mux(module, next_q, sampled_d.sampled, clk_edge, ff.is_fine);
}
SampledSig sampled_aload, sampled_ad, sampled_set, sampled_clr, sampled_arst;
// The check for a constant sig_aload is also done by opt_dff, but when using verific and running
// clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids
// generating a lot of extra logic.
bool has_nonconst_aload = ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1);
if (has_nonconst_aload) {
sampled_aload = sample_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine);
// The init value for the sampled ad is never used, so we can set it to fixed zero, reducing uninit'd FFs
sampled_ad = sample_data(module, ff.sig_ad, RTLIL::Const(State::S0, ff.width), ff.is_fine);
2016-10-14 07:55:07 -05:00
}
2020-07-18 20:25:41 -05:00
if (ff.has_sr) {
sampled_set = sample_control(module, ff.sig_set, ff.pol_set, ff.is_fine);
sampled_clr = sample_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine);
}
if (ff.has_arst)
sampled_arst = sample_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine);
// First perform updates using _only_ sampled values, then again using _only_ current values. Unlike the previous
// implementation, this approach correctly handles all the cases of multiple signals changing simultaneously.
for (int current = 0; current < 2; current++) {
if (has_nonconst_aload)
next_q = mux(module, next_q, sampled_ad[current], sampled_aload[current], ff.is_fine);
if (ff.has_sr)
next_q = bitwise_sr(module, next_q, sampled_set[current], sampled_clr[current], ff.is_fine);
if (ff.has_arst)
next_q = mux(module, next_q, ff.val_arst, sampled_arst[current], ff.is_fine);
2016-10-14 07:55:07 -05:00
}
module->connect(ff.sig_q, next_q);
2016-10-14 07:55:07 -05:00
}
}
}
}
} Clk2fflogicPass;
PRIVATE_NAMESPACE_END