From c0063288d699f4f3edf5e0ff6ee1bd5cfa9ac884 Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Thu, 21 Jul 2022 14:22:15 +0200 Subject: Add the $anyinit cell and the formalff pass These can be used to protect undefined flip-flop initialization values from optimizations that are not sound for formal verification and can help mapping all solver-provided values in witness traces for flows that use different backends simultaneously. --- kernel/celltypes.h | 6 ++++++ kernel/ff.cc | 19 +++++++++++++++---- kernel/ff.h | 8 +++++++- kernel/rtlil.cc | 17 +++++++++++++++++ kernel/rtlil.h | 2 ++ kernel/satgen.cc | 2 +- 6 files changed, 48 insertions(+), 6 deletions(-) (limited to 'kernel') 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 &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); -- cgit v1.2.3 From a5e1d3b9974668b4ab526a6b77ca96f1aa16d01f Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Tue, 2 Aug 2022 15:49:51 +0200 Subject: formalff: Set new replaced_by_gclk attribute on removed dff's clks This attribute can be used by formal backends to indicate which clocks were mapped to the global clock. Update the btor and smt2 backend which already handle clock inputs to understand this attribute. --- kernel/constids.inc | 1 + 1 file changed, 1 insertion(+) (limited to 'kernel') diff --git a/kernel/constids.inc b/kernel/constids.inc index 0f6dfc29b..239381f85 100644 --- a/kernel/constids.inc +++ b/kernel/constids.inc @@ -171,6 +171,7 @@ X(RD_TRANSPARENCY_MASK) X(RD_TRANSPARENT) X(RD_WIDE_CONTINUATION) X(reg) +X(replaced_by_gclk) X(reprocess_after) X(rom_block) X(rom_style) -- cgit v1.2.3