diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc
index d2bca3065..c60b43d3f 100644
--- a/backends/cxxrtl/cxxrtl_backend.cc
+++ b/backends/cxxrtl/cxxrtl_backend.cc
@@ -218,7 +218,7 @@ bool is_internal_cell(RTLIL::IdString type)
 
 bool is_effectful_cell(RTLIL::IdString type)
 {
-	return type.isPublic() || type == ID($print);
+	return type.in(ID($print), ID($check));
 }
 
 bool is_cxxrtl_blackbox_cell(const RTLIL::Cell *cell)
@@ -282,7 +282,7 @@ struct FlowGraph {
 			CONNECT,
 			CELL_SYNC,
 			CELL_EVAL,
-			PRINT_SYNC,
+			EFFECT_SYNC,
 			PROCESS_SYNC,
 			PROCESS_CASE,
 			MEM_RDPORT,
@@ -292,7 +292,7 @@ struct FlowGraph {
 		Type type;
 		RTLIL::SigSig connect = {};
 		const RTLIL::Cell *cell = nullptr;
-		std::vector<const RTLIL::Cell*> print_sync_cells;
+		std::vector<const RTLIL::Cell*> cells;
 		const RTLIL::Process *process = nullptr;
 		const Mem *mem = nullptr;
 		int portidx;
@@ -480,11 +480,11 @@ struct FlowGraph {
 		return node;
 	}
 
-	Node *add_print_sync_node(std::vector<const RTLIL::Cell*> cells)
+	Node *add_effect_sync_node(std::vector<const RTLIL::Cell*> cells)
 	{
 		Node *node = new Node;
-		node->type = Node::Type::PRINT_SYNC;
-		node->print_sync_cells = cells;
+		node->type = Node::Type::EFFECT_SYNC;
+		node->cells = cells;
 		nodes.push_back(node);
 		return node;
 	}
@@ -1063,99 +1063,6 @@ struct CxxrtlWorker {
 			f << ".val()";
 	}
 
-	void dump_print(const RTLIL::Cell *cell)
-	{
-		Fmt fmt = {};
-		fmt.parse_rtlil(cell);
-
-		f << indent << "if (";
-		dump_sigspec_rhs(cell->getPort(ID::EN));
-		f << " == value<1>{1u}) {\n";
-		inc_indent();
-			dict<std::string, RTLIL::SigSpec> fmt_args;
-			f << indent << "struct : public lazy_fmt {\n";
-			inc_indent();
-				f << indent << "std::string operator() () const override {\n";
-				inc_indent();
-					fmt.emit_cxxrtl(f, indent, [&](const RTLIL::SigSpec &sig) {
-						if (sig.size() == 0)
-							f << "value<0>()";
-						else {
-							std::string arg_name = "arg" + std::to_string(fmt_args.size());
-							fmt_args[arg_name] = sig;
-							f << arg_name;
-						}
-					}, "performer");
-				dec_indent();
-				f << indent << "}\n";
-				f << indent << "struct performer *performer;\n";
-				for (auto arg : fmt_args)
-					f << indent << "value<" << arg.second.size() << "> " << arg.first << ";\n";
-			dec_indent();
-			f << indent << "} formatter;\n";
-			f << indent << "formatter.performer = performer;\n";
-			for (auto arg : fmt_args) {
-				f << indent << "formatter." << arg.first << " = ";
-				dump_sigspec_rhs(arg.second);
-				f << ";\n";
-			}
-			f << indent << "if (performer) {\n";
-			inc_indent();
-				f << indent << "static const metadata_map attributes = ";
-				dump_metadata_map(cell->attributes);
-				f << ";\n";
-				f << indent << "performer->on_print(formatter, attributes);\n";
-			dec_indent();
-			f << indent << "} else {\n";
-			inc_indent();
-				f << indent << print_output << " << formatter();\n";
-			dec_indent();
-			f << indent << "}\n";
-		dec_indent();
-		f << indent << "}\n";
-	}
-
-	void dump_sync_print(std::vector<const RTLIL::Cell*> &cells)
-	{
-		log_assert(!cells.empty());
-		const auto &trg = cells[0]->getPort(ID::TRG);
-		const auto &trg_polarity = cells[0]->getParam(ID::TRG_POLARITY);
-
-		f << indent << "if (";
-		for (int i = 0; i < trg.size(); i++) {
-			RTLIL::SigBit trg_bit = trg[i];
-			trg_bit = sigmaps[trg_bit.wire->module](trg_bit);
-			log_assert(trg_bit.wire);
-
-			if (i != 0)
-				f << " || ";
-
-			if (trg_polarity[i] == State::S1)
-				f << "posedge_";
-			else
-				f << "negedge_";
-			f << mangle(trg_bit);
-		}
-		f << ") {\n";
-		inc_indent();
-			std::sort(cells.begin(), cells.end(), [](const RTLIL::Cell *a, const RTLIL::Cell *b) {
-				return a->getParam(ID::PRIORITY).as_int() > b->getParam(ID::PRIORITY).as_int();
-			});
-			for (auto cell : cells) {
-				log_assert(cell->getParam(ID::TRG_ENABLE).as_bool());
-				log_assert(cell->getPort(ID::TRG) == trg);
-				log_assert(cell->getParam(ID::TRG_POLARITY) == trg_polarity);
-
-				std::vector<const RTLIL::Cell*> inlined_cells;
-				collect_cell_eval(cell, /*for_debug=*/false, inlined_cells);
-				dump_inlined_cells(inlined_cells);
-				dump_print(cell);
-			}
-		dec_indent();
-
-		f << indent << "}\n";
-	}
-
 	void dump_inlined_cells(const std::vector<const RTLIL::Cell*> &cells)
 	{
 		if (cells.empty()) {
@@ -1309,6 +1216,144 @@ struct CxxrtlWorker {
 		}
 	}
 
+	void dump_print(const RTLIL::Cell *cell)
+	{
+		Fmt fmt;
+		fmt.parse_rtlil(cell);
+
+		f << indent << "if (";
+		dump_sigspec_rhs(cell->getPort(ID::EN));
+		f << " == value<1>{1u}) {\n";
+		inc_indent();
+			dict<std::string, RTLIL::SigSpec> fmt_args;
+			f << indent << "struct : public lazy_fmt {\n";
+			inc_indent();
+				f << indent << "std::string operator() () const override {\n";
+				inc_indent();
+					fmt.emit_cxxrtl(f, indent, [&](const RTLIL::SigSpec &sig) {
+						if (sig.size() == 0)
+							f << "value<0>()";
+						else {
+							std::string arg_name = "arg" + std::to_string(fmt_args.size());
+							fmt_args[arg_name] = sig;
+							f << arg_name;
+						}
+					}, "performer");
+				dec_indent();
+				f << indent << "}\n";
+				f << indent << "struct performer *performer;\n";
+				for (auto arg : fmt_args)
+					f << indent << "value<" << arg.second.size() << "> " << arg.first << ";\n";
+			dec_indent();
+			f << indent << "} formatter;\n";
+			f << indent << "formatter.performer = performer;\n";
+			for (auto arg : fmt_args) {
+				f << indent << "formatter." << arg.first << " = ";
+				dump_sigspec_rhs(arg.second);
+				f << ";\n";
+			}
+			f << indent << "if (performer) {\n";
+			inc_indent();
+				f << indent << "static const metadata_map attributes = ";
+				dump_metadata_map(cell->attributes);
+				f << ";\n";
+				f << indent << "performer->on_print(formatter, attributes);\n";
+			dec_indent();
+			f << indent << "} else {\n";
+			inc_indent();
+				f << indent << print_output << " << formatter();\n";
+			dec_indent();
+			f << indent << "}\n";
+		dec_indent();
+		f << indent << "}\n";
+	}
+
+	void dump_effect(const RTLIL::Cell *cell)
+	{
+		Fmt fmt;
+		fmt.parse_rtlil(cell);
+
+		f << indent << "if (";
+		dump_sigspec_rhs(cell->getPort(ID::EN));
+		f << ") {\n";
+		inc_indent();
+			dict<std::string, RTLIL::SigSpec> fmt_args;
+			f << indent << "struct : public lazy_fmt {\n";
+			inc_indent();
+				f << indent << "std::string operator() () const override {\n";
+				inc_indent();
+					fmt.emit_cxxrtl(f, indent, [&](const RTLIL::SigSpec &sig) {
+						if (sig.size() == 0)
+							f << "value<0>()";
+						else {
+							std::string arg_name = "arg" + std::to_string(fmt_args.size());
+							fmt_args[arg_name] = sig;
+							f << arg_name;
+						}
+					}, "performer");
+				dec_indent();
+				f << indent << "}\n";
+				f << indent << "struct performer *performer;\n";
+				for (auto arg : fmt_args)
+					f << indent << "value<" << arg.second.size() << "> " << arg.first << ";\n";
+			dec_indent();
+			f << indent << "} formatter;\n";
+			f << indent << "formatter.performer = performer;\n";
+			for (auto arg : fmt_args) {
+				f << indent << "formatter." << arg.first << " = ";
+				dump_sigspec_rhs(arg.second);
+				f << ";\n";
+			}
+			if (cell->hasPort(ID::A)) {
+				f << indent << "bool condition = (bool)";
+				dump_sigspec_rhs(cell->getPort(ID::A));
+				f << ";\n";
+			}
+			f << indent << "if (performer) {\n";
+			inc_indent();
+				f << indent << "static const metadata_map attributes = ";
+				dump_metadata_map(cell->attributes);
+				f << ";\n";
+				if (cell->type == ID($print)) {
+					f << indent << "performer->on_print(formatter, attributes);\n";
+				} else if (cell->type == ID($check)) {
+					std::string flavor = cell->getParam(ID::FLAVOR).decode_string();
+					f << indent << "performer->on_check(";
+					if (flavor == "assert")
+						f << "flavor::ASSERT";
+					else if (flavor == "assume")
+						f << "flavor::ASSUME";
+					else if (flavor == "live")
+						f << "flavor::ASSERT_EVENTUALLY";
+					else if (flavor == "fair")
+						f << "flavor::ASSUME_EVENTUALLY";
+					else if (flavor == "cover")
+						f << "flavor::COVER";
+					else log_assert(false);
+					f << ", condition, formatter, attributes);\n";
+				} else log_assert(false);
+			dec_indent();
+			f << indent << "} else {\n";
+			inc_indent();
+				if (cell->type == ID($print)) {
+					f << indent << print_output << " << formatter();\n";
+				} else if (cell->type == ID($check)) {
+					std::string flavor = cell->getParam(ID::FLAVOR).decode_string();
+					if (flavor == "assert" || flavor == "assume") {
+						f << indent << "if (!condition) {\n";
+						inc_indent();
+							f << indent << "std::cerr << formatter();\n";
+						dec_indent();
+						f << indent << "}\n";
+						f << indent << "CXXRTL_ASSERT(condition && \"Check failed\");\n";
+					}
+				} else log_assert(false);
+			dec_indent();
+			f << indent << "}\n";
+		dec_indent();
+		f << indent << "}\n";
+	}
+
 	void dump_cell_eval(const RTLIL::Cell *cell, bool for_debug = false)
 	{
 		std::vector<const RTLIL::Cell*> inlined_cells;
@@ -1322,30 +1367,34 @@ struct CxxrtlWorker {
 			f << " = ";
 			dump_cell_expr(cell, for_debug);
 			f << ";\n";
-		// $print cell
-		} else if (cell->type == ID($print)) {
+		// Effectful cells
+		} else if (is_effectful_cell(cell->type)) {
 			log_assert(!for_debug);
 
-			// Sync $print cells are grouped into PRINT_SYNC nodes in the FlowGraph.
+			// Sync effectful cells are grouped into EFFECT_SYNC nodes in the FlowGraph.
 			log_assert(!cell->getParam(ID::TRG_ENABLE).as_bool() || (cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0));
 
-			if (!cell->getParam(ID::TRG_ENABLE).as_bool()) { // async $print cell
-				f << indent << "auto " << mangle(cell) << "_curr = ";
+			if (!cell->getParam(ID::TRG_ENABLE).as_bool()) { // async effectful cell
+				f << indent << "auto " << mangle(cell) << "_next = ";
 				dump_sigspec_rhs(cell->getPort(ID::EN));
 				f << ".concat(";
-				dump_sigspec_rhs(cell->getPort(ID::ARGS));
+				if (cell->type == ID($print))
+					dump_sigspec_rhs(cell->getPort(ID::ARGS));
+				else if (cell->type == ID($check))
+					dump_sigspec_rhs(cell->getPort(ID::A));
+				else log_assert(false);
 				f << ").val();\n";
 
-				f << indent << "if (" << mangle(cell) << " != " << mangle(cell) << "_curr) {\n";
+				f << indent << "if (" << mangle(cell) << " != " << mangle(cell) << "_next) {\n";
 				inc_indent();
-					dump_print(cell);
-					f << indent << mangle(cell) << " = " << mangle(cell) << "_curr;\n";
+					dump_effect(cell);
+					f << indent << mangle(cell) << " = " << mangle(cell) << "_next;\n";
 				dec_indent();
 				f << indent << "}\n";
-			} else { // initial $print cell
+			} else { // initial effectful cell
 				f << indent << "if (!" << mangle(cell) << ") {\n";
 				inc_indent();
-					dump_print(cell);
+					dump_effect(cell);
 					f << indent << mangle(cell) << " = value<1>{1u};\n";
 				dec_indent();
 				f << indent << "}\n";
@@ -1728,6 +1777,47 @@ struct CxxrtlWorker {
 		}
 	}
 
+	void dump_cell_effect_sync(std::vector<const RTLIL::Cell*> &cells)
+	{
+		log_assert(!cells.empty());
+		const auto &trg = cells[0]->getPort(ID::TRG);
+		const auto &trg_polarity = cells[0]->getParam(ID::TRG_POLARITY);
+
+		f << indent << "if (";
+		for (int i = 0; i < trg.size(); i++) {
+			RTLIL::SigBit trg_bit = trg[i];
+			trg_bit = sigmaps[trg_bit.wire->module](trg_bit);
+			log_assert(trg_bit.wire);
+
+			if (i != 0)
+				f << " || ";
+
+			if (trg_polarity[i] == State::S1)
+				f << "posedge_";
+			else
+				f << "negedge_";
+			f << mangle(trg_bit);
+		}
+		f << ") {\n";
+		inc_indent();
+			std::sort(cells.begin(), cells.end(), [](const RTLIL::Cell *a, const RTLIL::Cell *b) {
+				return a->getParam(ID::PRIORITY).as_int() > b->getParam(ID::PRIORITY).as_int();
+			});
+			for (auto cell : cells) {
+				log_assert(cell->getParam(ID::TRG_ENABLE).as_bool());
+				log_assert(cell->getPort(ID::TRG) == trg);
+				log_assert(cell->getParam(ID::TRG_POLARITY) == trg_polarity);
+
+				std::vector<const RTLIL::Cell*> inlined_cells;
+				collect_cell_eval(cell, /*for_debug=*/false, inlined_cells);
+				dump_inlined_cells(inlined_cells);
+				dump_effect(cell);
+			}
+		dec_indent();
+
+		f << indent << "}\n";
+	}
+
 	void dump_mem_rdport(const Mem *mem, int portidx, bool for_debug = false)
 	{
 		auto &port = mem->rd_ports[portidx];
@@ -2047,11 +2137,10 @@ struct CxxrtlWorker {
 				}
 			}
 			for (auto cell : module->cells()) {
-				// Certain $print cells have additional state, which must be reset as well.
-				if (cell->type == ID($print) && !cell->getParam(ID::TRG_ENABLE).as_bool())
-					f << indent << mangle(cell) << " = value<" << (1 + cell->getParam(ID::ARGS_WIDTH).as_int()) << ">();\n";
-				if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0)
-					f << indent << mangle(cell) << " = value<1>();\n";
+				// Async and initial effectful cells have additional state, which must be reset as well.
+				if (is_effectful_cell(cell->type))
+					if (!cell->getParam(ID::TRG_ENABLE).as_bool() || cell->getParam(ID::TRG_WIDTH).as_int() == 0)
+						f << indent << mangle(cell) << " = {};\n";
 				if (is_internal_cell(cell->type))
 					continue;
 				f << indent << mangle(cell);
@@ -2099,8 +2188,8 @@ struct CxxrtlWorker {
 						case FlowGraph::Node::Type::CELL_EVAL:
 							dump_cell_eval(node.cell);
 							break;
-						case FlowGraph::Node::Type::PRINT_SYNC:
-							dump_sync_print(node.print_sync_cells);
+						case FlowGraph::Node::Type::EFFECT_SYNC:
+							dump_cell_effect_sync(node.cells);
 							break;
 						case FlowGraph::Node::Type::PROCESS_CASE:
 							dump_process_case(node.process);
@@ -2481,11 +2570,15 @@ struct CxxrtlWorker {
 					f << "\n";
 				bool has_cells = false;
 				for (auto cell : module->cells()) {
-					// Certain $print cells have additional state, which requires storage.
-					if (cell->type == ID($print) && !cell->getParam(ID::TRG_ENABLE).as_bool())
-						f << indent << "value<" << (1 + cell->getParam(ID::ARGS_WIDTH).as_int()) << "> " << mangle(cell) << ";\n";
-					if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0)
-						f << indent << "value<1> " << mangle(cell) << ";\n";
+					// Async and initial effectful cells have additional state, which requires storage.
+					if (is_effectful_cell(cell->type)) {
+						if (cell->getParam(ID::TRG_ENABLE).as_bool() && cell->getParam(ID::TRG_WIDTH).as_int() == 0)
+							f << indent << "value<1> " << mangle(cell) << ";\n"; // async initial cell
+						if (!cell->getParam(ID::TRG_ENABLE).as_bool() && cell->type == ID($print))
+							f << indent << "value<" << (1 + cell->getParam(ID::ARGS_WIDTH).as_int()) << "> " << mangle(cell) << ";\n"; // {EN, ARGS}
+						if (!cell->getParam(ID::TRG_ENABLE).as_bool() && cell->type == ID($check))
+							f << indent << "value<2> " << mangle(cell) << ";\n"; // {EN, A}
+					}
 					if (is_internal_cell(cell->type))
 						continue;
 					dump_attrs(cell);
@@ -2803,8 +2896,8 @@ struct CxxrtlWorker {
 							cell->parameters[ID::CLK_POLARITY].as_bool() ? RTLIL::STp : RTLIL::STn);
 				}
 
-				// $print cells may be triggered on posedge/negedge events.
-				if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool()) {
+				// Effectful cells may be triggered on posedge/negedge events.
+				if (is_effectful_cell(cell->type) && cell->getParam(ID::TRG_ENABLE).as_bool()) {
 					for (size_t i = 0; i < (size_t)cell->getParam(ID::TRG_WIDTH).as_int(); i++) {
 						RTLIL::SigBit trg = cell->getPort(ID::TRG).extract(i, 1);
 						if (is_valid_clock(trg))
@@ -2945,10 +3038,12 @@ struct CxxrtlWorker {
 			// Discover nodes reachable from primary outputs (i.e. members) and collect reachable wire users.
 			pool<FlowGraph::Node*, hash_ptr_ops> worklist;
 			for (auto node : flow.nodes) {
-				if (node->type == FlowGraph::Node::Type::CELL_EVAL && is_effectful_cell(node->cell->type))
-					worklist.insert(node); // node has effects
-				else if (node->type == FlowGraph::Node::Type::PRINT_SYNC)
-					worklist.insert(node); // node is sync $print
+				if (node->type == FlowGraph::Node::Type::CELL_EVAL && !is_internal_cell(node->cell->type))
+					worklist.insert(node); // node evaluates a submodule
+				else if (node->type == FlowGraph::Node::Type::CELL_EVAL && is_effectful_cell(node->cell->type))
+					worklist.insert(node); // node has async effects
+				else if (node->type == FlowGraph::Node::Type::EFFECT_SYNC)
+					worklist.insert(node); // node has sync effects
 				else if (node->type == FlowGraph::Node::Type::MEM_WRPORTS)
 					worklist.insert(node); // node is memory write
 				else if (node->type == FlowGraph::Node::Type::PROCESS_SYNC && is_memwr_process(node->process))
@@ -3005,21 +3100,21 @@ struct CxxrtlWorker {
 			}
 
 			// Emit reachable nodes in eval().
-			// Accumulate sync $print cells per trigger condition.
-			dict<std::pair<RTLIL::SigSpec, RTLIL::Const>, std::vector<const RTLIL::Cell*>> sync_print_cells;
+			// Accumulate sync effectful cells per trigger condition.
+			dict<std::pair<RTLIL::SigSpec, RTLIL::Const>, std::vector<const RTLIL::Cell*>> effect_sync_cells;
 			for (auto node : node_order)
 				if (live_nodes[node]) {
 					if (node->type == FlowGraph::Node::Type::CELL_EVAL &&
-							node->cell->type == ID($print) &&
+							is_effectful_cell(node->cell->type) &&
 							node->cell->getParam(ID::TRG_ENABLE).as_bool() &&
 							node->cell->getParam(ID::TRG_WIDTH).as_int() != 0)
-						sync_print_cells[make_pair(node->cell->getPort(ID::TRG), node->cell->getParam(ID::TRG_POLARITY))].push_back(node->cell);
+						effect_sync_cells[make_pair(node->cell->getPort(ID::TRG), node->cell->getParam(ID::TRG_POLARITY))].push_back(node->cell);
 					else
 						schedule[module].push_back(*node);
 				}
 
-			for (auto &it : sync_print_cells) {
-				auto node = flow.add_print_sync_node(it.second);
+			for (auto &it : effect_sync_cells) {
+				auto node = flow.add_effect_sync_node(it.second);
 				schedule[module].push_back(*node);
 			}
 
diff --git a/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h b/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h
index 550571497..ee55011e8 100644
--- a/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h
+++ b/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h
@@ -952,7 +952,23 @@ struct lazy_fmt {
 	virtual std::string operator() () const = 0;
 };
 
-// An object that can be passed to a `eval()` method in order to act on side effects.
+// Flavor of a `$check` cell.
+enum class flavor {
+	// Corresponds to a `$assert` cell in other flows, and a Verilog `assert ()` statement.
+	ASSERT,
+	// Corresponds to a `$assume` cell in other flows, and a Verilog `assume ()` statement.
+	ASSUME,
+	// Corresponds to a `$live` cell in other flows, and a Verilog `assert (eventually)` statement.
+	ASSERT_EVENTUALLY,
+	// Corresponds to a `$fair` cell in other flows, and a Verilog `assume (eventually)` statement.
+	ASSUME_EVENTUALLY,
+	// Corresponds to a `$cover` cell in other flows, and a Verilog `cover ()` statement.
+	COVER,
+};
+
+// An object that can be passed to a `eval()` method in order to act on side effects. The default behavior implemented
+// below is the same as the behavior of `eval(nullptr)`, except that `-print-output` option of `write_cxxrtl` is not
+// taken into account.
 struct performer {
 	// Called by generated formatting code to evaluate a Verilog `$time` expression.
 	virtual int64_t vlog_time() const { return 0; }
@@ -964,6 +980,15 @@ struct performer {
 	virtual void on_print(const lazy_fmt &formatter, const metadata_map &attributes) {
 		std::cout << formatter();
 	}
+
+	// Called when a `$check` cell is triggered.
+	virtual void on_check(flavor type, bool condition, const lazy_fmt &formatter, const metadata_map &attributes) {
+		if (type == flavor::ASSERT || type == flavor::ASSUME) {
+			if (!condition)
+				std::cerr << formatter();
+			CXXRTL_ASSERT(condition && "Check failed");
+		}
+	}
 };
 
 // An object that can be passed to a `commit()` method in order to produce a replay log of every state change in
diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc
index 41e51f328..988eef658 100644
--- a/backends/verilog/verilog_backend.cc
+++ b/backends/verilog/verilog_backend.cc
@@ -1008,7 +1008,7 @@ void dump_cell_expr_binop(std::ostream &f, std::string indent, RTLIL::Cell *cell
 
 void dump_cell_expr_print(std::ostream &f, std::string indent, const RTLIL::Cell *cell)
 {
-	Fmt fmt = {};
+	Fmt fmt;
 	fmt.parse_rtlil(cell);
 	std::vector<VerilogFmtArg> args = fmt.emit_verilog();
 
@@ -1041,6 +1041,23 @@ void dump_cell_expr_print(std::ostream &f, std::string indent, const RTLIL::Cell
 	f << stringf(");\n");
 }
 
+void dump_cell_expr_check(std::ostream &f, std::string indent, const RTLIL::Cell *cell)
+{
+	std::string flavor = cell->getParam(ID(FLAVOR)).decode_string();
+	if (flavor == "assert")
+		f << stringf("%s" "assert (", indent.c_str());
+	else if (flavor == "assume")
+		f << stringf("%s" "assume (", indent.c_str());
+	else if (flavor == "live")
+		f << stringf("%s" "assert (eventually ", indent.c_str());
+	else if (flavor == "fair")
+		f << stringf("%s" "assume (eventually ", indent.c_str());
+	else if (flavor == "cover")
+		f << stringf("%s" "cover (", indent.c_str());
+	dump_sigspec(f, cell->getPort(ID::A));
+	f << stringf(");\n");
+}
+
 bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 {
 	if (cell->type == ID($_NOT_)) {
@@ -1814,6 +1831,39 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		return true;
 	}
 
+	if (cell->type == ID($check))
+	{
+		// Sync $check cells are accumulated and handled in dump_module.
+		if (cell->getParam(ID::TRG_ENABLE).as_bool())
+			return true;
+
+		f << stringf("%s" "always @*\n", indent.c_str());
+
+		f << stringf("%s" "  if (", indent.c_str());
+		dump_sigspec(f, cell->getPort(ID::EN));
+		f << stringf(") begin\n");
+
+		std::string flavor = cell->getParam(ID::FLAVOR).decode_string();
+		if (flavor == "assert" || flavor == "assume") {
+			Fmt fmt;
+			fmt.parse_rtlil(cell);
+			if (!fmt.parts.empty()) {
+				f << stringf("%s" "    if (!", indent.c_str());
+				dump_sigspec(f, cell->getPort(ID::A));
+				f << stringf(")\n");
+				dump_cell_expr_print(f, indent + "      ", cell);
+			}
+		} else {
+			f << stringf("%s" "  /* message omitted */\n", indent.c_str());
+		}
+
+		dump_cell_expr_check(f, indent + "    ", cell);
+
+		f << stringf("%s" "  end\n", indent.c_str());
+
+		return true;
+	}
+
 	// FIXME: $fsm
 
 	return false;
@@ -1903,7 +1953,7 @@ void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 	}
 }
 
-void dump_sync_print(std::ostream &f, std::string indent, const RTLIL::SigSpec &trg, const RTLIL::Const &polarity, std::vector<const RTLIL::Cell*> &cells)
+void dump_sync_effect(std::ostream &f, std::string indent, const RTLIL::SigSpec &trg, const RTLIL::Const &polarity, std::vector<const RTLIL::Cell*> &cells)
 {
 	if (trg.size() == 0) {
 		f << stringf("%s" "initial begin\n", indent.c_str());
@@ -1927,9 +1977,29 @@ void dump_sync_print(std::ostream &f, std::string indent, const RTLIL::SigSpec &
 	for (auto cell : cells) {
 		f << stringf("%s" "  if (", indent.c_str());
 		dump_sigspec(f, cell->getPort(ID::EN));
-		f << stringf(")\n");
+		f << stringf(") begin\n");
 
-		dump_cell_expr_print(f, indent + "    ", cell);
+		if (cell->type == ID($print)) {
+			dump_cell_expr_print(f, indent + "    ", cell);
+		} else if (cell->type == ID($check)) {
+			std::string flavor = cell->getParam(ID::FLAVOR).decode_string();
+			if (flavor == "assert" || flavor == "assume") {
+				Fmt fmt;
+				fmt.parse_rtlil(cell);
+				if (!fmt.parts.empty()) {
+					f << stringf("%s" "    if (!", indent.c_str());
+					dump_sigspec(f, cell->getPort(ID::A));
+					f << stringf(")\n");
+					dump_cell_expr_print(f, indent + "      ", cell);
+				}
+			} else {
+				f << stringf("%s" "  /* message omitted */\n", indent.c_str());
+			}
+
+			dump_cell_expr_check(f, indent + "    ", cell);
+		}
+
+		f << stringf("%s" "  end\n", indent.c_str());
 	}
 
 	f << stringf("%s" "end\n", indent.c_str());
@@ -2182,7 +2252,7 @@ void dump_process(std::ostream &f, std::string indent, RTLIL::Process *proc, boo
 
 void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 {
-	std::map<std::pair<RTLIL::SigSpec, RTLIL::Const>, std::vector<const RTLIL::Cell*>> sync_print_cells;
+	std::map<std::pair<RTLIL::SigSpec, RTLIL::Const>, std::vector<const RTLIL::Cell*>> sync_effect_cells;
 
 	reg_wires.clear();
 	reset_auto_counter(module);
@@ -2214,8 +2284,8 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 		std::set<std::pair<RTLIL::Wire*,int>> reg_bits;
 		for (auto cell : module->cells())
 		{
-			if (cell->type == ID($print) && cell->getParam(ID::TRG_ENABLE).as_bool()) {
-				sync_print_cells[make_pair(cell->getPort(ID::TRG), cell->getParam(ID::TRG_POLARITY))].push_back(cell);
+			if (cell->type.in(ID($print), ID($check)) && cell->getParam(ID::TRG_ENABLE).as_bool()) {
+				sync_effect_cells[make_pair(cell->getPort(ID::TRG), cell->getParam(ID::TRG_POLARITY))].push_back(cell);
 				continue;
 			}
 
@@ -2274,8 +2344,8 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
 	for (auto cell : module->cells())
 		dump_cell(f, indent + "  ", cell);
 
-	for (auto &it : sync_print_cells)
-		dump_sync_print(f, indent + "  ", it.first.first, it.first.second, it.second);
+	for (auto &it : sync_effect_cells)
+		dump_sync_effect(f, indent + "  ", it.first.first, it.first.second, it.second);
 
 	for (auto it = module->processes.begin(); it != module->processes.end(); ++it)
 		dump_process(f, indent + "  ", it->second);
diff --git a/docs/source/CHAPTER_CellLib.rst b/docs/source/CHAPTER_CellLib.rst
index 0f0d79123..3b6f1b4d3 100644
--- a/docs/source/CHAPTER_CellLib.rst
+++ b/docs/source/CHAPTER_CellLib.rst
@@ -621,7 +621,7 @@ Add information about ``$specify2``, ``$specify3``, and ``$specrule`` cells.
 Formal verification cells
 ~~~~~~~~~~~~~~~~~~~~~~~~~
 
-Add information about ``$assert``, ``$assume``, ``$live``, ``$fair``,
+Add information about ``$check``, ``$assert``, ``$assume``, ``$live``, ``$fair``,
 ``$cover``, ``$equiv``, ``$initstate``, ``$anyconst``, ``$anyseq``,
 ``$anyinit``, ``$allconst``, ``$allseq`` cells.
 
@@ -654,8 +654,8 @@ If ``\TRG_ENABLE`` is true, the following parameters also apply:
 	negative-edge triggered.
 
 ``\PRIORITY``
-	When multiple ``$print`` cells fire on the same trigger, they execute in
-	descending priority order.
+	When multiple ``$print`` or ``$$check`` cells fire on the same trigger, they\
+	execute in descending priority order.
 
 Ports:
 
diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc
index 0a502162e..03697ebf3 100644
--- a/frontends/ast/genrtlil.cc
+++ b/frontends/ast/genrtlil.cc
@@ -163,6 +163,28 @@ static RTLIL::SigSpec mux2rtlil(AstNode *that, const RTLIL::SigSpec &cond, const
 	return wire;
 }
 
+static void check_unique_id(RTLIL::Module *module, RTLIL::IdString id,
+		const AstNode *node, const char *to_add_kind)
+{
+	auto already_exists = [&](const RTLIL::AttrObject *existing, const char *existing_kind) {
+		std::string src = existing->get_string_attribute(ID::src);
+		std::string location_str = "earlier";
+		if (!src.empty())
+			location_str = "at " + src;
+		node->input_error("Cannot add %s `%s' because a %s with the same name was already created %s!\n",
+						  to_add_kind, id.c_str(), existing_kind, location_str.c_str());
+	};
+
+	if (const RTLIL::Wire *wire = module->wire(id))
+		already_exists(wire, "signal");
+	if (const RTLIL::Cell *cell = module->cell(id))
+		already_exists(cell, "cell");
+	if (module->processes.count(id))
+		already_exists(module->processes.at(id), "process");
+	if (module->memories.count(id))
+		already_exists(module->memories.at(id), "memory");
+}
+
 // helper class for rewriting simple lookahead references in AST always blocks
 struct AST_INTERNAL::LookaheadRewriter
 {
@@ -316,10 +338,10 @@ struct AST_INTERNAL::ProcessGenerator
 	// Buffer for generating the init action
 	RTLIL::SigSpec init_lvalue, init_rvalue;
 
-	// The most recently assigned $print cell \PRIORITY.
-	int last_print_priority;
+	// The most recently assigned $print or $check cell \PRIORITY.
+	int last_effect_priority;
 
-	ProcessGenerator(AstNode *always, RTLIL::SigSpec initSyncSignalsArg = RTLIL::SigSpec()) : always(always), initSyncSignals(initSyncSignalsArg), last_print_priority(0)
+	ProcessGenerator(AstNode *always, RTLIL::SigSpec initSyncSignalsArg = RTLIL::SigSpec()) : always(always), initSyncSignals(initSyncSignalsArg), last_effect_priority(0)
 	{
 		// rewrite lookahead references
 		LookaheadRewriter la_rewriter(always);
@@ -703,8 +725,10 @@ struct AST_INTERNAL::ProcessGenerator
 				std::stringstream sstr;
 				sstr << ast->str << "$" << ast->filename << ":" << ast->location.first_line << "$" << (autoidx++);
 
-				RTLIL::Cell *cell = current_module->addCell(sstr.str(), ID($print));
-				set_src_attr(cell, ast);
+				Wire *en = current_module->addWire(sstr.str() + "_EN", 1);
+				set_src_attr(en, ast);
+				proc->root_case.actions.push_back(SigSig(en, false));
+				current_case->actions.push_back(SigSig(en, true));
 
 				RTLIL::SigSpec triggers;
 				RTLIL::Const polarity;
@@ -717,18 +741,15 @@ struct AST_INTERNAL::ProcessGenerator
 						polarity.bits.push_back(RTLIL::S0);
 					}
 				}
-				cell->parameters[ID::TRG_WIDTH] = triggers.size();
-				cell->parameters[ID::TRG_ENABLE] = (always->type == AST_INITIAL) || !triggers.empty();
-				cell->parameters[ID::TRG_POLARITY] = polarity;
-				cell->parameters[ID::PRIORITY] = --last_print_priority;
+
+				RTLIL::Cell *cell = current_module->addCell(sstr.str(), ID($print));
+				set_src_attr(cell, ast);
+				cell->setParam(ID::TRG_WIDTH, triggers.size());
+				cell->setParam(ID::TRG_ENABLE, (always->type == AST_INITIAL) || !triggers.empty());
+				cell->setParam(ID::TRG_POLARITY, polarity);
+				cell->setParam(ID::PRIORITY, --last_effect_priority);
 				cell->setPort(ID::TRG, triggers);
-
-				Wire *wire = current_module->addWire(sstr.str() + "_EN", 1);
-				set_src_attr(wire, ast);
-				cell->setPort(ID::EN, wire);
-
-				proc->root_case.actions.push_back(SigSig(wire, false));
-				current_case->actions.push_back(SigSig(wire, true));
+				cell->setPort(ID::EN, en);
 
 				int default_base = 10;
 				if (ast->str.back() == 'b')
@@ -766,7 +787,7 @@ struct AST_INTERNAL::ProcessGenerator
 					args.push_back(arg);
 				}
 
-				Fmt fmt = {};
+				Fmt fmt;
 				fmt.parse_verilog(args, /*sformat_like=*/false, default_base, /*task_name=*/ast->str, current_module->name);
 				if (ast->str.substr(0, 8) == "$display")
 					fmt.append_string("\n");
@@ -776,6 +797,70 @@ struct AST_INTERNAL::ProcessGenerator
 			}
 			break;
 
+		// generate $check cells
+		case AST_ASSERT:
+		case AST_ASSUME:
+		case AST_LIVE:
+		case AST_FAIR:
+		case AST_COVER:
+			{
+				std::string flavor, desc;
+				if (ast->type == AST_ASSERT) { flavor = "assert"; desc = "assert ()"; }
+				if (ast->type == AST_ASSUME) { flavor = "assume"; desc = "assume ()"; }
+				if (ast->type == AST_LIVE) { flavor = "live"; desc = "assert (eventually)"; }
+				if (ast->type == AST_FAIR) { flavor = "fair"; desc = "assume (eventually)"; }
+				if (ast->type == AST_COVER) { flavor = "cover"; desc = "cover ()"; }
+
+				IdString cellname;
+				if (ast->str.empty())
+					cellname = stringf("$%s$%s:%d$%d", flavor.c_str(), RTLIL::encode_filename(ast->filename).c_str(), ast->location.first_line, autoidx++);
+				else
+					cellname = ast->str;
+				check_unique_id(current_module, cellname, ast, "procedural assertion");
+
+				RTLIL::SigSpec check = ast->children[0]->genWidthRTLIL(-1, false, &subst_rvalue_map.stdmap());
+				if (GetSize(check) != 1)
+					check = current_module->ReduceBool(NEW_ID, check);
+
+				Wire *en = current_module->addWire(cellname.str() + "_EN", 1);
+				set_src_attr(en, ast);
+				proc->root_case.actions.push_back(SigSig(en, false));
+				current_case->actions.push_back(SigSig(en, true));
+
+				RTLIL::SigSpec triggers;
+				RTLIL::Const polarity;
+				for (auto sync : proc->syncs) {
+					if (sync->type == RTLIL::STp) {
+						triggers.append(sync->signal);
+						polarity.bits.push_back(RTLIL::S1);
+					} else if (sync->type == RTLIL::STn) {
+						triggers.append(sync->signal);
+						polarity.bits.push_back(RTLIL::S0);
+					}
+				}
+
+				RTLIL::Cell *cell = current_module->addCell(cellname, ID($check));
+				set_src_attr(cell, ast);
+				for (auto &attr : ast->attributes) {
+					if (attr.second->type != AST_CONSTANT)
+						log_file_error(ast->filename, ast->location.first_line, "Attribute `%s' with non-constant value!\n", attr.first.c_str());
+					cell->attributes[attr.first] = attr.second->asAttrConst();
+				}
+				cell->setParam(ID::FLAVOR, flavor);
+				cell->setParam(ID::TRG_WIDTH, triggers.size());
+				cell->setParam(ID::TRG_ENABLE, (always->type == AST_INITIAL) || !triggers.empty());
+				cell->setParam(ID::TRG_POLARITY, polarity);
+				cell->setParam(ID::PRIORITY, --last_effect_priority);
+				cell->setPort(ID::TRG, triggers);
+				cell->setPort(ID::EN, en);
+				cell->setPort(ID::A, check);
+
+				// No message is emitted to ensure Verilog code roundtrips correctly.
+				Fmt fmt;
+				fmt.emit_rtlil(cell);
+				break;
+			}
+
 		case AST_NONE:
 		case AST_FOR:
 			break;
@@ -1242,28 +1327,6 @@ void AstNode::detectSignWidth(int &width_hint, bool &sign_hint, bool *found_real
 					width_hint, kWidthLimit);
 }
 
-static void check_unique_id(RTLIL::Module *module, RTLIL::IdString id,
-		const AstNode *node, const char *to_add_kind)
-{
-	auto already_exists = [&](const RTLIL::AttrObject *existing, const char *existing_kind) {
-		std::string src = existing->get_string_attribute(ID::src);
-		std::string location_str = "earlier";
-		if (!src.empty())
-			location_str = "at " + src;
-		node->input_error("Cannot add %s `%s' because a %s with the same name was already created %s!\n",
-						  to_add_kind, id.c_str(), existing_kind, location_str.c_str());
-	};
-
-	if (const RTLIL::Wire *wire = module->wire(id))
-		already_exists(wire, "signal");
-	if (const RTLIL::Cell *cell = module->cell(id))
-		already_exists(cell, "cell");
-	if (module->processes.count(id))
-		already_exists(module->processes.at(id), "process");
-	if (module->memories.count(id))
-		already_exists(module->memories.at(id), "memory");
-}
-
 // create RTLIL from an AST node
 // all generated cells, wires and processes are added to the module pointed to by 'current_module'
 // when the AST node is an expression (AST_ADD, AST_BIT_XOR, etc.), the result signal is returned.
@@ -1945,48 +2008,50 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 		}
 		break;
 
-	// generate $assert cells
+	// generate $check cells
 	case AST_ASSERT:
 	case AST_ASSUME:
 	case AST_LIVE:
 	case AST_FAIR:
 	case AST_COVER:
 		{
-			IdString celltype;
-			if (type == AST_ASSERT) celltype = ID($assert);
-			if (type == AST_ASSUME) celltype = ID($assume);
-			if (type == AST_LIVE) celltype = ID($live);
-			if (type == AST_FAIR) celltype = ID($fair);
-			if (type == AST_COVER) celltype = ID($cover);
+			std::string flavor, desc;
+			if (type == AST_ASSERT) { flavor = "assert"; desc = "assert property ()"; }
+			if (type == AST_ASSUME) { flavor = "assume"; desc = "assume property ()"; }
+			if (type == AST_LIVE) { flavor = "live"; desc = "assert property (eventually)"; }
+			if (type == AST_FAIR) { flavor = "fair"; desc = "assume property (eventually)"; }
+			if (type == AST_COVER) { flavor = "cover"; desc = "cover property ()"; }
 
-			log_assert(children.size() == 2);
+			IdString cellname;
+			if (str.empty())
+				cellname = stringf("$%s$%s:%d$%d", flavor.c_str(), RTLIL::encode_filename(filename).c_str(), location.first_line, autoidx++);
+			else
+				cellname = str;
+			check_unique_id(current_module, cellname, this, "procedural assertion");
 
 			RTLIL::SigSpec check = children[0]->genRTLIL();
 			if (GetSize(check) != 1)
 				check = current_module->ReduceBool(NEW_ID, check);
 
-			RTLIL::SigSpec en = children[1]->genRTLIL();
-			if (GetSize(en) != 1)
-				en = current_module->ReduceBool(NEW_ID, en);
-
-			IdString cellname;
-			if (str.empty())
-				cellname = stringf("%s$%s:%d$%d", celltype.c_str(), RTLIL::encode_filename(filename).c_str(), location.first_line, autoidx++);
-			else
-				cellname = str;
-
-			check_unique_id(current_module, cellname, this, "procedural assertion");
-			RTLIL::Cell *cell = current_module->addCell(cellname, celltype);
+			RTLIL::Cell *cell = current_module->addCell(cellname, ID($check));
 			set_src_attr(cell, this);
-
 			for (auto &attr : attributes) {
 				if (attr.second->type != AST_CONSTANT)
 					input_error("Attribute `%s' with non-constant value!\n", attr.first.c_str());
 				cell->attributes[attr.first] = attr.second->asAttrConst();
 			}
-
+			cell->setParam(ID(FLAVOR), flavor);
+			cell->parameters[ID::TRG_WIDTH] = 0;
+			cell->parameters[ID::TRG_ENABLE] = 0;
+			cell->parameters[ID::TRG_POLARITY] = 0;
+			cell->parameters[ID::PRIORITY] = 0;
+			cell->setPort(ID::TRG, RTLIL::SigSpec());
+			cell->setPort(ID::EN, RTLIL::S1);
 			cell->setPort(ID::A, check);
-			cell->setPort(ID::EN, en);
+
+			// No message is emitted to ensure Verilog code roundtrips correctly.
+			Fmt fmt;
+			fmt.emit_rtlil(cell);
 		}
 		break;
 
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index fa079f3e3..8e0de2994 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -178,7 +178,7 @@ Fmt AstNode::processFormat(int stage, bool sformat_like, int default_base, size_
 		args.push_back(arg);
 	}
 
-	Fmt fmt = {};
+	Fmt fmt;
 	fmt.parse_verilog(args, sformat_like, default_base, /*task_name=*/str, current_module->name);
 	return fmt;
 }
@@ -784,7 +784,7 @@ AstNode *AstNode::clone_at_zero()
 				pointee->type != AST_MEMORY)
 			break;
 
-		YS_FALLTHROUGH;
+		YS_FALLTHROUGH
 	case AST_MEMRD:
 		detectSignWidth(width_hint, sign_hint);
 		return mkconst_int(0, sign_hint, width_hint);
@@ -3039,97 +3039,6 @@ bool AstNode::simplify(bool const_fold, int stage, int width_hint, bool sign_hin
 	}
 skip_dynamic_range_lvalue_expansion:;
 
-	if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME || type == AST_LIVE || type == AST_FAIR || type == AST_COVER) && current_block != NULL)
-	{
-		std::stringstream sstr;
-		sstr << "$formal$" << RTLIL::encode_filename(filename) << ":" << location.first_line << "$" << (autoidx++);
-		std::string id_check = sstr.str() + "_CHECK", id_en = sstr.str() + "_EN";
-
-		AstNode *wire_check = new AstNode(AST_WIRE);
-		wire_check->str = id_check;
-		wire_check->was_checked = true;
-		current_ast_mod->children.push_back(wire_check);
-		current_scope[wire_check->str] = wire_check;
-		while (wire_check->simplify(true, 1, -1, false)) { }
-
-		AstNode *wire_en = new AstNode(AST_WIRE);
-		wire_en->str = id_en;
-		wire_en->was_checked = true;
-		current_ast_mod->children.push_back(wire_en);
-		if (current_always_clocked) {
-			current_ast_mod->children.push_back(new AstNode(AST_INITIAL, new AstNode(AST_BLOCK, new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), AstNode::mkconst_int(0, false, 1)))));
-			current_ast_mod->children.back()->children[0]->children[0]->children[0]->str = id_en;
-			current_ast_mod->children.back()->children[0]->children[0]->children[0]->was_checked = true;
-		}
-		current_scope[wire_en->str] = wire_en;
-		while (wire_en->simplify(true, 1, -1, false)) { }
-
-		AstNode *check_defval;
-		if (type == AST_LIVE || type == AST_FAIR) {
-			check_defval = new AstNode(AST_REDUCE_BOOL, children[0]->clone());
-		} else {
-			std::vector<RTLIL::State> x_bit;
-			x_bit.push_back(RTLIL::State::Sx);
-			check_defval = mkconst_bits(x_bit, false);
-		}
-
-		AstNode *assign_check = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), check_defval);
-		assign_check->children[0]->str = id_check;
-		assign_check->children[0]->was_checked = true;
-
-		AstNode *assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), mkconst_int(0, false, 1));
-		assign_en->children[0]->str = id_en;
-		assign_en->children[0]->was_checked = true;
-
-		AstNode *default_signals = new AstNode(AST_BLOCK);
-		default_signals->children.push_back(assign_check);
-		default_signals->children.push_back(assign_en);
-		current_top_block->children.insert(current_top_block->children.begin(), default_signals);
-
-		if (type == AST_LIVE || type == AST_FAIR) {
-			assign_check = nullptr;
-		} else {
-			assign_check = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), new AstNode(AST_REDUCE_BOOL, children[0]->clone()));
-			assign_check->children[0]->str = id_check;
-			assign_check->children[0]->was_checked = true;
-			assign_check->fixup_hierarchy_flags();
-		}
-
-		if (current_always == nullptr || current_always->type != AST_INITIAL) {
-			assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), mkconst_int(1, false, 1));
-		} else {
-			assign_en = new AstNode(AST_ASSIGN_LE, new AstNode(AST_IDENTIFIER), new AstNode(AST_FCALL));
-			assign_en->children[1]->str = "\\$initstate";
-		}
-		assign_en->children[0]->str = id_en;
-		assign_en->children[0]->was_checked = true;
-		assign_en->fixup_hierarchy_flags();
-
-		newNode = new AstNode(AST_BLOCK);
-		if (assign_check != nullptr)
-			newNode->children.push_back(assign_check);
-		newNode->children.push_back(assign_en);
-
-		AstNode *assertnode = new AstNode(type);
-		assertnode->location = location;
-		assertnode->str = str;
-		assertnode->children.push_back(new AstNode(AST_IDENTIFIER));
-		assertnode->children.push_back(new AstNode(AST_IDENTIFIER));
-		assertnode->children[0]->str = id_check;
-		assertnode->children[1]->str = id_en;
-		assertnode->attributes.swap(attributes);
-		current_ast_mod->children.push_back(assertnode);
-
-		goto apply_newNode;
-	}
-
-	if (stage > 1 && (type == AST_ASSERT || type == AST_ASSUME || type == AST_LIVE || type == AST_FAIR || type == AST_COVER) && children.size() == 1)
-	{
-		children.push_back(mkconst_int(1, false, 1));
-		fixup_hierarchy_flags();
-		did_something = true;
-	}
-
 	// found right-hand side identifier for memory -> replace with memory read port
 	if (stage > 1 && type == AST_IDENTIFIER && id2ast != NULL && id2ast->type == AST_MEMORY && !in_lvalue &&
 			children.size() == 1 && children[0]->type == AST_RANGE && children[0]->children.size() == 1) {
diff --git a/kernel/celltypes.h b/kernel/celltypes.h
index cad505d9a..77cb3e324 100644
--- a/kernel/celltypes.h
+++ b/kernel/celltypes.h
@@ -102,6 +102,7 @@ struct CellTypes
 		setup_type(ID($specify3), {ID::EN, ID::SRC, ID::DST, ID::DAT}, pool<RTLIL::IdString>(), true);
 		setup_type(ID($specrule), {ID::EN_SRC, ID::EN_DST, ID::SRC, ID::DST}, pool<RTLIL::IdString>(), true);
 		setup_type(ID($print), {ID::EN, ID::ARGS, ID::TRG}, pool<RTLIL::IdString>());
+		setup_type(ID($check), {ID::A, ID::EN, ID::ARGS, ID::TRG}, pool<RTLIL::IdString>());
 		setup_type(ID($set_tag), {ID::A, ID::SET, ID::CLR}, {ID::Y});
 		setup_type(ID($get_tag), {ID::A}, {ID::Y});
 		setup_type(ID($overwrite_tag), {ID::A, ID::SET, ID::CLR}, pool<RTLIL::IdString>());
diff --git a/kernel/constids.inc b/kernel/constids.inc
index 480e2afc6..7db21debb 100644
--- a/kernel/constids.inc
+++ b/kernel/constids.inc
@@ -88,6 +88,7 @@ X(equiv_merged)
 X(equiv_region)
 X(extract_order)
 X(F)
+X(FLAVOR)
 X(FORMAT)
 X(force_downto)
 X(force_upto)
diff --git a/kernel/rtlil.cc b/kernel/rtlil.cc
index f19da69e2..125730f29 100644
--- a/kernel/rtlil.cc
+++ b/kernel/rtlil.cc
@@ -1068,6 +1068,12 @@ namespace {
 				error(__LINE__);
 		}
 
+		std::string param_string(const RTLIL::IdString &name)
+		{
+			param(name);
+			return cell->parameters.at(name).decode_string();
+		}
+
 		void port(const RTLIL::IdString& name, int width)
 		{
 			auto it = cell->connections_.find(name);
@@ -1747,6 +1753,22 @@ namespace {
 				return;
 			}
 
+			if (cell->type == ID($check)) {
+				std::string flavor = param_string(ID(FLAVOR));
+				if (!(flavor == "assert" || flavor == "assume" || flavor == "live" || flavor == "fair" || flavor == "cover"))
+					error(__LINE__);
+				param(ID(FORMAT));
+				param_bool(ID::TRG_ENABLE);
+				param(ID::TRG_POLARITY);
+				param(ID::PRIORITY);
+				port(ID::A, 1);
+				port(ID::EN, 1);
+				port(ID::TRG, param(ID::TRG_WIDTH));
+				port(ID::ARGS, param(ID::ARGS_WIDTH));
+				check_expected();
+				return;
+			}
+
 			if (cell->type == ID($_BUF_))    { port(ID::A,1); port(ID::Y,1); check_expected(); return; }
 			if (cell->type == ID($_NOT_))    { port(ID::A,1); port(ID::Y,1); check_expected(); return; }
 			if (cell->type == ID($_AND_))    { port(ID::A,1); port(ID::B,1); port(ID::Y,1); check_expected(); return; }
diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc
index 69cc6fb91..90f890e80 100644
--- a/passes/hierarchy/hierarchy.cc
+++ b/passes/hierarchy/hierarchy.cc
@@ -671,7 +671,7 @@ bool set_keep_assert(std::map<RTLIL::Module*, bool> &cache, RTLIL::Module *mod)
 	if (cache.count(mod) == 0)
 		for (auto c : mod->cells()) {
 			RTLIL::Module *m = mod->design->module(c->type);
-			if ((m != nullptr && set_keep_assert(cache, m)) || c->type.in(ID($assert), ID($assume), ID($live), ID($fair), ID($cover)))
+			if ((m != nullptr && set_keep_assert(cache, m)) || c->type.in(ID($check), ID($assert), ID($assume), ID($live), ID($fair), ID($cover)))
 				return cache[mod] = true;
 		}
 	return cache[mod];
diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index a219e4708..ffb3052db 100644
--- a/passes/opt/opt_clean.cc
+++ b/passes/opt/opt_clean.cc
@@ -82,7 +82,7 @@ struct keep_cache_t
 		if (!ignore_specify && cell->type.in(ID($specify2), ID($specify3), ID($specrule)))
 			return true;
 
-		if (cell->type == ID($print))
+		if (cell->type == ID($print) || cell->type == ID($check))
 			return true;
 
 		if (cell->has_keep_attr())
diff --git a/techlibs/common/simlib.v b/techlibs/common/simlib.v
index fd804786f..930d2000b 100644
--- a/techlibs/common/simlib.v
+++ b/techlibs/common/simlib.v
@@ -1803,11 +1803,12 @@ endmodule
 
 module \$print (EN, TRG, ARGS);
 
+parameter PRIORITY = 0;
+
 parameter FORMAT = "";
 parameter ARGS_WIDTH = 0;
-parameter PRIORITY = 0;
-parameter TRG_ENABLE = 1;
 
+parameter TRG_ENABLE = 1;
 parameter TRG_WIDTH = 0;
 parameter TRG_POLARITY = 0;
 
@@ -1817,6 +1818,27 @@ input [ARGS_WIDTH-1:0] ARGS;
 
 endmodule
 
+// --------------------------------------------------------
+
+module \$check (A, EN, TRG, ARGS);
+
+parameter FLAVOR = "";
+parameter PRIORITY = 0;
+
+parameter FORMAT = "";
+parameter ARGS_WIDTH = 0;
+
+parameter TRG_ENABLE = 1;
+parameter TRG_WIDTH = 0;
+parameter TRG_POLARITY = 0;
+
+input A;
+input EN;
+input [TRG_WIDTH-1:0] TRG;
+input [ARGS_WIDTH-1:0] ARGS;
+
+endmodule
+
 // --------------------------------------------------------
 `ifndef SIMLIB_NOSR