diff --git a/backends/ilang/ilang_backend.cc b/backends/ilang/ilang_backend.cc
index 03e29c524..14e15017d 100644
--- a/backends/ilang/ilang_backend.cc
+++ b/backends/ilang/ilang_backend.cc
@@ -228,6 +228,7 @@ void ILANG_BACKEND::dump_proc_sync(std::ostream &f, std::string indent, const RT
 		f << stringf("\n");
 		break;
 	case RTLIL::STa: f << stringf("always\n"); break;
+	case RTLIL::STg: f << stringf("global\n"); break;
 	case RTLIL::STi: f << stringf("init\n"); break;
 	}
 
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 3c57162aa..229a3b596 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -220,12 +220,19 @@ struct AST_INTERNAL::ProcessGenerator
 		subst_lvalue_to = new_temp_signal(subst_lvalue_from);
 		subst_lvalue_map = subst_lvalue_from.to_sigbit_map(subst_lvalue_to);
 
+		bool found_global_syncs = false;
 		bool found_anyedge_syncs = false;
 		for (auto child : always->children)
-			if (child->type == AST_EDGE)
-				found_anyedge_syncs = true;
+			if (child->type == AST_EDGE) {
+				if (GetSize(child->children) == 1 && child->children.at(0)->type == AST_IDENTIFIER && child->children.at(0)->str == "\\$global_clock")
+					found_global_syncs = true;
+				else
+					found_anyedge_syncs = true;
+			}
 
 		if (found_anyedge_syncs) {
+			if (found_global_syncs)
+				log_error("Found non-synthesizable event list at %s:%d!\n", always->filename.c_str(), always->linenum);
 			log("Note: Assuming pure combinatorial block at %s:%d in\n", always->filename.c_str(), always->linenum);
 			log("compliance with IEC 62142(E):2005 / IEEE Std. 1364.1(E):2002. Recommending\n");
 			log("use of @* instead of @(...) for better match of synthesis and simulation.\n");
@@ -236,7 +243,7 @@ struct AST_INTERNAL::ProcessGenerator
 		for (auto child : always->children)
 			if (child->type == AST_POSEDGE || child->type == AST_NEGEDGE) {
 				found_clocked_sync = true;
-				if (found_anyedge_syncs)
+				if (found_global_syncs || found_anyedge_syncs)
 					log_error("Found non-synthesizable event list at %s:%d!\n", always->filename.c_str(), always->linenum);
 				RTLIL::SyncRule *syncrule = new RTLIL::SyncRule;
 				syncrule->type = child->type == AST_POSEDGE ? RTLIL::STp : RTLIL::STn;
@@ -248,7 +255,7 @@ struct AST_INTERNAL::ProcessGenerator
 			}
 		if (proc->syncs.empty()) {
 			RTLIL::SyncRule *syncrule = new RTLIL::SyncRule;
-			syncrule->type = RTLIL::STa;
+			syncrule->type = found_global_syncs ? RTLIL::STg : RTLIL::STa;
 			syncrule->signal = RTLIL::SigSpec();
 			addChunkActions(syncrule->actions, subst_lvalue_from, subst_lvalue_to, true);
 			proc->syncs.push_back(syncrule);
diff --git a/frontends/ilang/ilang_lexer.l b/frontends/ilang/ilang_lexer.l
index 415de74eb..842388548 100644
--- a/frontends/ilang/ilang_lexer.l
+++ b/frontends/ilang/ilang_lexer.l
@@ -74,6 +74,7 @@ USING_YOSYS_NAMESPACE
 "negedge"	{ return TOK_NEGEDGE; }
 "edge"		{ return TOK_EDGE; }
 "always"	{ return TOK_ALWAYS; }
+"global"	{ return TOK_GLOBAL; }
 "init"		{ return TOK_INIT; }
 "update"	{ return TOK_UPDATE; }
 "process"	{ return TOK_PROCESS; }
diff --git a/frontends/ilang/ilang_parser.y b/frontends/ilang/ilang_parser.y
index cc31c8642..fe5f23d66 100644
--- a/frontends/ilang/ilang_parser.y
+++ b/frontends/ilang/ilang_parser.y
@@ -57,7 +57,7 @@ USING_YOSYS_NAMESPACE
 %token <integer> TOK_INT
 %token TOK_AUTOIDX TOK_MODULE TOK_WIRE TOK_WIDTH TOK_INPUT TOK_OUTPUT TOK_INOUT
 %token TOK_CELL TOK_CONNECT TOK_SWITCH TOK_CASE TOK_ASSIGN TOK_SYNC
-%token TOK_LOW TOK_HIGH TOK_POSEDGE TOK_NEGEDGE TOK_EDGE TOK_ALWAYS TOK_INIT
+%token TOK_LOW TOK_HIGH TOK_POSEDGE TOK_NEGEDGE TOK_EDGE TOK_ALWAYS TOK_GLOBAL TOK_INIT
 %token TOK_UPDATE TOK_PROCESS TOK_END TOK_INVALID TOK_EOL TOK_OFFSET
 %token TOK_PARAMETER TOK_ATTRIBUTE TOK_MEMORY TOK_SIZE TOK_SIGNED TOK_UPTO
 
@@ -301,6 +301,12 @@ sync_list:
 		rule->signal = RTLIL::SigSpec();
 		current_process->syncs.push_back(rule);
 	} update_list |
+	sync_list TOK_SYNC TOK_GLOBAL EOL {
+		RTLIL::SyncRule *rule = new RTLIL::SyncRule;
+		rule->type = RTLIL::SyncType::STg;
+		rule->signal = RTLIL::SigSpec();
+		current_process->syncs.push_back(rule);
+	} update_list |
 	sync_list TOK_SYNC TOK_INIT EOL {
 		RTLIL::SyncRule *rule = new RTLIL::SyncRule;
 		rule->type = RTLIL::SyncType::STi;
diff --git a/kernel/rtlil.h b/kernel/rtlil.h
index 058f6acf4..109e33351 100644
--- a/kernel/rtlil.h
+++ b/kernel/rtlil.h
@@ -42,7 +42,8 @@ namespace RTLIL
 		STn = 3, // edge sensitive: negedge
 		STe = 4, // edge sensitive: both edges
 		STa = 5, // always active
-		STi = 6  // init
+		STg = 6, // global clock
+		STi = 7  // init
 	};
 
 	enum ConstFlags : unsigned char {
diff --git a/passes/proc/proc_dff.cc b/passes/proc/proc_dff.cc
index f532990c2..98653dc6b 100644
--- a/passes/proc/proc_dff.cc
+++ b/passes/proc/proc_dff.cc
@@ -196,7 +196,7 @@ void gen_dff(RTLIL::Module *mod, RTLIL::SigSpec sig_in, RTLIL::Const val_rst, RT
 	std::stringstream sstr;
 	sstr << "$procdff$" << (autoidx++);
 
-	RTLIL::Cell *cell = mod->addCell(sstr.str(), arst ? "$adff" : "$dff");
+	RTLIL::Cell *cell = mod->addCell(sstr.str(), clk.empty() ? "$ff" : arst ? "$adff" : "$dff");
 	cell->attributes = proc->attributes;
 
 	cell->parameters["\\WIDTH"] = RTLIL::Const(sig_in.size());
@@ -204,15 +204,21 @@ void gen_dff(RTLIL::Module *mod, RTLIL::SigSpec sig_in, RTLIL::Const val_rst, RT
 		cell->parameters["\\ARST_POLARITY"] = RTLIL::Const(arst_polarity, 1);
 		cell->parameters["\\ARST_VALUE"] = val_rst;
 	}
-	cell->parameters["\\CLK_POLARITY"] = RTLIL::Const(clk_polarity, 1);
+	if (!clk.empty()) {
+		cell->parameters["\\CLK_POLARITY"] = RTLIL::Const(clk_polarity, 1);
+	}
 
 	cell->setPort("\\D", sig_in);
 	cell->setPort("\\Q", sig_out);
 	if (arst)
 		cell->setPort("\\ARST", *arst);
-	cell->setPort("\\CLK", clk);
+	if (!clk.empty())
+		cell->setPort("\\CLK", clk);
 
-	log("  created %s cell `%s' with %s edge clock", cell->type.c_str(), cell->name.c_str(), clk_polarity ? "positive" : "negative");
+	if (!clk.empty())
+		log("  created %s cell `%s' with %s edge clock", cell->type.c_str(), cell->name.c_str(), clk_polarity ? "positive" : "negative");
+	else
+		log("  created %s cell `%s' with global clock", cell->type.c_str(), cell->name.c_str());
 	if (arst)
 		log(" and %s level reset", arst_polarity ? "positive" : "negative");
 	log(".\n");
@@ -236,6 +242,7 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce)
 		RTLIL::SyncRule *sync_level = NULL;
 		RTLIL::SyncRule *sync_edge = NULL;
 		RTLIL::SyncRule *sync_always = NULL;
+		bool global_clock = false;
 
 		std::map<RTLIL::SigSpec, std::set<RTLIL::SyncRule*>> many_async_rules;
 
@@ -267,6 +274,10 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce)
 				sig.replace(action.first, action.second, &insig);
 				sync_always = sync;
 			}
+			else if (sync->type == RTLIL::SyncType::STg) {
+				sig.replace(action.first, action.second, &insig);
+				global_clock = true;
+			}
 			else {
 				log_error("Event with any-edge sensitivity found for this signal!\n");
 			}
@@ -328,7 +339,7 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce)
 			continue;
 		}
 
-		if (!sync_edge)
+		if (!sync_edge && !global_clock)
 			log_error("Missing edge-sensitive event for this signal!\n");
 
 		if (many_async_rules.size() > 0)
@@ -346,9 +357,10 @@ void proc_dff(RTLIL::Module *mod, RTLIL::Process *proc, ConstEval &ce)
 		}
 		else
 			gen_dff(mod, insig, rstval.as_const(), sig,
-					sync_edge->type == RTLIL::SyncType::STp,
+					sync_edge && sync_edge->type == RTLIL::SyncType::STp,
 					sync_level && sync_level->type == RTLIL::SyncType::ST1,
-					sync_edge->signal, sync_level ? &sync_level->signal : NULL, proc);
+					sync_edge ? sync_edge->signal : SigSpec(),
+					sync_level ? &sync_level->signal : NULL, proc);
 
 		if (free_sync_level)
 			delete sync_level;
diff --git a/techlibs/common/simcells.v b/techlibs/common/simcells.v
index c4f170a3c..e770c5453 100644
--- a/techlibs/common/simcells.v
+++ b/techlibs/common/simcells.v
@@ -495,6 +495,23 @@ always @(posedge S, posedge R) begin
 end
 endmodule
 
+`ifdef SIMCELLS_FF
+//  |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+//-
+//-     $_FF_ (D, Q)
+//-
+//- A D-type flip-flop that is clocked from the implicit global clock. (This cell
+//- type is usually only used in netlists for formal verification.)
+//-
+module \$_FF_ (D, Q);
+input D;
+output reg Q;
+always @($global_clock) begin
+	Q <= D;
+end
+endmodule
+`endif
+
 //  |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
 //-
 //-     $_DFF_N_ (D, C, Q)
diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index db818269b..b10c858f2 100644
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -1382,18 +1382,22 @@ endmodule
 
 `endif
 // --------------------------------------------------------
+`ifdef SIMLIB_FF
 
 module \$ff (D, Q);
 
 parameter WIDTH = 0;
 
 input [WIDTH-1:0] D;
-output [WIDTH-1:0] Q;
+output reg [WIDTH-1:0] Q;
 
-assign D = Q;
+always @($global_clk) begin
+	Q <= D;
+end
 
 endmodule
 
+`endif
 // --------------------------------------------------------
 
 module \$dff (CLK, D, Q);