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.

6 files changed, 48 insertions, 6 deletions

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);