diff options
| -rw-r--r-- | CHANGELOG | 6 | ||||
| -rw-r--r-- | kernel/celltypes.h | 6 | ||||
| -rw-r--r-- | kernel/ff.cc | 19 | ||||
| -rw-r--r-- | kernel/ff.h | 8 | ||||
| -rw-r--r-- | kernel/rtlil.cc | 17 | ||||
| -rw-r--r-- | kernel/rtlil.h | 2 | ||||
| -rw-r--r-- | kernel/satgen.cc | 2 | ||||
| -rw-r--r-- | manual/CHAPTER_CellLib.tex | 2 | ||||
| -rw-r--r-- | passes/cmds/show.cc | 1 | ||||
| -rw-r--r-- | passes/fsm/fsm_detect.cc | 1 | ||||
| -rw-r--r-- | passes/hierarchy/submod.cc | 1 | ||||
| -rw-r--r-- | passes/opt/opt_clean.cc | 2 | ||||
| -rw-r--r-- | passes/sat/Makefile.inc | 1 | ||||
| -rw-r--r-- | passes/sat/formalff.cc | 192 | ||||
| -rw-r--r-- | passes/sat/sim.cc | 2 | ||||
| -rw-r--r-- | techlibs/common/simlib.v | 17 |
16 files changed, 271 insertions, 8 deletions
@@ -4,6 +4,12 @@ List of major changes and improvements between releases Yosys 0.20 .. Yosys 0.20-dev -------------------------- + * New commands and options + - Added "formalff" pass - transforms FFs for formal verification + + * Formal Verification + - Added $anyinit cell to directly represent FFs with an unconstrained + initialization value. These can be generated by the new formalff pass. Yosys 0.19 .. Yosys 0.20 -------------------------- diff --git a/kernel/celltypes.h b/kernel/celltypes.h index 7e9cfb38d..d62ba1506 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -51,6 +51,7 @@ struct CellTypes setup_internals(); setup_internals_mem(); + setup_internals_anyinit(); setup_stdcells(); setup_stdcells_mem(); } @@ -155,6 +156,11 @@ struct CellTypes setup_type(ID($dlatchsr), {ID::EN, ID::SET, ID::CLR, ID::D}, {ID::Q}); } + void setup_internals_anyinit() + { + setup_type(ID($anyinit), {ID::D}, {ID::Q}); + } + void setup_internals_mem() { setup_internals_ff(); diff --git a/kernel/ff.cc b/kernel/ff.cc index b0f1a924f..697ba7342 100644 --- a/kernel/ff.cc +++ b/kernel/ff.cc @@ -33,10 +33,14 @@ FfData::FfData(FfInitVals *initvals, Cell *cell_) : FfData(cell_->module, initva std::string type_str = cell->type.str(); - if (cell->type.in(ID($ff), ID($dff), ID($dffe), ID($dffsr), ID($dffsre), ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($sdff), ID($sdffe), ID($sdffce), ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr))) { - if (cell->type == ID($ff)) { + if (cell->type.in(ID($anyinit), ID($ff), ID($dff), ID($dffe), ID($dffsr), ID($dffsre), ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($sdff), ID($sdffe), ID($sdffce), ID($dlatch), ID($adlatch), ID($dlatchsr), ID($sr))) { + if (cell->type.in(ID($anyinit), ID($ff))) { has_gclk = true; sig_d = cell->getPort(ID::D); + if (cell->type == ID($anyinit)) { + is_anyinit = true; + log_assert(val_init.is_fully_undef()); + } } else if (cell->type == ID($sr)) { // No data input at all. } else if (cell->type.in(ID($dlatch), ID($adlatch), ID($dlatchsr))) { @@ -274,6 +278,7 @@ FfData FfData::slice(const std::vector<int> &bits) { res.has_sr = has_sr; res.ce_over_srst = ce_over_srst; res.is_fine = is_fine; + res.is_anyinit = is_anyinit; res.pol_clk = pol_clk; res.pol_ce = pol_ce; res.pol_aload = pol_aload; @@ -542,7 +547,7 @@ Cell *FfData::emit() { return nullptr; } } - if (initvals) + if (initvals && !is_anyinit) initvals->set_init(sig_q, val_init); if (!is_fine) { if (has_gclk) { @@ -552,7 +557,12 @@ Cell *FfData::emit() { log_assert(!has_arst); log_assert(!has_srst); log_assert(!has_sr); - cell = module->addFf(name, sig_d, sig_q); + if (is_anyinit) { + cell = module->addAnyinit(name, sig_d, sig_q); + log_assert(val_init.is_fully_undef()); + } else { + cell = module->addFf(name, sig_d, sig_q); + } } else if (!has_aload && !has_clk) { log_assert(has_sr); cell = module->addSr(name, sig_set, sig_clr, sig_q, pol_set, pol_clr); @@ -603,6 +613,7 @@ Cell *FfData::emit() { log_assert(!has_arst); log_assert(!has_srst); log_assert(!has_sr); + log_assert(!is_anyinit); cell = module->addFfGate(name, sig_d, sig_q); } else if (!has_aload && !has_clk) { log_assert(has_sr); diff --git a/kernel/ff.h b/kernel/ff.h index 41721b4a1..e684d3c43 100644 --- a/kernel/ff.h +++ b/kernel/ff.h @@ -28,7 +28,10 @@ YOSYS_NAMESPACE_BEGIN // Describes a flip-flop or a latch. // // If has_gclk, this is a formal verification FF with implicit global clock: -// Q is simply previous cycle's D. +// Q is simply previous cycle's D. Additionally if is_anyinit is true, this is +// an $anyinit cell which always has an undefined initialization value. Note +// that $anyinit is not considered to be among the FF celltypes, so a pass has +// to explicitly opt-in to process $anyinit cells with FfData. // // Otherwise, the FF/latch can have any number of features selected by has_* // attributes that determine Q's value (in order of decreasing priority): @@ -126,6 +129,8 @@ struct FfData { // True if this FF is a fine cell, false if it is a coarse cell. // If true, width must be 1. bool is_fine; + // True if this FF is an $anyinit cell. Depends on has_gclk. + bool is_anyinit; // Polarities, corresponding to sig_*. True means active-high, false // means active-low. bool pol_clk; @@ -156,6 +161,7 @@ struct FfData { has_sr = false; ce_over_srst = false; is_fine = false; + is_anyinit = false; pol_clk = false; pol_aload = false; pol_ce = false; diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc index b274bba78..5211c3b3f 100644 --- a/kernel/rtlil.cc +++ b/kernel/rtlil.cc @@ -1632,6 +1632,13 @@ namespace { return; } + if (cell->type.in(ID($anyinit))) { + port(ID::D, param(ID::WIDTH)); + port(ID::Q, param(ID::WIDTH)); + check_expected(); + return; + } + if (cell->type == ID($equiv)) { port(ID::A, 1); port(ID::B, 1); @@ -3120,6 +3127,16 @@ RTLIL::Cell* RTLIL::Module::addDlatchsrGate(RTLIL::IdString name, const RTLIL::S return cell; } +RTLIL::Cell* RTLIL::Module::addAnyinit(RTLIL::IdString name, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, const std::string &src) +{ + RTLIL::Cell *cell = addCell(name, ID($anyinit)); + cell->parameters[ID::WIDTH] = sig_q.size(); + cell->setPort(ID::D, sig_d); + cell->setPort(ID::Q, sig_q); + cell->set_src_attribute(src); + return cell; +} + RTLIL::SigSpec RTLIL::Module::Anyconst(RTLIL::IdString name, int width, const std::string &src) { RTLIL::SigSpec sig = addWire(NEW_ID, width); diff --git a/kernel/rtlil.h b/kernel/rtlil.h index db175d7e9..27ffdff1f 100644 --- a/kernel/rtlil.h +++ b/kernel/rtlil.h @@ -1375,6 +1375,8 @@ public: RTLIL::Cell* addDlatchsrGate (RTLIL::IdString name, const RTLIL::SigSpec &sig_en, const RTLIL::SigSpec &sig_set, const RTLIL::SigSpec &sig_clr, RTLIL::SigSpec sig_d, const RTLIL::SigSpec &sig_q, bool en_polarity = true, bool set_polarity = true, bool clr_polarity = true, const std::string &src = ""); + RTLIL::Cell* addAnyinit(RTLIL::IdString name, const RTLIL::SigSpec &sig_d, const RTLIL::SigSpec &sig_q, const std::string &src = ""); + // The methods without the add* prefix create a cell and an output signal. They return the newly created output signal. RTLIL::SigSpec Not (RTLIL::IdString name, const RTLIL::SigSpec &sig_a, bool is_signed = false, const std::string &src = ""); diff --git a/kernel/satgen.cc b/kernel/satgen.cc index 9c40ec66d..05eeca76e 100644 --- a/kernel/satgen.cc +++ b/kernel/satgen.cc @@ -1176,7 +1176,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep) return true; } - if (timestep > 0 && RTLIL::builtin_ff_cell_types().count(cell->type)) + if (timestep > 0 && (RTLIL::builtin_ff_cell_types().count(cell->type) || cell->type == ID($anyinit))) { FfData ff(nullptr, cell); diff --git a/manual/CHAPTER_CellLib.tex b/manual/CHAPTER_CellLib.tex index 3c9fb31cc..86b1f6a9a 100644 --- a/manual/CHAPTER_CellLib.tex +++ b/manual/CHAPTER_CellLib.tex @@ -603,7 +603,7 @@ Add information about {\tt \$specify2}, {\tt \$specify3}, and {\tt \$specrule} c \begin{fixme} Add information about {\tt \$assert}, {\tt \$assume}, {\tt \$live}, {\tt \$fair}, {\tt \$cover}, {\tt \$equiv}, -{\tt \$initstate}, {\tt \$anyconst}, {\tt \$anyseq}, {\tt \$allconst}, {\tt \$allseq} cells. +{\tt \$initstate}, {\tt \$anyconst}, {\tt \$anyseq}, {\tt \$anyinit}, {\tt \$allconst}, {\tt \$allseq} cells. \end{fixme} \begin{fixme} diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc index 43deba47b..4d5605932 100644 --- a/passes/cmds/show.cc +++ b/passes/cmds/show.cc @@ -574,6 +574,7 @@ struct ShowWorker { ct.setup_internals(); ct.setup_internals_mem(); + ct.setup_internals_anyinit(); ct.setup_stdcells(); ct.setup_stdcells_mem(); ct.setup_design(design); diff --git a/passes/fsm/fsm_detect.cc b/passes/fsm/fsm_detect.cc index a2d38a0bd..f829714c4 100644 --- a/passes/fsm/fsm_detect.cc +++ b/passes/fsm/fsm_detect.cc @@ -280,6 +280,7 @@ struct FsmDetectPass : public Pass { CellTypes ct; ct.setup_internals(); + ct.setup_internals_anyinit(); ct.setup_internals_mem(); ct.setup_stdcells(); ct.setup_stdcells_mem(); diff --git a/passes/hierarchy/submod.cc b/passes/hierarchy/submod.cc index 845dc850f..c0c40671d 100644 --- a/passes/hierarchy/submod.cc +++ b/passes/hierarchy/submod.cc @@ -260,6 +260,7 @@ struct SubmodWorker } ct.setup_internals(); + ct.setup_internals_anyinit(); ct.setup_internals_mem(); ct.setup_stdcells(); ct.setup_stdcells_mem(); diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc index cb2c261c4..dde7c5299 100644 --- a/passes/opt/opt_clean.cc +++ b/passes/opt/opt_clean.cc @@ -633,6 +633,7 @@ struct OptCleanPass : public Pass { keep_cache.reset(design); ct_reg.setup_internals_mem(); + ct_reg.setup_internals_anyinit(); ct_reg.setup_stdcells_mem(); ct_all.setup(design); @@ -694,6 +695,7 @@ struct CleanPass : public Pass { keep_cache.reset(design); ct_reg.setup_internals_mem(); + ct_reg.setup_internals_anyinit(); ct_reg.setup_stdcells_mem(); ct_all.setup(design); diff --git a/passes/sat/Makefile.inc b/passes/sat/Makefile.inc index da6d49433..ebe3dc536 100644 --- a/passes/sat/Makefile.inc +++ b/passes/sat/Makefile.inc @@ -10,6 +10,7 @@ OBJS += passes/sat/expose.o OBJS += passes/sat/assertpmux.o OBJS += passes/sat/clk2fflogic.o OBJS += passes/sat/async2sync.o +OBJS += passes/sat/formalff.o OBJS += passes/sat/supercover.o OBJS += passes/sat/fmcombine.o OBJS += passes/sat/mutate.o diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc new file mode 100644 index 000000000..fe6f98c16 --- /dev/null +++ b/passes/sat/formalff.cc @@ -0,0 +1,192 @@ +/* + * yosys -- Yosys Open SYnthesis Suite + * + * Copyright (C) 2022 Jannis Harder <jix@yosyshq.com> <me@jix.one> + * + * 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" +#include "kernel/ffinit.h" +#include "kernel/ff.h" + +USING_YOSYS_NAMESPACE +PRIVATE_NAMESPACE_BEGIN + +struct FormalFfPass : public Pass { + FormalFfPass() : Pass("formalff", "prepare FFs for formal") { } + void help() override + { + // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---| + log("\n"); + log(" formalff [options] [selection]\n"); + log("\n"); + log("This pass transforms clocked flip-flops to prepare a design for formal\n"); + log("verification. If a design contains latches and/or multiple different clocks run\n"); + log("the async2sync or clk2fflogic passes before using this pass.\n"); + log("\n"); + log(" -clk2ff\n"); + log(" Replace all clocked flip-flops with $ff cells that use the implicit\n"); + log(" global clock. This assumes, without checking, that the design uses a\n"); + log(" single global clock. If that is not the case, the clk2fflogic pass\n"); + log(" should be used instead.\n"); + log("\n"); + log(" -ff2anyinit\n"); + log(" Replace uninitialized bits of $ff cells with $anyinit cells. An\n"); + log(" $anyinit cell behaves exactly like an $ff cell with an undefined\n"); + log(" initialization value. The difference is that $anyinit inhibits\n"); + log(" don't-care optimizations and is used to track solver-provided values\n"); + log(" in witness traces.\n"); + log("\n"); + log(" If combined with -clk2ff this also affects newly created $ff cells.\n"); + log("\n"); + log(" -anyinit2ff\n"); + log(" Replaces $anyinit cells with uninitialized $ff cells. This performs the\n"); + log(" reverse of -ff2anyinit and can be used, before running a backend pass\n"); + log(" (or similar) that is not yet aware of $anyinit cells.\n"); + log("\n"); + log(" Note that after running -anyinit2ff, in general, performing don't-care\n"); + log(" optimizations is not sound in a formal verification setting.\n"); + log("\n"); + log(" -fine\n"); + log(" Emit fine-grained $_FF_ cells instead of coarse-grained $ff cells for\n"); + log(" -anyinit2ff. Cannot be combined with -clk2ff or -ff2anyinit.\n"); + log("\n"); + + // TODO: An option to check whether all FFs use the same clock before changing it to the global clock + } + void execute(std::vector<std::string> args, RTLIL::Design *design) override + { + bool flag_clk2ff = false; + bool flag_ff2anyinit = false; + bool flag_anyinit2ff = false; + bool flag_fine = false; + + log_header(design, "Executing FORMALFF pass.\n"); + + size_t argidx; + for (argidx = 1; argidx < args.size(); argidx++) + { + if (args[argidx] == "-clk2ff") { + flag_clk2ff = true; + continue; + } + if (args[argidx] == "-ff2anyinit") { + flag_ff2anyinit = true; + continue; + } + if (args[argidx] == "-anyinit2ff") { + flag_anyinit2ff = true; + continue; + } + if (args[argidx] == "-fine") { + flag_fine = true; + continue; + } + break; + } + extra_args(args, argidx, design); + + if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff)) + log_cmd_error("One of the options -clk2ff, -ff2anyinit, or -anyinit2ff must be specified.\n"); + + if (flag_ff2anyinit && flag_anyinit2ff) + log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n"); + + if (flag_fine && !flag_anyinit2ff) + log_cmd_error("The option -fine requries the -anyinit2ff option.\n"); + + if (flag_fine && flag_clk2ff) + log_cmd_error("The options -fine and -clk2ff are exclusive.\n"); + + for (auto module : design->selected_modules()) + { + SigMap sigmap(module); + FfInitVals initvals(&sigmap, module); + + + for (auto cell : module->selected_cells()) + { + if (flag_anyinit2ff && cell->type == ID($anyinit)) + { + FfData ff(&initvals, cell); + ff.remove(); + ff.is_anyinit = false; + ff.is_fine = flag_fine; + if (flag_fine) + for (int i = 0; i < ff.width; i++) + ff.slice({i}).emit(); + else + ff.emit(); + + continue; + } + + if (!RTLIL::builtin_ff_cell_types().count(cell->type)) + continue; + + FfData ff(&initvals, cell); + bool emit = false; + + if (flag_clk2ff && ff.has_clk) { + if (ff.sig_clk.is_fully_const()) + log_error("Const CLK on %s (%s) from module %s, run async2sync first.\n", + log_id(cell), log_id(cell->type), log_id(module)); + + ff.unmap_ce_srst(); + ff.has_clk = false; + ff.has_gclk = true; + emit = true; + } + + if (!ff.has_gclk) { + continue; + } + + if (flag_ff2anyinit && !ff.val_init.is_fully_def()) + { + ff.remove(); + emit = false; + + int cursor = 0; + while (cursor < ff.val_init.size()) + { + bool is_anyinit = ff.val_init[cursor] == State::Sx; + std::vector<int> bits; + bits.push_back(cursor++); + while (cursor < ff.val_init.size() && (ff.val_init[cursor] == State::Sx) == is_anyinit) + bits.push_back(cursor++); + + if ((int)bits.size() == ff.val_init.size()) { + // This check is only to make the private names more helpful for debugging + ff.is_anyinit = true; + emit = true; + break; + } + + auto slice = ff.slice(bits); + slice.is_anyinit = is_anyinit; + slice.emit(); + } + } + + if (emit) + ff.emit(); + } + } + } +} FormalFfPass; + +PRIVATE_NAMESPACE_END diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 53644c6b7..ea64dce06 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -231,7 +231,7 @@ struct SimInstance } } - if (RTLIL::builtin_ff_cell_types().count(cell->type)) { + if (RTLIL::builtin_ff_cell_types().count(cell->type) || cell->type == ID($anyinit)) { FfData ff_data(nullptr, cell); ff_state_t ff; ff.past_d = Const(State::Sx, ff_data.width); diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v index b14488ff4..ab9bd7e1d 100644 --- a/techlibs/common/simlib.v +++ b/techlibs/common/simlib.v @@ -1697,6 +1697,23 @@ assign Y = 'bx; endmodule // -------------------------------------------------------- +`ifdef SIMLIB_FF +module \$anyinit (D, Q); + +parameter WIDTH = 0; + +input [WIDTH-1:0] D; +output reg [WIDTH-1:0] Q; + +initial Q <= 'bx; + +always @($global_clk) begin + Q <= D; +end + +endmodule +`endif +// -------------------------------------------------------- module \$allconst (Y); |