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.

backends/aiger/aiger.cc

@@ -733,6 +733,9 @@ struct AigerWriter
 				auto sig_qy = cell->getPort(cell->type.in(ID($anyconst), ID($anyseq)) ? ID::Y : ID::Q);
 				SigSpec sig = sigmap(sig_qy);
 
+				if (cell->get_bool_attribute(ID(clk2fflogic)))
+					sig_qy = cell->getPort(ID::D); // For a clk2fflogic $_FF_ the named signal is the D input not the Q output
+
 				for (int i = 0; i < GetSize(sig_qy); i++) {
 					if (sig_qy[i].wire == nullptr || sig[i].wire == nullptr)
 						continue;

backends/btor/btor.cc

@@ -728,7 +728,10 @@ struct BtorWorker
 			else
 				btorf("%d state %d %s\n", nid, sid, log_id(symbol));
 
-			ywmap_state(sig_q);
+			if (cell->get_bool_attribute(ID(clk2fflogic)))
+				ywmap_state(cell->getPort(ID::D)); // For a clk2fflogic FF the named signal is the D input not the Q output
+			else
+				ywmap_state(sig_q);
 
 			if (nid_init_val >= 0) {
 				int nid_init = next_nid++;

backends/smt2/smt2.cc

@@ -626,8 +626,9 @@ struct Smt2Worker
 				}
 
 				bool init_only = cell->type.in(ID($anyconst), ID($anyinit), ID($allconst));
+				bool clk2fflogic = cell->type == ID($anyinit) && cell->get_bool_attribute(ID(clk2fflogic));
 				int smtoffset = 0;
-				for (auto chunk : cell->getPort(QY).chunks()) {
+				for (auto chunk : cell->getPort(clk2fflogic ? ID::D : QY).chunks()) {
 					if (chunk.is_wire())
 						decls.push_back(witness_signal(init_only ? "init" : "seq", chunk.width, chunk.offset, "", idcounter, chunk.wire, smtoffset));
 					smtoffset += chunk.width;

passes/cmds/rename.cc

@@ -139,7 +139,12 @@ static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &ca
 
 		if (cell->type.in(ID($anyconst), ID($anyseq), ID($anyinit), ID($allconst), ID($allseq))) {
 			has_witness_signals = true;
-			auto QY = cell->type == ID($anyinit) ? ID::Q : ID::Y;
+			IdString QY;
+			bool clk2fflogic = false;
+			if (cell->type == ID($anyinit))
+				QY = (clk2fflogic = cell->get_bool_attribute(ID(clk2fflogic))) ? ID::D : ID::Q;
+			else
+				QY = ID::Y;
 			auto sig_out = cell->getPort(QY);
 
 			for (auto chunk : sig_out.chunks()) {
@@ -151,7 +156,10 @@ static bool rename_witness(RTLIL::Design *design, dict<RTLIL::Module *, int> &ca
 					auto new_id = module->uniquify("\\_witness_." + name);
 					auto new_wire = module->addWire(new_id, GetSize(sig_out));
 					new_wire->set_hdlname_attribute({ "_witness_", strstr(new_id.c_str(), ".") + 1 });
-					module->connect({sig_out, new_wire});
+					if (clk2fflogic)
+						module->connect({new_wire, sig_out});
+					else
+						module->connect({sig_out, new_wire});
 					cell->setPort(QY, new_wire);
 					break;
 				}

passes/opt/opt_clean.cc

@@ -292,10 +292,12 @@ bool rmunused_module_signals(RTLIL::Module *module, bool purge_mode, bool verbos
 	if (!purge_mode)
 		for (auto &it : module->cells_) {
 			RTLIL::Cell *cell = it.second;
-			if (ct_reg.cell_known(cell->type))
+			if (ct_reg.cell_known(cell->type)) {
+				bool clk2fflogic = cell->get_bool_attribute(ID(clk2fflogic));
 				for (auto &it2 : cell->connections())
-					if (ct_reg.cell_output(cell->type, it2.first))
+					if (clk2fflogic ? it2.first == ID::D : ct_reg.cell_output(cell->type, it2.first))
 						register_signals.add(it2.second);
+			}
 			for (auto &it2 : cell->connections())
 				connected_signals.add(it2.second);
 		}

passes/sat/clk2fflogic.cc

@@ -80,15 +80,27 @@ struct Clk2fflogicPass : public Pass {
 		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.
-	SampledSig sample_data(Module *module, SigSpec sig, RTLIL::Const init, bool is_fine) {
+	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());
+
+
 		Wire *sampled_sig = module->addWire(NEW_ID_SUFFIX(stringf("%s#sampled", sig_str.c_str())), GetSize(sig));
 		sampled_sig->attributes[ID::init] = init;
+
+		Cell *cell;
 		if (is_fine)
-			module->addFfGate(NEW_ID, sig, sampled_sig);
+			cell = module->addFfGate(NEW_ID, sig, sampled_sig);
 		else
-			module->addFf(NEW_ID, sig, sampled_sig);
+			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) {
@@ -213,7 +225,7 @@ struct Clk2fflogicPass : public Pass {
 					if (ff.has_clk)
 						ff.unmap_ce_srst();
 
-					auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine).sampled;
+					auto next_q = sample_data(module, ff.sig_q, ff.val_init, ff.is_fine, true).sampled;
 
 					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

passes/sat/sim.cc

@@ -140,6 +140,7 @@ struct SimInstance
 	dict<SigBit, pool<Wire*>> upd_outports;
 
 	dict<SigBit, SigBit> in_parent_drivers;
+	dict<SigBit, SigBit> clk2fflogic_drivers;
 
 	pool<SigBit> dirty_bits;
 	pool<Cell*> dirty_cells;
@@ -270,6 +271,11 @@ struct SimInstance
 				ff.past_srst = State::Sx;
 				ff.data = ff_data;
 				ff_database[cell] = ff;
+
+				if (cell->get_bool_attribute(ID(clk2fflogic))) {
+					for (int i = 0; i < ff_data.width; i++)
+						clk2fflogic_drivers.emplace(sigmap(ff_data.sig_d[i]), sigmap(ff_data.sig_q[i]));
+				}
 			}
 
 			if (cell->is_mem_cell())
@@ -389,6 +395,10 @@ struct SimInstance
 			auto sigbit = sig[i];
 			auto sigval = value[i];
 
+			auto clk2fflogic_driver = clk2fflogic_drivers.find(sigbit);
+			if (clk2fflogic_driver != clk2fflogic_drivers.end())
+				sigbit = clk2fflogic_driver->second;
+
 			auto in_parent_driver = in_parent_drivers.find(sigbit);
 			if (in_parent_driver == in_parent_drivers.end())
 				set_state(sigbit, sigval);