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.

16 files changed, 271 insertions, 8 deletions

diff --git a/CHANGELOG b/CHANGELOG
index 434872248..199d6a61a 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -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);