sim/formalff: Clock handling for yw cosim

backends/btor/btor.cc

@@ -95,7 +95,9 @@ struct BtorWorker
 
 	vector<ywmap_btor_sig> ywmap_inputs;
 	vector<ywmap_btor_sig> ywmap_states;
-	dict<SigBit, int> ywmap_clocks;
+	dict<SigBit, int> ywmap_clock_bits;
+	dict<SigBit, int> ywmap_clock_inputs;
+
 
 	PrettyJson ywmap_json;
 
@@ -693,7 +695,7 @@ struct BtorWorker
 					info_clocks[nid] |= negedge ? 2 : 1;
 
 				if (ywmap_json.active())
-					ywmap_clocks[sig_c] |= negedge ? 2 : 1;
+					ywmap_clock_bits[sig_c] |= negedge ? 2 : 1;
 			}
 
 			IdString symbol;
@@ -1175,6 +1177,20 @@ struct BtorWorker
 
 		btorf_push("inputs");
 
+		if (ywmap_json.active()) {
+			for (auto wire : module->wires())
+			{
+				auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
+				if (gclk_attr == wire->attributes.end())
+					continue;
+				SigSpec sig = sigmap(wire);
+				if (gclk_attr->second == State::S1)
+					ywmap_clock_bits[sig] |= 1;
+				else if (gclk_attr->second == State::S0)
+					ywmap_clock_bits[sig] |= 2;
+			}
+		}
+
 		for (auto wire : module->wires())
 		{
 			if (wire->attributes.count(ID::init)) {
@@ -1206,12 +1222,12 @@ struct BtorWorker
 			}
 
 			if (ywmap_json.active()) {
-				auto gclk_attr = wire->attributes.find(ID::replaced_by_gclk);
+				for (int i = 0; i < GetSize(sig); i++) {
-				if (gclk_attr != wire->attributes.end()) {
+					auto input_bit = SigBit(wire, i);
-					if (gclk_attr->second == State::S1)
+					auto bit = sigmap(input_bit);
-						ywmap_clocks[sig] |= 1;
+					if (!ywmap_clock_bits.count(bit))
-					else if (gclk_attr->second == State::S0)
+						continue;
-						ywmap_clocks[sig] |= 2;
+					ywmap_clock_inputs[input_bit] = ywmap_clock_bits[bit];
 				}
 			}
 		}
@@ -1479,7 +1495,7 @@ struct BtorWorker
 
 			ywmap_json.name("clocks");
 			ywmap_json.begin_array();
-			for (auto &entry : ywmap_clocks) {
+			for (auto &entry : ywmap_clock_inputs) {
 				if (entry.second != 1 && entry.second != 2)
 					continue;
 				log_assert(entry.first.is_wire());

backends/smt2/smt2.cc

@@ -998,7 +998,7 @@ struct Smt2Worker
 				if (contains_clock && GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
 					comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
 							clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
-				if (contains_clock) {
+				if (wire->port_input && contains_clock) {
 					for (int i = 0; i < GetSize(sig); i++) {
 						bool is_posedge = clock_posedge.count(sig[i]);
 						bool is_negedge = clock_negedge.count(sig[i]);

kernel/yw.h

@@ -69,8 +69,8 @@ struct ReadWitness
 	struct Clock {
 		IdPath path;
 		int offset;
-		bool is_posedge;
+		bool is_posedge = false;
-		bool is_negedge;
+		bool is_negedge = false;
 	};
 
 	struct Signal {

passes/sat/formalff.cc

@@ -317,6 +317,172 @@ struct InitValWorker
 	}
 };
 
+struct ReplacedPort {
+	IdString name;
+	int offset;
+	bool clk_pol;
+};
+
+struct HierarchyWorker
+{
+	Design *design;
+	pool<Module *> pending;
+
+	dict<Module *, std::vector<ReplacedPort>> replaced_clk_inputs;
+
+	HierarchyWorker(Design *design) :
+		design(design)
+	{
+		for (auto module : design->modules())
+			pending.insert(module);
+	}
+
+	void propagate();
+
+	const std::vector<ReplacedPort> &find_replaced_clk_inputs(IdString cell_type);
+};
+
+// Propagates replaced clock signals
+struct PropagateWorker
+{
+	HierarchyWorker &hierarchy;
+
+	Module *module;
+	SigMap sigmap;
+
+	dict<SigBit, bool> replaced_clk_bits;
+	dict<SigBit, SigBit> not_drivers;
+
+	std::vector<ReplacedPort> replaced_clk_inputs;
+	std::vector<std::pair<SigBit, bool>> pending;
+
+	PropagateWorker(Module *module, HierarchyWorker &hierarchy) :
+		hierarchy(hierarchy), module(module), sigmap(module)
+	{
+		hierarchy.pending.erase(module);
+
+		for (auto wire : module->wires())
+			if (wire->has_attribute(ID::replaced_by_gclk))
+				replace_clk_bit(SigBit(wire), wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1, false);
+
+		for (auto cell : module->cells()) {
+			if (cell->type.in(ID($not), ID($_NOT_))) {
+				auto sig_a = cell->getPort(ID::A);
+				auto &sig_y = cell->getPort(ID::Y);
+				sig_a.extend_u0(GetSize(sig_y), cell->parameters.at(ID::A_SIGNED).as_bool());
+
+				for (int i = 0; i < GetSize(sig_a); i++)
+					if (sig_a[i].is_wire())
+						not_drivers.emplace(sigmap(sig_y[i]), sigmap(sig_a[i]));
+			} else {
+				for (auto &port_bit : hierarchy.find_replaced_clk_inputs(cell->type))
+					replace_clk_bit(cell->getPort(port_bit.name)[port_bit.offset], port_bit.clk_pol, true);
+			}
+		}
+
+		while (!pending.empty()) {
+			auto current = pending.back();
+			pending.pop_back();
+			auto it = not_drivers.find(current.first);
+			if (it == not_drivers.end())
+				continue;
+
+			replace_clk_bit(it->second, !current.second, true);
+		}
+
+		for (auto cell : module->cells()) {
+			if (cell->type.in(ID($not), ID($_NOT_)))
+				continue;
+			for (auto &conn : cell->connections()) {
+				if (!cell->output(conn.first))
+					continue;
+				for (SigBit bit : conn.second) {
+					sigmap.apply(bit);
+					if (replaced_clk_bits.count(bit))
+						log_error("derived signal %s driven by %s (%s) from module %s is used as clock, derived clocks are only supported with clk2fflogic.\n",
+								log_signal(bit), log_id(cell->name), log_id(cell->type), log_id(module));
+				}
+			}
+		}
+
+		for (auto port : module->ports) {
+			auto wire = module->wire(port);
+			if (!wire->port_input)
+				continue;
+			for (int i = 0; i < GetSize(wire); i++) {
+				SigBit bit(wire, i);
+				sigmap.apply(bit);
+				auto it = replaced_clk_bits.find(bit);
+				if (it == replaced_clk_bits.end())
+					continue;
+				replaced_clk_inputs.emplace_back(ReplacedPort {port, i, it->second});
+
+				if (it->second) {
+					bit = module->Not(NEW_ID, bit);
+				}
+			}
+		}
+	}
+
+	void replace_clk_bit(SigBit bit, bool polarity, bool add_attribute)
+	{
+		sigmap.apply(bit);
+		if (!bit.is_wire())
+			log_error("XXX todo\n");
+
+		auto it = replaced_clk_bits.find(bit);
+		if (it != replaced_clk_bits.end()) {
+			if (it->second != polarity)
+				log_error("signal %s from module %s is used as clock with different polarities, run clk2fflogic instead.\n",
+						log_signal(bit), log_id(module));
+			return;
+		}
+
+		replaced_clk_bits.emplace(bit, polarity);
+
+		if (add_attribute) {
+			Wire *clk_wire = bit.wire;
+			if (bit.offset != 0 || GetSize(bit.wire) != 1) {
+				clk_wire = module->addWire(NEW_ID);
+				module->connect(RTLIL::SigBit(clk_wire), bit);
+			}
+			clk_wire->attributes[ID::replaced_by_gclk] = polarity ? State::S1 : State::S0;
+			clk_wire->set_bool_attribute(ID::keep);
+		}
+
+		pending.emplace_back(bit, polarity);
+	}
+};
+
+const std::vector<ReplacedPort> &HierarchyWorker::find_replaced_clk_inputs(IdString cell_type)
+{
+	static const std::vector<ReplacedPort> empty;
+	if (!cell_type.isPublic())
+		return empty;
+
+	Module *module = design->module(cell_type);
+	if (module == nullptr)
+		return empty;
+
+	auto it = replaced_clk_inputs.find(module);
+	if (it != replaced_clk_inputs.end())
+		return it->second;
+
+	if (pending.count(module)) {
+		PropagateWorker worker(module, *this);
+		return replaced_clk_inputs.emplace(module, std::move(worker.replaced_clk_inputs)).first->second;
+	}
+
+	return empty;
+}
+
+
+void HierarchyWorker::propagate()
+{
+	while (!pending.empty())
+		PropagateWorker worker(pending.pop(), *this);
+}
+
 struct FormalFfPass : public Pass {
 	FormalFfPass() : Pass("formalff", "prepare FFs for formal") { }
 	void help() override
@@ -362,6 +528,15 @@ struct FormalFfPass : public Pass {
 		log("        them. For -ff2anyinit, this reduces the number of generated $anyinit\n");
 		log("        cells that drive wires with private names.\n");
 		log("\n");
+		log("    -hierarchy\n");
+		log("        Propagates the 'replaced_by_gclk' attribute set by clk2ff upwards\n");
+		log("        through the design hierarchy towards the toplevel inputs. This option\n");
+		log("        works on the whole design and ignores the selection.\n");
+		log("\n");
+		log("    -assume\n");
+		log("        Add assumptions that constrain wires with the 'replaced_by_gclk'\n");
+		log("        attribute to the value they would have before an active clock edge.\n");
+		log("\n");
 
 		// TODO: An option to check whether all FFs use the same clock before changing it to the global clock
 	}
@@ -372,6 +547,8 @@ struct FormalFfPass : public Pass {
 		bool flag_anyinit2ff = false;
 		bool flag_fine = false;
 		bool flag_setundef = false;
+		bool flag_hierarchy = false;
+		bool flag_assume = false;
 
 		log_header(design, "Executing FORMALFF pass.\n");
 
@@ -398,12 +575,20 @@ struct FormalFfPass : public Pass {
 				flag_setundef = true;
 				continue;
 			}
+			if (args[argidx] == "-hierarchy") {
+				flag_hierarchy = true;
+				continue;
+			}
+			if (args[argidx] == "-assume") {
+				flag_assume = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
 
-		if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff))
+		if (!(flag_clk2ff || flag_ff2anyinit || flag_anyinit2ff || flag_hierarchy || flag_assume))
-			log_cmd_error("One of the options -clk2ff, -ff2anyinit, or -anyinit2ff must be specified.\n");
+			log_cmd_error("One of the options -clk2ff, -ff2anyinit, -anyinit2ff, -hierarchy or -assume must be specified.\n");
 
 		if (flag_ff2anyinit && flag_anyinit2ff)
 			log_cmd_error("The options -ff2anyinit and -anyinit2ff are exclusive.\n");
@@ -548,6 +733,33 @@ struct FormalFfPass : public Pass {
 					ff.emit();
 			}
 		}
+
+		if (flag_hierarchy) {
+			HierarchyWorker worker(design);
+			worker.propagate();
+		}
+
+		if (flag_assume) {
+			for (auto module : design->selected_modules()) {
+				std::vector<pair<SigBit, bool>> found;
+				for (auto wire : module->wires()) {
+					if (!wire->has_attribute(ID::replaced_by_gclk))
+						continue;
+					bool clk_pol = wire->attributes[ID::replaced_by_gclk].bits.at(0) == State::S1;
+
+					found.emplace_back(SigSpec(wire), clk_pol);
+				}
+				for (auto pair : found) {
+					SigBit clk = pair.first;
+
+					if (pair.second)
+						clk = module->Not(NEW_ID, clk);
+
+					module->addAssume(NEW_ID, clk, State::S1);
+
+				}
+			}
+		}
 	}
 } FormalFfPass;
 

passes/sat/sim.cc

@@ -1655,28 +1655,25 @@ struct SimWorker : SimShared
 	};
 
 	struct YwHierarchy {
-		dict<IdPath, FoundYWPath> signal_paths;
+		dict<IdPath, FoundYWPath> paths;
-		dict<IdPath, FoundYWPath> clock_paths;
 	};
 
 	YwHierarchy prepare_yw_hierarchy(const ReadWitness &yw)
 	{
+		YwHierarchy hierarchy;
 		pool<IdPath> paths;
 		dict<IdPath, pool<IdString>> mem_paths;
 
 		for (auto &signal : yw.signals)
 			paths.insert(signal.path);
 
-		for (auto &clock : yw.clocks) {
+		for (auto &clock : yw.clocks)
-			if (paths.count(clock.path))
-				log_warning("Witness path `%s` is present as witness signal and as clock, treating as clock and ignoring signal data.\n", clock.path.str().c_str());
 			paths.insert(clock.path);
-		}
+
 		for (auto &path : paths)
 			if (path.has_address())
 				mem_paths[path.prefix()].insert(path.back());
 
-		YwHierarchy hierarchy;
 		witness_hierarchy(top->module, top, [&](IdPath const &path, WitnessHierarchyItem item, SimInstance *instance) {
 			if (item.cell != nullptr)
 				return instance->children.at(item.cell);
@@ -1684,7 +1681,7 @@ struct SimWorker : SimShared
 				if (paths.count(path)) {
 					if (debug)
 						log("witness hierarchy: found wire %s\n", path.str().c_str());
-					bool inserted = hierarchy.signal_paths.emplace(path, {instance, item.wire, {}, INT_MIN}).second;
+					bool inserted = hierarchy.paths.emplace(path, {instance, item.wire, {}, INT_MIN}).second;
 					if (!inserted)
 						log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str());
 				}
@@ -1701,7 +1698,7 @@ struct SimWorker : SimShared
 						word_path.get_address(addr);
 						if (addr < item.mem->start_offset || (addr - item.mem->start_offset) >= item.mem->size)
 							continue;
-						bool inserted = hierarchy.signal_paths.emplace(word_path, {instance, nullptr, item.mem->memid, addr}).second;
+						bool inserted = hierarchy.paths.emplace(word_path, {instance, nullptr, item.mem->memid, addr}).second;
 						if (!inserted)
 							log_warning("Yosys witness path `%s` is ambiguous in this design\n", path.str().c_str());
 					}
@@ -1711,19 +1708,35 @@ struct SimWorker : SimShared
 		});
 
 		for (auto &path : paths)
-			if (!hierarchy.signal_paths.count(path))
+			if (!hierarchy.paths.count(path))
 				log_warning("Yosys witness path `%s` was not found in this design, ignoring\n", path.str().c_str());
 
+		dict<IdPath, dict<int, bool>> clock_inputs;
+
 		for (auto &clock : yw.clocks) {
-			auto found_path_it = hierarchy.signal_paths.find(clock.path);
+			if (clock.is_negedge == clock.is_posedge)
-			if (found_path_it == hierarchy.signal_paths.end())
 				continue;
-			hierarchy.clock_paths.insert(*found_path_it);
+			clock_inputs[clock.path].emplace(clock.offset, clock.is_posedge);
-			hierarchy.signal_paths.erase(found_path_it);
-			paths.insert(clock.path);
 		}
+		for (auto &signal : yw.signals) {
+			auto it = clock_inputs.find(signal.path);
+			if (it == clock_inputs.end())
+				continue;
 
+			for (auto &clock_input : it->second) {
+				int offset = clock_input.first;
+				if (offset >= signal.offset && (offset - signal.offset) < signal.width) {
+					int clock_bits_offset = signal.bits_offset + (offset - signal.offset);
 
+					State expected = clock_input.second ? State::S0 : State::S1;
+
+					for (int t = 0; t < GetSize(yw.steps); t++) {
+						if (yw.get_bits(t, clock_bits_offset, 1) != expected)
+							log_warning("Yosys witness trace has an unexpected value for the clock input `%s` in step %d.\n", signal.path.str().c_str(), t);
+					}
+				}
+			}
+		}
 		// TODO add checks and warnings for witness signals (toplevel inputs, $any*) not present in the witness file
 
 		return hierarchy;
@@ -1736,8 +1749,8 @@ struct SimWorker : SimShared
 		for (auto &signal : yw.signals) {
 			if (signal.init_only && t >= 1)
 				continue;
-			auto found_path_it = hierarchy.signal_paths.find(signal.path);
+			auto found_path_it = hierarchy.paths.find(signal.path);
-			if (found_path_it == hierarchy.signal_paths.end())
+			if (found_path_it == hierarchy.paths.end())
 				continue;
 			auto &found_path = found_path_it->second;
 
@@ -1767,8 +1780,8 @@ struct SimWorker : SimShared
 		for (auto &clock : yw.clocks) {
 			if (clock.is_negedge == clock.is_posedge)
 				continue;
-			auto found_path_it = hierarchy.clock_paths.find(clock.path);
+			auto found_path_it = hierarchy.paths.find(clock.path);
-			if (found_path_it == hierarchy.clock_paths.end())
+			if (found_path_it == hierarchy.paths.end())
 				continue;
 			auto &found_path = found_path_it->second;