Merge pull request #17 from YosysHQ/master

bump fork for version 0.38

.github/workflows/codeql.yml

@@ -14,10 +14,10 @@ jobs:
       run: sudo apt-get install bison flex libreadline-dev tcl-dev libffi-dev
 
     - name: Checkout repository
-      uses: actions/checkout@v3
+      uses: actions/checkout@v4
 
     - name: Initialize CodeQL
-      uses: github/codeql-action/init@v2
+      uses: github/codeql-action/init@v3
       with:
         languages: cpp
         queries: security-extended,security-and-quality
@@ -26,4 +26,4 @@ jobs:
       run: make yosys -j6
 
     - name: Perform CodeQL Analysis
-      uses: github/codeql-action/analyze@v2
+      uses: github/codeql-action/analyze@v3

.github/workflows/emcc.yml

@@ -6,13 +6,13 @@ jobs:
   emcc:
     runs-on: ubuntu-latest
     steps:
-      - uses: mymindstorm/setup-emsdk@v11
-      - uses: actions/checkout@v3
+      - uses: mymindstorm/setup-emsdk@v14
+      - uses: actions/checkout@v4
       - name: Build
         run: |
           make config-emcc
           make YOSYS_VER=latest
-      - uses: actions/upload-artifact@v3
+      - uses: actions/upload-artifact@v4
         with:
           name: yosysjs
           path: yosysjs-latest.zip

.github/workflows/test-linux.yml

@@ -79,19 +79,19 @@ jobs:
           $CXX --version
 
       - name: Checkout Yosys
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Get iverilog
         shell: bash
         run: |
           git clone https://github.com/steveicarus/iverilog.git
           cd iverilog
-          git checkout ${{ vars.IVERILOG_VERSION }}
+          git checkout 192b6aec96fde982e6ddcb28b346d5893aa8e874
           echo "IVERILOG_GIT=$(git rev-parse HEAD)" >> $GITHUB_ENV
 
       - name: Cache iverilog
         id: cache-iverilog
-        uses: actions/cache@v3
+        uses: actions/cache@v4
         with:
           path: .local/
           key: ${{ matrix.os.id }}-${{ env.IVERILOG_GIT }}
@@ -111,10 +111,14 @@ jobs:
         shell: bash
         run: |
           make config-${CC%%-*}
-          make -j${{ env.procs }} CCXXSTD=${{ matrix.cpp_std }} CC=$CC CXX=$CC LD=$CC
+          make -j${{ env.procs }} CXXSTD=${{ matrix.cpp_std }} CC=$CC CXX=$CC LD=$CC
 
       - name: Run tests
         if: (matrix.cpp_std == 'c++11') && (matrix.compiler == 'gcc-11')
         shell: bash
         run: |
           make -j${{ env.procs }} test CXXSTD=${{ matrix.cpp_std }} CC=$CC CXX=$CC LD=$CC
+
+      - name: Log yosys-config output
+        run: |
+          ./yosys-config || true

.github/workflows/test-macos.yml

@@ -35,19 +35,19 @@ jobs:
           cc --version
 
       - name: Checkout Yosys
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
 
       - name: Get iverilog
         shell: bash
         run: |
           git clone https://github.com/steveicarus/iverilog.git
           cd iverilog
-          git checkout ${{ vars.IVERILOG_VERSION }}
+          git checkout 192b6aec96fde982e6ddcb28b346d5893aa8e874
           echo "IVERILOG_GIT=$(git rev-parse HEAD)" >> $GITHUB_ENV
 
       - name: Cache iverilog
         id: cache-iverilog
-        uses: actions/cache@v3
+        uses: actions/cache@v4
         with:
           path: .local/
           key: ${{ matrix.os.id }}-${{ env.IVERILOG_GIT }}

.github/workflows/version.yml

@@ -10,7 +10,7 @@ jobs:
     runs-on: ubuntu-latest
     steps:
       - name: Checkout
-        uses: actions/checkout@v3
+        uses: actions/checkout@v4
         with:
           fetch-depth: 0
       - name: Take last commit

.github/workflows/vs.yml

@@ -6,10 +6,10 @@ jobs:
   yosys-vcxsrc:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Build
         run: make vcxsrc YOSYS_VER=latest
-      - uses: actions/upload-artifact@v3
+      - uses: actions/upload-artifact@v4
         with:
           name: vcxsrc
           path: yosys-win32-vcxsrc-latest.zip
@@ -18,7 +18,7 @@ jobs:
     runs-on: windows-2019
     needs: yosys-vcxsrc
     steps:  
-      - uses: actions/download-artifact@v3
+      - uses: actions/download-artifact@v4
         with:
           name: vcxsrc
           path: .

.github/workflows/wasi.yml

@@ -6,7 +6,7 @@ jobs:
   wasi:
     runs-on: ubuntu-latest
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - name: Build
         run: |
           WASI_SDK=wasi-sdk-19.0

CHANGELOG

@@ -2,9 +2,28 @@
 List of major changes and improvements between releases
 =======================================================
 
-Yosys 0.37 .. Yosys 0.38-dev
+Yosys 0.38 .. Yosys 0.39-dev
 --------------------------
 
+Yosys 0.37 .. Yosys 0.38
+--------------------------
+ * New commands and options
+    - Added option "-tech" to "opt_lut" pass.
+    - Added option "-nokeep_prints" to "hierarchy" pass.
+    - Added option "-nolower" to "async2sync" and "clk2fflogic" pass.
+    - Added option "-lower" to "chformal" pass.
+
+ * Various
+    - Added $check cell to represent assertions with messages.
+    - Allow capturing $print cell output in CXXRTL.
+    - Added API to overwrite existing pass from plugin.
+    - Follow the XDG Base Directory Specification for storing history files.
+    - Without a known top module, derive all deferred modules (hierarchy pass).
+    - Detect and error out on combinational loops in write_aiger.
+
+ * Verific support
+    - Added option "-no-split-complex-ports" to "verific -import".
+
 Yosys 0.36 .. Yosys 0.37
 --------------------------
  * New commands and options

Makefile

@@ -141,7 +141,7 @@ LDLIBS += -lrt
 endif
 endif
 
-YOSYS_VER := 0.37+27
+YOSYS_VER := 0.38+46
 
 # Note: We arrange for .gitcommit to contain the (short) commit hash in
 # tarballs generated with git-archive(1) using .gitattributes. The git repo
@@ -157,7 +157,7 @@ endif
 OBJS = kernel/version_$(GIT_REV).o
 
 bumpversion:
-	sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline a5c7f69.. | wc -l`/;" Makefile
+	sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 543faed.. | wc -l`/;" Makefile
 
 # set 'ABCREV = default' to use abc/ as it is
 #
@@ -630,6 +630,7 @@ $(eval $(call add_include_file,kernel/qcsat.h))
 $(eval $(call add_include_file,kernel/register.h))
 $(eval $(call add_include_file,kernel/rtlil.h))
 $(eval $(call add_include_file,kernel/satgen.h))
+$(eval $(call add_include_file,kernel/scopeinfo.h))
 $(eval $(call add_include_file,kernel/sigtools.h))
 $(eval $(call add_include_file,kernel/timinginfo.h))
 $(eval $(call add_include_file,kernel/utils.h))
@@ -656,7 +657,7 @@ $(eval $(call add_include_file,backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi_v
 
 OBJS += kernel/driver.o kernel/register.o kernel/rtlil.o kernel/log.o kernel/calc.o kernel/yosys.o
 OBJS += kernel/binding.o
-OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o kernel/yw.o kernel/json.o kernel/fmt.o
+OBJS += kernel/cellaigs.o kernel/celledges.o kernel/satgen.o kernel/scopeinfo.o kernel/qcsat.o kernel/mem.o kernel/ffmerge.o kernel/ff.o kernel/yw.o kernel/json.o kernel/fmt.o
 ifeq ($(ENABLE_ZLIB),1)
 OBJS += kernel/fstdata.o
 endif
@@ -679,12 +680,8 @@ OBJS += libs/bigint/BigUnsigned.o libs/bigint/BigUnsignedInABase.o
 
 OBJS += libs/sha1/sha1.o
 
-ifneq ($(SMALL),1)
-
 OBJS += libs/json11/json11.o
 
-OBJS += libs/subcircuit/subcircuit.o
-
 OBJS += libs/ezsat/ezsat.o
 OBJS += libs/ezsat/ezminisat.o
 
@@ -699,6 +696,10 @@ OBJS += libs/fst/fastlz.o
 OBJS += libs/fst/lz4.o
 endif
 
+ifneq ($(SMALL),1)
+
+OBJS += libs/subcircuit/subcircuit.o
+
 include $(YOSYS_SRC)/frontends/*/Makefile.inc
 include $(YOSYS_SRC)/passes/*/Makefile.inc
 include $(YOSYS_SRC)/backends/*/Makefile.inc
@@ -707,6 +708,9 @@ include $(YOSYS_SRC)/techlibs/*/Makefile.inc
 else
 
 include $(YOSYS_SRC)/frontends/verilog/Makefile.inc
+ifeq ($(ENABLE_VERIFIC),1)
+include $(YOSYS_SRC)/frontends/verific/Makefile.inc
+endif
 include $(YOSYS_SRC)/frontends/rtlil/Makefile.inc
 include $(YOSYS_SRC)/frontends/ast/Makefile.inc
 include $(YOSYS_SRC)/frontends/blif/Makefile.inc
@@ -844,9 +848,22 @@ else
 ABCOPT=""
 endif
 
+# When YOSYS_NOVERIFIC is set as a make variable, also export it to the
+# enviornment, so that `YOSYS_NOVERIFIC=1 make test` _and_
+# `make test YOSYS_NOVERIFIC=1` will run with verific disabled.
+ifeq ($(YOSYS_NOVERIFIC),1)
+export YOSYS_NOVERIFIC
+endif
+
 test: $(TARGETS) $(EXTRA_TARGETS)
 ifeq ($(ENABLE_VERIFIC),1)
+ifeq ($(YOSYS_NOVERIFIC),1)
+	@echo
+	@echo "Running tests without verific support due to YOSYS_NOVERIFIC=1"
+	@echo
+else
 	+cd tests/verific && bash run-test.sh $(SEEDOPT)
+endif
 endif
 	+cd tests/simple && bash run-test.sh $(SEEDOPT)
 	+cd tests/simple_abc9 && bash run-test.sh $(SEEDOPT)

README.md

@@ -587,7 +587,13 @@ from SystemVerilog:
 - enums are supported (including inside packages)
 	- but are currently not strongly typed
 
-- packed structs and unions are supported.
+- packed structs and unions are supported
+	- arrays of packed structs/unions are currently not supported
+	- structure literals are currently not supported
+
+- multidimensional arrays are supported
+	- array assignment of unpacked arrays is currently not supported
+	- array literals are currently not supported
 
 - SystemVerilog interfaces (SVIs) are supported. Modports for specifying whether
   ports are inputs or outputs are supported.

backends/aiger/aiger.cc

@@ -54,6 +54,8 @@ struct AigerWriter
 
 	vector<pair<int, int>> aig_gates;
 	vector<int> aig_latchin, aig_latchinit, aig_outputs;
+	vector<SigBit> bit2aig_stack;
+	size_t next_loop_check = 1024;
 	int aig_m = 0, aig_i = 0, aig_l = 0, aig_o = 0, aig_a = 0;
 	int aig_b = 0, aig_c = 0, aig_j = 0, aig_f = 0;
 
@@ -81,6 +83,23 @@ struct AigerWriter
 			return it->second;
 		}
 
+		if (bit2aig_stack.size() == next_loop_check) {
+			for (size_t i = 0; i < next_loop_check; ++i)
+			{
+				SigBit report_bit = bit2aig_stack[i];
+				if (report_bit != bit)
+					continue;
+				for (size_t j = i; j < next_loop_check; ++j) {
+					report_bit = bit2aig_stack[j];
+					if (report_bit.is_wire() && report_bit.wire->name.isPublic())
+						break;
+				}
+				log_error("Found combinational logic loop while processing signal %s.\n", log_signal(report_bit));
+			}
+			next_loop_check *= 2;
+		}
+		bit2aig_stack.push_back(bit);
+
 		// NB: Cannot use iterator returned from aig_map.insert()
 		//     since this function is called recursively
 
@@ -101,6 +120,8 @@ struct AigerWriter
 			a = initstate_ff;
 		}
 
+		bit2aig_stack.pop_back();
+
 		if (bit == State::Sx || bit == State::Sz)
 			log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n");
 
@@ -299,6 +320,9 @@ struct AigerWriter
 				continue;
 			}
 
+			if (cell->type == ID($scopeinfo))
+				continue;
+
 			log_error("Unsupported cell type: %s (%s)\n", log_id(cell->type), log_id(cell));
 		}
 

backends/blif/blif.cc

@@ -226,6 +226,9 @@ struct BlifDumper
 
 		for (auto cell : module->cells())
 		{
+			if (cell->type == ID($scopeinfo))
+				continue;
+
 			if (config->unbuf_types.count(cell->type)) {
 				auto portnames = config->unbuf_types.at(cell->type);
 				f << stringf(".names %s %s\n1 1\n",

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";
@@ -1446,7 +1495,7 @@ struct CxxrtlWorker {
 				f << indent;
 				dump_sigspec_lhs(cell->getPort(ID::Q));
 				f << " = ";
-				dump_sigspec_lhs(cell->getPort(ID::Q));
+				dump_sigspec_rhs(cell->getPort(ID::Q));
 				f << ".update(";
 				dump_const(RTLIL::Const(RTLIL::S1, cell->getParam(ID::WIDTH).as_int()));
 				f << ", ";
@@ -1458,7 +1507,7 @@ struct CxxrtlWorker {
 				f << indent;
 				dump_sigspec_lhs(cell->getPort(ID::Q));
 				f << " = ";
-				dump_sigspec_lhs(cell->getPort(ID::Q));
+				dump_sigspec_rhs(cell->getPort(ID::Q));
 				f << ".update(";
 				dump_const(RTLIL::Const(RTLIL::S0, cell->getParam(ID::WIDTH).as_int()));
 				f << ", ";
@@ -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);
 			}
 

backends/cxxrtl/runtime/cxxrtl/capi/cxxrtl_capi.h

@@ -240,6 +240,11 @@ struct cxxrtl_object {
 	// through wires, the bits are double buffered. To avoid race conditions, user code should
 	// always read from `curr` and write to `next`. The `curr` pointer is always valid; for objects
 	// that cannot be modified, or cannot be modified in a race-free way, `next` is NULL.
+	//
+	// In case where `width == 0`, `curr` is a non-NULL pointer unique for the wire. That is,
+	// there is a 1-to-1 correspondence between simulation objects and `curr` pointers, regardless
+	// of whether they have storage or not. (Aliases' `curr` pointer equals that of some other
+	// simulated object.)
 	uint32_t *curr;
 	uint32_t *next;
 

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
@@ -1151,7 +1176,7 @@ struct debug_item : ::cxxrtl_object {
 
 	template<size_t Bits>
 	debug_item(value<Bits> &item, size_t lsb_offset = 0, uint32_t flags_ = 0) {
-		static_assert(sizeof(item) == value<Bits>::chunks * sizeof(chunk_t),
+		static_assert(Bits == 0 || sizeof(item) == value<Bits>::chunks * sizeof(chunk_t),
 		              "value<Bits> is not compatible with C layout");
 		type    = VALUE;
 		flags   = flags_;
@@ -1167,7 +1192,7 @@ struct debug_item : ::cxxrtl_object {
 
 	template<size_t Bits>
 	debug_item(const value<Bits> &item, size_t lsb_offset = 0) {
-		static_assert(sizeof(item) == value<Bits>::chunks * sizeof(chunk_t),
+		static_assert(Bits == 0 || sizeof(item) == value<Bits>::chunks * sizeof(chunk_t),
 		              "value<Bits> is not compatible with C layout");
 		type    = VALUE;
 		flags   = DRIVEN_COMB;
@@ -1183,8 +1208,9 @@ struct debug_item : ::cxxrtl_object {
 
 	template<size_t Bits>
 	debug_item(wire<Bits> &item, size_t lsb_offset = 0, uint32_t flags_ = 0) {
-		static_assert(sizeof(item.curr) == value<Bits>::chunks * sizeof(chunk_t) &&
-		              sizeof(item.next) == value<Bits>::chunks * sizeof(chunk_t),
+		static_assert(Bits == 0 ||
+		              (sizeof(item.curr) == value<Bits>::chunks * sizeof(chunk_t) &&
+		               sizeof(item.next) == value<Bits>::chunks * sizeof(chunk_t)),
 		              "wire<Bits> is not compatible with C layout");
 		type    = WIRE;
 		flags   = flags_;
@@ -1200,7 +1226,7 @@ struct debug_item : ::cxxrtl_object {
 
 	template<size_t Width>
 	debug_item(memory<Width> &item, size_t zero_offset = 0) {
-		static_assert(sizeof(item.data[0]) == value<Width>::chunks * sizeof(chunk_t),
+		static_assert(Width == 0 || sizeof(item.data[0]) == value<Width>::chunks * sizeof(chunk_t),
 		              "memory<Width> is not compatible with C layout");
 		type    = MEMORY;
 		flags   = 0;
@@ -1216,7 +1242,7 @@ struct debug_item : ::cxxrtl_object {
 
 	template<size_t Bits>
 	debug_item(debug_alias, const value<Bits> &item, size_t lsb_offset = 0) {
-		static_assert(sizeof(item) == value<Bits>::chunks * sizeof(chunk_t),
+		static_assert(Bits == 0 || sizeof(item) == value<Bits>::chunks * sizeof(chunk_t),
 		              "value<Bits> is not compatible with C layout");
 		type    = ALIAS;
 		flags   = DRIVEN_COMB;
@@ -1232,8 +1258,9 @@ struct debug_item : ::cxxrtl_object {
 
 	template<size_t Bits>
 	debug_item(debug_alias, const wire<Bits> &item, size_t lsb_offset = 0) {
-		static_assert(sizeof(item.curr) == value<Bits>::chunks * sizeof(chunk_t) &&
-		              sizeof(item.next) == value<Bits>::chunks * sizeof(chunk_t),
+		static_assert(Bits == 0 ||
+		              (sizeof(item.curr) == value<Bits>::chunks * sizeof(chunk_t) &&
+		               sizeof(item.next) == value<Bits>::chunks * sizeof(chunk_t)),
 		              "wire<Bits> is not compatible with C layout");
 		type    = ALIAS;
 		flags   = DRIVEN_COMB;
@@ -1249,7 +1276,7 @@ struct debug_item : ::cxxrtl_object {
 
 	template<size_t Bits>
 	debug_item(debug_outline &group, const value<Bits> &item, size_t lsb_offset = 0) {
-		static_assert(sizeof(item) == value<Bits>::chunks * sizeof(chunk_t),
+		static_assert(Bits == 0 || sizeof(item) == value<Bits>::chunks * sizeof(chunk_t),
 		              "value<Bits> is not compatible with C layout");
 		type    = OUTLINE;
 		flags   = DRIVEN_COMB;
@@ -1293,6 +1320,14 @@ namespace cxxrtl {
 using debug_attrs = ::_cxxrtl_attr_set;
 
 struct debug_items {
+	// Debug items may be composed of multiple parts, but the attributes are shared between all of them.
+	// There are additional invariants, not all of which are not checked by this code:
+	// - Memories and non-memories cannot be mixed together.
+	// - Bit indices (considering `lsb_at` and `width`) must not overlap.
+	// - Row indices (considering `depth` and `zero_at`) must be the same.
+	// - The `INPUT` and `OUTPUT` flags must be the same for all parts.
+	// Other than that, the parts can be quite different, e.g. it is OK to mix a value, a wire, an alias,
+	// and an outline, in the debug information for a single name in four parts.
 	std::map<std::string, std::vector<debug_item>> table;
 	std::map<std::string, std::unique_ptr<debug_attrs>> attrs_table;
 
@@ -1317,29 +1352,32 @@ struct debug_items {
 		return table.at(name).size();
 	}
 
-	const std::vector<debug_item> &parts_at(const std::string &name) const {
+	const std::vector<debug_item> &at(const std::string &name) const {
 		return table.at(name);
 	}
 
-	const debug_item &at(const std::string &name) const {
+	// Like `at()`, but operates only on single-part debug items.
+	const debug_item &operator [](const std::string &name) const {
 		const std::vector<debug_item> &parts = table.at(name);
 		assert(parts.size() == 1);
 		return parts.at(0);
 	}
 
-	const debug_item &operator [](const std::string &name) const {
-		return at(name);
-	}
-
 	const metadata_map &attrs(const std::string &name) const {
 		return attrs_table.at(name)->map;
 	}
 };
 
-// Tag class to disambiguate the default constructor used by the toplevel module that calls reset(),
+// Tag class to disambiguate the default constructor used by the toplevel module that calls `reset()`,
 // and the constructor of interior modules that should not call it.
 struct interior {};
 
+// The core API of the `module` class consists of only four virtual methods: `reset()`, `eval()`,
+// `commit`, and `debug_info()`. (The virtual destructor is made necessary by C++.) Every other method
+// is a convenience method, and exists solely to simplify some common pattern for C++ API consumers.
+// No behavior may be added to such convenience methods that other parts of CXXRTL can rely on, since
+// there is no guarantee they will be called (and, for example, other CXXRTL libraries will often call
+// the `eval()` and `commit()` directly instead, as well as being exposed in the C API).
 struct module {
 	module() {}
 	virtual ~module() {}
@@ -1355,8 +1393,14 @@ struct module {
 
 	virtual void reset() = 0;
 
+	// The `eval()` callback object, `performer`, is included in the virtual call signature since
+	// the generated code has broadly identical performance properties.
 	virtual bool eval(performer *performer = nullptr) = 0;
-	virtual bool commit() = 0; // commit observer isn't available since it avoids virtual calls
+
+	// The `commit()` callback object, `observer`, is not included in the virtual call signature since
+	// the generated code is severely pessimized by it. To observe commit events, the non-virtual
+	// `commit(observer *)` overload must be called directly on a `module` subclass.
+	virtual bool commit() = 0;
 
 	size_t step(performer *performer = nullptr) {
 		size_t deltas = 0;

backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h

@@ -641,7 +641,7 @@ public:
 			assert(items.count(name) != 0);
 			assert(part_index < items.count(name));
 
-			const debug_item &part = items.parts_at(name).at(part_index);
+			const debug_item &part = items.at(name).at(part_index);
 			assert(chunks == (part.width + sizeof(chunk_t) * 8 - 1) / (sizeof(chunk_t) * 8));
 			assert(depth == part.depth);
 

backends/edif/edif.cc

@@ -213,6 +213,9 @@ struct EdifBackend : public Backend {
 
 			for (auto cell : module->cells())
 			{
+				if (cell->type == ID($scopeinfo))
+					continue;
+
 				if (design->module(cell->type) == nullptr || design->module(cell->type)->get_blackbox_attribute()) {
 					lib_cell_ports[cell->type];
 					for (auto p : cell->connections())

backends/firrtl/firrtl.cc

@@ -980,6 +980,9 @@ struct FirrtlWorker
 				register_reverse_wire_map(y_id, cell->getPort(ID::Y));
 				continue;
 			}
+
+			if (cell->type == ID($scopeinfo))
+				continue;
 			log_error("Cell type not supported: %s (%s.%s)\n", log_id(cell->type), log_id(module), log_id(cell));
 		}
 

backends/json/json.cc

@@ -192,6 +192,10 @@ struct JsonWriter
 		for (auto c : module->cells()) {
 			if (use_selection && !module->selected(c))
 				continue;
+			// Eventually we will want to emit $scopeinfo, but currently this
+			// will break JSON netlist consumers like nextpnr
+			if (c->type == ID($scopeinfo))
+				continue;
 			f << stringf("%s\n", first ? "" : ",");
 			f << stringf("        %s: {\n", get_name(c->name).c_str());
 			f << stringf("          \"hide_name\": %s,\n", c->name[0] == '$' ? "1" : "0");

backends/smv/smv.cc

@@ -573,6 +573,9 @@ struct SmvWorker
 				continue;
 			}
 
+			if (cell->type == ID($scopeinfo))
+				continue;
+
 			if (cell->type[0] == '$') {
 				if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) {
 					log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smv`.\n",

backends/spice/spice.cc

@@ -72,6 +72,9 @@ static void print_spice_module(std::ostream &f, RTLIL::Module *module, RTLIL::De
 
 	for (auto cell : module->cells())
 	{
+		if (cell->type == ID($scopeinfo))
+			continue;
+
 		f << stringf("X%d", cell_counter++);
 
 		std::vector<RTLIL::SigSpec> port_sigs;

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_)) {
@@ -1053,6 +1070,15 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 		f << stringf(";\n");
 		return true;
 	}
+	
+	if (cell->type == ID($_BUF_)) {
+		f << stringf("%s" "assign ", indent.c_str());
+		dump_sigspec(f, cell->getPort(ID::Y));
+		f << stringf(" = ");
+		dump_cell_expr_port(f, cell, "A", false);
+		f << stringf(";\n");
+		return true;
+	}
 
 	if (cell->type.in(ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_), ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_))) {
 		f << stringf("%s" "assign ", indent.c_str());
@@ -1805,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;
@@ -1812,6 +1871,13 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 
 void dump_cell(std::ostream &f, std::string indent, RTLIL::Cell *cell)
 {
+	// To keep the output compatible with other tools we ignore $scopeinfo
+	// cells that exist only to hold metadata. If in the future that metadata
+	// should be exposed as part of the write_verilog output it should be
+	// opt-in and/or represented as something else than a $scopeinfo cell.
+	if (cell->type == ID($scopeinfo))
+		return;
+
 	// Handled by dump_memory
 	if (cell->is_mem_cell())
 		return;
@@ -1894,7 +1960,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());
@@ -1918,9 +1984,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());
@@ -1949,13 +2035,8 @@ void dump_conn(std::ostream &f, std::string indent, const RTLIL::SigSpec &left,
 
 void dump_proc_switch(std::ostream &f, std::string indent, RTLIL::SwitchRule *sw);
 
-void dump_case_body(std::ostream &f, std::string indent, RTLIL::CaseRule *cs, bool omit_trailing_begin = false)
+void dump_case_actions(std::ostream &f, std::string indent, RTLIL::CaseRule *cs)
 {
-	int number_of_stmts = cs->switches.size() + cs->actions.size();
-
-	if (!omit_trailing_begin && number_of_stmts >= 2)
-		f << stringf("%s" "begin\n", indent.c_str());
-
 	for (auto it = cs->actions.begin(); it != cs->actions.end(); ++it) {
 		if (it->first.size() == 0)
 			continue;
@@ -1965,15 +2046,6 @@ void dump_case_body(std::ostream &f, std::string indent, RTLIL::CaseRule *cs, bo
 		dump_sigspec(f, it->second);
 		f << stringf(";\n");
 	}
-
-	for (auto it = cs->switches.begin(); it != cs->switches.end(); ++it)
-		dump_proc_switch(f, indent + "  ", *it);
-
-	if (!omit_trailing_begin && number_of_stmts == 0)
-		f << stringf("%s  /* empty */;\n", indent.c_str());
-
-	if (omit_trailing_begin || number_of_stmts >= 2)
-		f << stringf("%s" "end\n", indent.c_str());
 }
 
 bool dump_proc_switch_ifelse(std::ostream &f, std::string indent, RTLIL::SwitchRule *sw)
@@ -1996,36 +2068,52 @@ bool dump_proc_switch_ifelse(std::ostream &f, std::string indent, RTLIL::SwitchR
 		}
 	}
 
+	dump_attributes(f, indent, sw->attributes);
 	f << indent;
 	auto sig_it = sw->signal.begin();
 	for (auto it = sw->cases.begin(); it != sw->cases.end(); ++it, ++sig_it) {
-		bool had_newline = true;
 		if (it != sw->cases.begin()) {
-			if ((*it)->compare.empty()) {
-				f << indent << "else\n";
-				had_newline = true;
-			} else {
-				f << indent << "else ";
-				had_newline = false;
-			}
+			if ((*it)->compare.empty())
+				f << " else begin\n";
+			else
+				f << " else ";
 		}
 		if (!(*it)->compare.empty()) {
-			if (!(*it)->attributes.empty()) {
-				if (!had_newline)
-					f << "\n" << indent;
-				dump_attributes(f, "", (*it)->attributes, "\n" + indent);
-			}
 			f << stringf("if (");
 			dump_sigspec(f, *sig_it);
-			f << stringf(")\n");
+			f << stringf(") begin\n");
 		}
-		dump_case_body(f, indent, *it);
+
+		dump_case_actions(f, indent, (*it));
+		for (auto it2 = (*it)->switches.begin(); it2 != (*it)->switches.end(); ++it2)
+			dump_proc_switch(f, indent + "  ", *it2);
+
+		f << indent << "end";
 		if ((*it)->compare.empty())
 			break;
 	}
+	f << "\n";
 	return true;
 }
 
+void dump_case_body(std::ostream &f, std::string indent, RTLIL::CaseRule *cs, bool omit_trailing_begin = false)
+{
+	int number_of_stmts = cs->switches.size() + cs->actions.size();
+
+	if (!omit_trailing_begin && number_of_stmts >= 2)
+		f << stringf("%s" "begin\n", indent.c_str());
+
+	dump_case_actions(f, indent, cs);
+	for (auto it = cs->switches.begin(); it != cs->switches.end(); ++it)
+		dump_proc_switch(f, indent + "  ", *it);
+
+	if (!omit_trailing_begin && number_of_stmts == 0)
+		f << stringf("%s  /* empty */;\n", indent.c_str());
+
+	if (omit_trailing_begin || number_of_stmts >= 2)
+		f << stringf("%s" "end\n", indent.c_str());
+}
+
 void dump_proc_switch(std::ostream &f, std::string indent, RTLIL::SwitchRule *sw)
 {
 	if (sw->signal.size() == 0) {
@@ -2171,7 +2259,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);
@@ -2203,8 +2291,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;
 			}
 
@@ -2263,8 +2351,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);

docs/source/CHAPTER_Basics.rst

@@ -503,7 +503,7 @@ This process is illustrated in :numref:`Fig. %s <fig:Basics_flow>`.
 	:name: fig:Basics_flow
 
 	Typical design flow.  Green boxes represent manually created models.
-	Orange boxes represent modesl generated by synthesis tools.
+	Orange boxes represent models generated by synthesis tools.
 
 
 In this example the System Level Model and the Behavioural Model are both

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:
 

examples/cxx-api/scopeinfo_example.cc

@@ -0,0 +1,144 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2023  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.
+ *
+ */
+
+// build: yosys-config --build scopeinfo_example.so scopeinfo_example.cc
+// use: yosys -m scopeinfo_example.so
+
+#include "backends/rtlil/rtlil_backend.h"
+#include "kernel/scopeinfo.h"
+#include "kernel/yosys.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct ScopeinfoExamplePass : public Pass {
+	ScopeinfoExamplePass() : Pass("scopeinfo_example", "dump scopeinfo") {}
+	void help() override
+	{
+		//   |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+		log("\n");
+		log("    scopeinfo_example [options] [selection]\n");
+		log("\n");
+	}
+
+	void execute(std::vector<std::string> args, RTLIL::Design *design) override
+	{
+		log_header(design, "Executing SCOPEINFO_EXAMPLE pass.\n");
+
+		bool do_wires = false;
+		bool do_common = false;
+
+		size_t argidx;
+		for (argidx = 1; argidx < args.size(); argidx++) {
+			if (args[argidx] == "-wires") {
+				do_wires = true;
+				continue;
+			}
+			if (args[argidx] == "-common") {
+				do_common = true;
+				continue;
+			}
+			break;
+		}
+		extra_args(args, argidx, design);
+
+
+		if (do_wires) {
+			for (auto module : design->selected_modules()) {
+				log("Source hierarchy for all selected wires within %s:\n", log_id(module));
+				ModuleHdlnameIndex index(module);
+
+				index.index_scopeinfo_cells();
+
+				for (auto wire : module->selected_wires()) {
+					if (!wire->name.isPublic())
+						continue;
+
+					auto wire_scope = index.containing_scope(wire);
+
+					if (!wire_scope.first.valid()) {
+						log_warning("Couldn't find containing scope for %s in index\n", log_id(wire));
+						continue;
+					}
+
+					log("%s %s\n", wire_scope.first.path_str().c_str(), log_id(wire_scope.second));
+					for (auto src : index.sources(wire))
+						log(" - %s\n", src.c_str());
+				}
+			}
+		}
+
+		if (do_common) {
+			for (auto module : design->selected_modules()) {
+				std::vector<Wire *> wires = module->selected_wires();
+
+				// Shuffle wires so this example produces more interesting outputs
+				std::sort(wires.begin(), wires.end(), [](Wire *a, Wire *b) {
+					return mkhash_xorshift(a->name.hash() * 0x2c9277b5) < mkhash_xorshift(b->name.hash() * 0x2c9277b5);
+				});
+
+				ModuleHdlnameIndex index(module);
+
+				index.index_scopeinfo_cells();
+
+				for (auto wire_i = wires.begin(), wire_end = wires.end(); wire_i != wire_end; ++wire_i) {
+					if (!(*wire_i)->name.isPublic())
+						continue;
+
+					std::pair<ModuleHdlnameIndex::Cursor, IdString> scope_i = index.containing_scope(*wire_i);
+					if (!scope_i.first.valid())
+						continue;
+
+					int limit = 0;
+
+					for (auto wire_j = wire_i + 1; wire_j != wire_end; ++wire_j) {
+						if (!(*wire_j)->name.isPublic())
+							continue;
+
+						std::pair<ModuleHdlnameIndex::Cursor, IdString> scope_j = index.containing_scope(*wire_j);
+						if (!scope_j.first.valid())
+							continue;
+
+						// Skip wires in the same hierarchy level
+						if (scope_i.first == scope_j.first)
+							continue;
+
+
+						ModuleHdlnameIndex::Cursor common = scope_i.first.common_ancestor(scope_j.first);
+
+						// Try to show at least some non-root common ancestors
+						if (common.is_root() && limit > 5)
+							continue;
+
+						log("common_ancestor(%s %s%s%s, %s %s%s%s) = %s %s\n",
+							log_id(module), scope_i.first.path_str().c_str(), scope_i.first.is_root() ? "" : " ", log_id(scope_i.second),
+							log_id(module), scope_j.first.path_str().c_str(), scope_j.first.is_root() ? "" : " ", log_id(scope_j.second),
+							log_id(module), common.path_str().c_str()
+						);
+
+						if (++limit == 10)
+							break;
+					}
+				}
+			}
+		}
+	}
+} ScopeinfoExamplePass;
+
+PRIVATE_NAMESPACE_END

frontends/ast/ast.cc

@@ -224,6 +224,7 @@ AstNode::AstNode(AstNodeType type, AstNode *child1, AstNode *child2, AstNode *ch
 	port_id = 0;
 	range_left = -1;
 	range_right = 0;
+	unpacked_dimensions = 0;
 	integer = 0;
 	realvalue = 0;
 	id2ast = NULL;
@@ -349,17 +350,15 @@ void AstNode::dumpAst(FILE *f, std::string indent) const
 		fprintf(f, " int=%u", (int)integer);
 	if (realvalue != 0)
 		fprintf(f, " real=%e", realvalue);
-	if (!multirange_dimensions.empty()) {
-		fprintf(f, " multirange=[");
-		for (int v : multirange_dimensions)
-			fprintf(f, " %d", v);
-		fprintf(f, " ]");
-	}
-	if (!multirange_swapped.empty()) {
-		fprintf(f, " multirange_swapped=[");
-		for (bool v : multirange_swapped)
-			fprintf(f, " %d", v);
-		fprintf(f, " ]");
+	if (!dimensions.empty()) {
+		fprintf(f, " dimensions=");
+		for (auto &dim : dimensions) {
+			int left = dim.range_right + dim.range_width - 1;
+			int right = dim.range_right;
+			if (dim.range_swapped)
+				std::swap(left, right);
+			fprintf(f, "[%d:%d]", left, right);
+		}
 	}
 	if (is_enum) {
 		fprintf(f, " type=enum");
@@ -489,6 +488,20 @@ void AstNode::dumpVlog(FILE *f, std::string indent) const
 		fprintf(f, ";\n");
 		break;
 
+	if (0) { case AST_MEMRD:   txt = "@memrd@";  }
+	if (0) { case AST_MEMINIT: txt = "@meminit@";  }
+	if (0) { case AST_MEMWR:   txt = "@memwr@";  }
+		fprintf(f, "%s%s", indent.c_str(), txt.c_str());
+		for (auto child : children) {
+			fprintf(f, first ? "(" : ", ");
+			child->dumpVlog(f, "");
+			first = false;
+		}
+		fprintf(f, ")");
+		if (type != AST_MEMRD)
+			fprintf(f, ";\n");
+		break;
+
 	case AST_RANGE:
 		if (range_valid) {
 			if (range_swapped)
@@ -505,6 +518,11 @@ void AstNode::dumpVlog(FILE *f, std::string indent) const
 		}
 		break;
 
+	case AST_MULTIRANGE:
+		for (auto child : children)
+			child->dumpVlog(f, "");
+		break;
+
 	case AST_ALWAYS:
 		fprintf(f, "%s" "always @", indent.c_str());
 		for (auto child : children) {
@@ -542,7 +560,7 @@ void AstNode::dumpVlog(FILE *f, std::string indent) const
 
 	case AST_IDENTIFIER:
 		{
-			AST::AstNode *member_node = AST::get_struct_member(this);
+			AstNode *member_node = get_struct_member();
 			if (member_node)
 				fprintf(f, "%s[%d:%d]", id2vl(str).c_str(), member_node->range_left, member_node->range_right);
 			else
@@ -552,6 +570,12 @@ void AstNode::dumpVlog(FILE *f, std::string indent) const
 			child->dumpVlog(f, "");
 		break;
 
+	case AST_STRUCT:
+	case AST_UNION:
+	case AST_STRUCT_ITEM:
+		fprintf(f, "%s", id2vl(str).c_str());
+		break;
+
 	case AST_CONSTANT:
 		if (!str.empty())
 			fprintf(f, "\"%s\"", str.c_str());

frontends/ast/ast.h

@@ -202,9 +202,17 @@ namespace AST
 		// set for IDs typed to an enumeration, not used
 		bool is_enum;
 
-		// if this is a multirange memory then this vector contains offset and length of each dimension
-		std::vector<int> multirange_dimensions;
-		std::vector<bool> multirange_swapped; // true if range is swapped
+		// Declared range for array dimension.
+		struct dimension_t {
+			int range_right;     // lsb in [msb:lsb]
+			int range_width;     // msb - lsb + 1
+			bool range_swapped;  // if the declared msb < lsb, msb and lsb above are swapped
+		};
+		// Packed and unpacked dimensions for arrays.
+		// Unpacked dimensions go first, to follow the order of indexing.
+		std::vector<dimension_t> dimensions;
+		// Number of unpacked dimensions.
+		int unpacked_dimensions;
 
 		// this is set by simplify and used during RTLIL generation
 		AstNode *id2ast;
@@ -371,6 +379,10 @@ namespace AST
 		// localized fixups after modifying children/attributes of a particular node
 		void fixup_hierarchy_flags(bool force_descend = false);
 
+		// helpers for indexing
+		AstNode *make_index_range(AstNode *node, bool unpacked_range = false);
+		AstNode *get_struct_member() const;
+
 		// helper to print errors from simplify/genrtlil code
 		[[noreturn]] void input_error(const char *format, ...) const YS_ATTRIBUTE(format(printf, 2, 3));
 	};
@@ -416,10 +428,6 @@ namespace AST
 	// Helper for setting the src attribute.
 	void set_src_attr(RTLIL::AttrObject *obj, const AstNode *ast);
 
-	// struct helper exposed from simplify for genrtlil
-	AstNode *make_struct_member_range(AstNode *node, AstNode *member_node);
-	AstNode *get_struct_member(const AstNode *node);
-
 	// generate standard $paramod... derived module name; parameters should be
 	// in the order they are declared in the instantiated module
 	std::string derived_module_name(std::string stripped_name, const std::vector<std::pair<RTLIL::IdString, RTLIL::Const>> &parameters);

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;
@@ -960,7 +1045,7 @@ void AstNode::detectSignWidthWorker(int &width_hint, bool &sign_hint, bool *foun
 			if (children.size() > 1)
 				range = children[1];
 		} else if (id_ast->type == AST_STRUCT_ITEM || id_ast->type == AST_STRUCT || id_ast->type == AST_UNION) {
-			AstNode *tmp_range = make_struct_member_range(this, id_ast);
+			AstNode *tmp_range = make_index_range(id_ast);
 			this_width = tmp_range->range_left - tmp_range->range_right + 1;
 			delete tmp_range;
 		} else
@@ -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.
@@ -1521,7 +1584,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
 			chunk.width = wire->width;
 			chunk.offset = 0;
 
-			if ((member_node = get_struct_member(this))) {
+			if ((member_node = get_struct_member())) {
 				// Clamp wire chunk to range of member within struct/union.
 				chunk.width = member_node->range_left - member_node->range_right + 1;
 				chunk.offset = member_node->range_right;
@@ -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;
 

frontends/blif/blifparse.cc

@@ -256,6 +256,16 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool
 				continue;
 			}
 
+			if (!strcmp(cmd, ".area") || !strcmp(cmd, ".delay") || !strcmp(cmd, ".wire_load_slope") || !strcmp(cmd, ".wire") ||
+			    !strcmp(cmd, ".input_arrival") || !strcmp(cmd, ".default_input_arrival") || !strcmp(cmd, ".output_required") ||
+			    !strcmp(cmd, ".default_output_required") || !strcmp(cmd, ".input_drive") || !strcmp(cmd, ".default_input_drive") ||
+			    !strcmp(cmd, ".max_input_load") || !strcmp(cmd, ".default_max_input_load") || !strcmp(cmd, ".output_load") ||
+			    !strcmp(cmd, ".default_output_load"))
+			{
+				log_warning("Blif delay constraints (%s) are not supported.", cmd);
+				continue;
+			}
+
 			if (!strcmp(cmd, ".inputs") || !strcmp(cmd, ".outputs"))
 			{
 				char *p;

frontends/verific/verific.cc

@@ -343,36 +343,46 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att
 	}
 }
 
+RTLIL::SigBit VerificImporter::netToSigBit(Verific::Net *net) {
+	if (net && net->IsGnd())
+		return RTLIL::State::S0;
+	else if (net && net->IsPwr())
+		return RTLIL::State::S1;
+	else if (net && net->IsX())
+		return RTLIL::State::Sx;
+	else if (net)
+		return net_map_at(net);
+	else
+		return RTLIL::State::Sz;
+}
+
 RTLIL::SigSpec VerificImporter::operatorInput(Instance *inst)
 {
 	RTLIL::SigSpec sig;
-	for (int i = int(inst->InputSize())-1; i >= 0; i--)
-		if (inst->GetInputBit(i))
-			sig.append(net_map_at(inst->GetInputBit(i)));
-		else
-			sig.append(RTLIL::State::Sz);
+	for (int i = int(inst->InputSize())-1; i >= 0; i--) {
+		Net *net = inst->GetInputBit(i);
+		sig.append(netToSigBit(net));
+	}
 	return sig;
 }
 
 RTLIL::SigSpec VerificImporter::operatorInput1(Instance *inst)
 {
 	RTLIL::SigSpec sig;
-	for (int i = int(inst->Input1Size())-1; i >= 0; i--)
-		if (inst->GetInput1Bit(i))
-			sig.append(net_map_at(inst->GetInput1Bit(i)));
-		else
-			sig.append(RTLIL::State::Sz);
+	for (int i = int(inst->Input1Size())-1; i >= 0; i--) {
+		Net *net = inst->GetInput1Bit(i);
+		sig.append(netToSigBit(net));
+	}
 	return sig;
 }
 
 RTLIL::SigSpec VerificImporter::operatorInput2(Instance *inst)
 {
 	RTLIL::SigSpec sig;
-	for (int i = int(inst->Input2Size())-1; i >= 0; i--)
-		if (inst->GetInput2Bit(i))
-			sig.append(net_map_at(inst->GetInput2Bit(i)));
-		else
-			sig.append(RTLIL::State::Sz);
+	for (int i = int(inst->Input2Size())-1; i >= 0; i--) {
+		Net *net = inst->GetInput2Bit(i);
+		sig.append(netToSigBit(net));
+	}
 	return sig;
 }
 
@@ -1980,6 +1990,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
 		}
 
 		RTLIL::Cell *cell = module->addCell(inst_name, inst_type);
+		import_attributes(cell->attributes, inst);
 
 		if (inst->IsPrimitive() && mode_keep)
 			cell->attributes[ID::keep] = 1;
@@ -2815,6 +2826,9 @@ struct VerificPass : public Pass {
 		log("  -extnets\n");
 		log("    Resolve references to external nets by adding module ports as needed.\n");
 		log("\n");
+		log("  -no-split-complex-ports\n");
+		log("    Complex ports (structs or arrays) are not split and remain packed as a single port.\n");
+		log("\n");
 		log("  -autocover\n");
 		log("    Generate automatic cover statements for all asserts\n");
 		log("\n");
@@ -3548,6 +3562,7 @@ struct VerificPass : public Pass {
 			bool mode_nosva = false, mode_names = false, mode_verific = false;
 			bool mode_autocover = false, mode_fullinit = false;
 			bool flatten = false, extnets = false, mode_cells = false;
+			bool split_complex_ports = true;
 			string dumpfile;
 			string ppfile;
 			Map parameters(STRING_HASH);
@@ -3565,6 +3580,10 @@ struct VerificPass : public Pass {
 					flatten = true;
 					continue;
 				}
+				if (args[argidx] == "-no-split-complex-ports") {
+					split_complex_ports = false;
+					continue;
+				}
 				if (args[argidx] == "-extnets") {
 					extnets = true;
 					continue;
@@ -3804,8 +3823,10 @@ struct VerificPass : public Pass {
 					worker.run(nl.second);
 			}
 
-			for (auto nl : nl_todo)
-				nl.second->ChangePortBusStructures(1 /* hierarchical */);
+			if (split_complex_ports) {
+				for (auto nl : nl_todo)
+					nl.second->ChangePortBusStructures(1 /* hierarchical */);
+			}
 
 			if (!dumpfile.empty()) {
 				VeriWrite veri_writer;

frontends/verific/verific.h

@@ -83,6 +83,7 @@ struct VerificImporter
 	RTLIL::IdString new_verific_id(Verific::DesignObj *obj);
 	void import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, Verific::DesignObj *obj, Verific::Netlist  *nl = nullptr);
 
+	RTLIL::SigBit netToSigBit(Verific::Net *net);
 	RTLIL::SigSpec operatorInput(Verific::Instance *inst);
 	RTLIL::SigSpec operatorInput1(Verific::Instance *inst);
 	RTLIL::SigSpec operatorInput2(Verific::Instance *inst);

frontends/verilog/verilog_parser.y

@@ -197,9 +197,20 @@ static AstNode *checkRange(AstNode *type_node, AstNode *range_node)
 			range_node = makeRange(type_node->range_left, type_node->range_right, false);
 		}
 	}
-	if (range_node && range_node->children.size() != 2) {
-		frontend_verilog_yyerror("wire/reg/logic packed dimension must be of the form: [<expr>:<expr>], [<expr>+:<expr>], or [<expr>-:<expr>]");
+
+	if (range_node) {
+		bool valid = true;
+		if (range_node->type == AST_RANGE) {
+			valid = range_node->children.size() == 2;
+		} else {  // AST_MULTIRANGE
+			for (auto child : range_node->children) {
+				valid = valid && child->children.size() == 2;
+			}
+		}
+		if (!valid)
+			frontend_verilog_yyerror("wire/reg/logic packed dimension must be of the form [<expr>:<expr>]");
 	}
+
 	return range_node;
 }
 
@@ -672,7 +683,7 @@ module_arg:
 		ast_stack.back()->children.push_back(astbuf2);
 		delete astbuf1; // really only needed if multiple instances of same type.
 	} module_arg_opt_assignment |
-	attr wire_type range TOK_ID {
+	attr wire_type range_or_multirange TOK_ID {
 		AstNode *node = $2;
 		node->str = *$4;
 		SET_AST_NODE_LOC(node, @4, @4);
@@ -1165,7 +1176,7 @@ task_func_args:
 	task_func_port | task_func_args ',' task_func_port;
 
 task_func_port:
-	attr wire_type range {
+	attr wire_type range_or_multirange {
 		bool prev_was_input = true;
 		bool prev_was_output = false;
 		if (albuf) {
@@ -1889,10 +1900,11 @@ struct_member_type: { astbuf1 = new AstNode(AST_STRUCT_ITEM); } member_type_toke
 	;
 
 member_type_token:
-	  member_type
-	| hierarchical_type_id {
-			addWiretypeNode($1, astbuf1);
-		}
+	member_type range_or_multirange {
+		AstNode *range = checkRange(astbuf1, $2);
+		if (range)
+			astbuf1->children.push_back(range);
+	}
 	| {
 		delete astbuf1;
 	} struct_union {
@@ -1908,7 +1920,8 @@ member_type_token:
 	;
 
 member_type: type_atom type_signing
-	| type_vec type_signing range_or_multirange	{ if ($3) astbuf1->children.push_back($3); }
+	| type_vec type_signing
+	| hierarchical_type_id { addWiretypeNode($1, astbuf1); }
 	;
 
 struct_var_list: struct_var
@@ -1928,7 +1941,7 @@ struct_var: TOK_ID	{	auto *var_node = astbuf2->clone();
 /////////
 
 wire_decl:
-	attr wire_type range {
+	attr wire_type range_or_multirange {
 		albuf = $1;
 		astbuf1 = $2;
 		astbuf2 = checkRange(astbuf1, $3);
@@ -2104,14 +2117,14 @@ type_name: TOK_ID		// first time seen
 	 ;
 
 typedef_decl:
-	TOK_TYPEDEF typedef_base_type range type_name range_or_multirange ';' {
+	TOK_TYPEDEF typedef_base_type range_or_multirange type_name range_or_multirange ';' {
 		astbuf1 = $2;
 		astbuf2 = checkRange(astbuf1, $3);
 		if (astbuf2)
 			astbuf1->children.push_back(astbuf2);
 
 		if ($5 != NULL) {
-			if (!astbuf2) {
+			if (!astbuf2 && !astbuf1->is_custom_type) {
 				addRange(astbuf1, 0, 0, false);
 			}
 			rewriteAsMemoryNode(astbuf1, $5);
@@ -2484,7 +2497,7 @@ assert:
 			delete $5;
 		} else {
 			AstNode *node = new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5);
-			SET_AST_NODE_LOC(node, @1, @6);
+			SET_AST_NODE_LOC(node, ($1 != nullptr ? @1 : @2), @6);
 			if ($1 != nullptr)
 				node->str = *$1;
 			ast_stack.back()->children.push_back(node);
@@ -2497,7 +2510,7 @@ assert:
 			delete $5;
 		} else {
 			AstNode *node = new AstNode(assert_assumes_mode ? AST_ASSERT : AST_ASSUME, $5);
-			SET_AST_NODE_LOC(node, @1, @6);
+			SET_AST_NODE_LOC(node, ($1 != nullptr ? @1 : @2), @6);
 			if ($1 != nullptr)
 				node->str = *$1;
 			ast_stack.back()->children.push_back(node);
@@ -2510,7 +2523,7 @@ assert:
 			delete $6;
 		} else {
 			AstNode *node = new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6);
-			SET_AST_NODE_LOC(node, @1, @7);
+			SET_AST_NODE_LOC(node, ($1 != nullptr ? @1 : @2), @7);
 			if ($1 != nullptr)
 				node->str = *$1;
 			ast_stack.back()->children.push_back(node);
@@ -2523,7 +2536,7 @@ assert:
 			delete $6;
 		} else {
 			AstNode *node = new AstNode(assert_assumes_mode ? AST_LIVE : AST_FAIR, $6);
-			SET_AST_NODE_LOC(node, @1, @7);
+			SET_AST_NODE_LOC(node, ($1 != nullptr ? @1 : @2), @7);
 			if ($1 != nullptr)
 				node->str = *$1;
 			ast_stack.back()->children.push_back(node);
@@ -2533,7 +2546,7 @@ assert:
 	} |
 	opt_sva_label TOK_COVER opt_property '(' expr ')' ';' {
 		AstNode *node = new AstNode(AST_COVER, $5);
-		SET_AST_NODE_LOC(node, @1, @6);
+		SET_AST_NODE_LOC(node, ($1 != nullptr ? @1 : @2), @6);
 		if ($1 != nullptr) {
 			node->str = *$1;
 			delete $1;
@@ -2542,7 +2555,7 @@ assert:
 	} |
 	opt_sva_label TOK_COVER opt_property '(' ')' ';' {
 		AstNode *node = new AstNode(AST_COVER, AstNode::mkconst_int(1, false));
-		SET_AST_NODE_LOC(node, @1, @5);
+		SET_AST_NODE_LOC(node, ($1 != nullptr ? @1 : @2), @5);
 		if ($1 != nullptr) {
 			node->str = *$1;
 			delete $1;
@@ -2551,7 +2564,7 @@ assert:
 	} |
 	opt_sva_label TOK_COVER ';' {
 		AstNode *node = new AstNode(AST_COVER, AstNode::mkconst_int(1, false));
-		SET_AST_NODE_LOC(node, @1, @2);
+		SET_AST_NODE_LOC(node, ($1 != nullptr ? @1 : @2), @2);
 		if ($1 != nullptr) {
 			node->str = *$1;
 			delete $1;
@@ -2563,7 +2576,7 @@ assert:
 			delete $5;
 		} else {
 			AstNode *node = new AstNode(AST_ASSUME, $5);
-			SET_AST_NODE_LOC(node, @1, @6);
+			SET_AST_NODE_LOC(node, ($1 != nullptr ? @1 : @2), @6);
 			if ($1 != nullptr)
 				node->str = *$1;
 			ast_stack.back()->children.push_back(node);
@@ -2578,7 +2591,7 @@ assert:
 			delete $6;
 		} else {
 			AstNode *node = new AstNode(AST_FAIR, $6);
-			SET_AST_NODE_LOC(node, @1, @7);
+			SET_AST_NODE_LOC(node, ($1 != nullptr ? @1 : @2), @7);
 			if ($1 != nullptr)
 				node->str = *$1;
 			ast_stack.back()->children.push_back(node);

kernel/celltypes.h

@@ -102,11 +102,13 @@ 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>());
 		setup_type(ID($original_tag), {ID::A}, {ID::Y});
 		setup_type(ID($future_ff), {ID::A}, {ID::Y});
+		setup_type(ID($scopeinfo), {}, {});
 	}
 
 	void setup_internals_eval()

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)

kernel/driver.cc

@@ -92,8 +92,15 @@ int getopt(int argc, char **argv, const char *optstring)
 		return optopt;
 	}
 
-	optarg = argv[++optind];
+	if (++optind >= argc) {
+		fprintf(stderr, "%s: option '-%c' expects an argument\n", argv[0], optopt);
+		optopt = '?';
+		return optopt;
+	}
+
+	optarg = argv[optind];
 	optind++, optcur = 1;
+
 	return optopt;
 }
 
@@ -243,14 +250,6 @@ int main(int argc, char **argv)
 	bool mode_v = false;
 	bool mode_q = false;
 
-#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
-	if (getenv("HOME") != NULL) {
-		yosys_history_file = stringf("%s/.yosys_history", getenv("HOME"));
-		read_history(yosys_history_file.c_str());
-		yosys_history_offset = where_history();
-	}
-#endif
-
 	if (argc == 2 && (!strcmp(argv[1], "-h") || !strcmp(argv[1], "-help") || !strcmp(argv[1], "--help")))
 	{
 		printf("\n");
@@ -538,6 +537,36 @@ int main(int argc, char **argv)
 	if (print_banner)
 		yosys_banner();
 
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
+	std::string state_dir;
+	#if defined(_WIN32)
+		if (getenv("HOMEDRIVE") != NULL && getenv("HOMEPATH") != NULL) {
+			state_dir = stringf("%s%s/.local/state", getenv("HOMEDRIVE"), getenv("HOMEPATH"));
+		} else {
+			log_debug("$HOMEDRIVE and/or $HOMEPATH is empty. No history file will be created.\n");
+		}
+	#else
+		if (getenv("XDG_STATE_HOME") == NULL || getenv("XDG_STATE_HOME")[0] == '\0') {
+			if (getenv("HOME") != NULL) {
+				state_dir = stringf("%s/.local/state", getenv("HOME"));
+			} else {
+				log_debug("$HOME is empty. No history file will be created.\n");
+			}
+		} else {
+			state_dir = stringf("%s", getenv("XDG_STATE_HOME"));
+		}
+	#endif
+
+	if (!state_dir.empty()) {
+		std::string yosys_dir = state_dir + "/yosys";
+		create_directory(yosys_dir);
+
+		yosys_history_file = yosys_dir + "/history";
+		read_history(yosys_history_file.c_str());
+		yosys_history_offset = where_history();
+	}
+#endif
+
 	if (print_stats)
 		log_hasher = new SHA1;
 
@@ -569,6 +598,8 @@ int main(int argc, char **argv)
 	for (auto &fn : plugin_filenames)
 		load_plugin(fn, {});
 
+	log_suppressed();
+
 	if (!vlog_defines.empty()) {
 		std::string vdef_cmd = "read -define";
 		for (auto vdef : vlog_defines)

kernel/hashlib.h

@@ -17,6 +17,8 @@
 #include <string>
 #include <vector>
 
+#include <stdint.h>
+
 namespace hashlib {
 
 const int hashtable_size_trigger = 2;

kernel/register.cc

@@ -108,9 +108,8 @@ Pass::Pass(std::string name, std::string short_help) : pass_name(name), short_he
 
 void Pass::run_register()
 {
-	if (pass_register.count(pass_name))
+	if (pass_register.count(pass_name) && !replace_existing_pass())
 		log_error("Unable to register pass '%s', pass already exists!\n", pass_name.c_str());
-
 	pass_register[pass_name] = this;
 }
 
@@ -447,13 +446,12 @@ Frontend::Frontend(std::string name, std::string short_help) :
 
 void Frontend::run_register()
 {
-	if (pass_register.count(pass_name))
+	if (pass_register.count(pass_name) && !replace_existing_pass())
 		log_error("Unable to register pass '%s', pass already exists!\n", pass_name.c_str());
 	pass_register[pass_name] = this;
 
-	if (frontend_register.count(frontend_name))
+	if (frontend_register.count(frontend_name) && !replace_existing_pass())
 		log_error("Unable to register frontend '%s', frontend already exists!\n", frontend_name.c_str());
-
 	frontend_register[frontend_name] = this;
 }
 

kernel/register.h

@@ -70,6 +70,7 @@ struct Pass
 
 	virtual void on_register();
 	virtual void on_shutdown();
+	virtual bool replace_existing_pass() const { return false; }
 };
 
 struct ScriptPass : Pass

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,31 @@ 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($scopeinfo)) {
+				param(ID::TYPE);
+				check_expected();
+				std::string scope_type = cell->getParam(ID::TYPE).decode_string();
+				if (scope_type != "module" && scope_type != "struct")
+					error(__LINE__);
+				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; }
@@ -2157,17 +2188,10 @@ void RTLIL::Module::remove(const pool<RTLIL::Wire*> &wires)
 		}
 
 		void operator()(RTLIL::SigSpec &lhs, RTLIL::SigSpec &rhs) {
-			log_assert(GetSize(lhs) == GetSize(rhs));
-			lhs.unpack();
-			rhs.unpack();
-			for (int i = 0; i < GetSize(lhs); i++) {
-				RTLIL::SigBit &lhs_bit = lhs.bits_[i];
-				RTLIL::SigBit &rhs_bit = rhs.bits_[i];
-				if ((lhs_bit.wire != nullptr && wires_p->count(lhs_bit.wire)) || (rhs_bit.wire != nullptr && wires_p->count(rhs_bit.wire))) {
-					lhs_bit = State::Sx;
-					rhs_bit = State::Sx;
-				}
-			}
+			// If a deleted wire occurs on the lhs or rhs we just remove that part
+			// of the assignment
+			lhs.remove2(*wires_p, &rhs);
+			rhs.remove2(*wires_p, &lhs);
 		}
 	};
 
@@ -3693,6 +3717,9 @@ RTLIL::SigChunk::SigChunk(const RTLIL::SigBit &bit)
 
 RTLIL::SigChunk RTLIL::SigChunk::extract(int offset, int length) const
 {
+	log_assert(offset >= 0);
+	log_assert(length >= 0);
+	log_assert(offset + length <= width);
 	RTLIL::SigChunk ret;
 	if (wire) {
 		ret.wire = wire;
@@ -4238,6 +4265,34 @@ void RTLIL::SigSpec::remove2(const std::set<RTLIL::SigBit> &pattern, RTLIL::SigS
 	check();
 }
 
+void RTLIL::SigSpec::remove2(const pool<RTLIL::Wire*> &pattern, RTLIL::SigSpec *other)
+{
+	if (other)
+		cover("kernel.rtlil.sigspec.remove_other");
+	else
+		cover("kernel.rtlil.sigspec.remove");
+
+	unpack();
+
+	if (other != NULL) {
+		log_assert(width_ == other->width_);
+		other->unpack();
+	}
+
+	for (int i = GetSize(bits_) - 1; i >= 0; i--) {
+		if (bits_[i].wire != NULL && pattern.count(bits_[i].wire)) {
+			bits_.erase(bits_.begin() + i);
+			width_--;
+			if (other != NULL) {
+				other->bits_.erase(other->bits_.begin() + i);
+				other->width_--;
+			}
+		}
+	}
+
+	check();
+}
+
 RTLIL::SigSpec RTLIL::SigSpec::extract(const RTLIL::SigSpec &pattern, const RTLIL::SigSpec *other) const
 {
 	if (other)
@@ -4377,6 +4432,9 @@ void RTLIL::SigSpec::remove(int offset, int length)
 
 RTLIL::SigSpec RTLIL::SigSpec::extract(int offset, int length) const
 {
+	log_assert(offset >= 0);
+	log_assert(length >= 0);
+	log_assert(offset + length <= width_);
 	unpack();
 	cover("kernel.rtlil.sigspec.extract_pos");
 	return std::vector<RTLIL::SigBit>(bits_.begin() + offset, bits_.begin() + offset + length);

kernel/rtlil.h

@@ -924,6 +924,7 @@ public:
 	void remove(const pool<RTLIL::SigBit> &pattern, RTLIL::SigSpec *other) const;
 	void remove2(const pool<RTLIL::SigBit> &pattern, RTLIL::SigSpec *other);
 	void remove2(const std::set<RTLIL::SigBit> &pattern, RTLIL::SigSpec *other);
+	void remove2(const pool<RTLIL::Wire*> &pattern, RTLIL::SigSpec *other);
 
 	void remove(int offset, int length = 1);
 	void remove_const();

kernel/satgen.cc

@@ -1379,6 +1379,11 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
 		return true;
 	}
 
+	if (cell->type == ID($scopeinfo))
+	{
+		return true;
+	}
+
 	// Unsupported internal cell types: $pow $fsm $mem*
 	// .. and all sequential cells with asynchronous inputs
 	return false;

kernel/scopeinfo.cc

@@ -0,0 +1,129 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2024  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/scopeinfo.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+template <typename I, typename Filter> void ModuleHdlnameIndex::index_items(I begin, I end, Filter filter)
+{
+	for (; begin != end; ++begin) {
+		auto const &item = *begin;
+
+		if (!filter(item))
+			continue;
+		std::vector<IdString> path = parse_hdlname(item);
+		if (!path.empty())
+			lookup.emplace(item, tree.insert(path, item));
+	}
+}
+
+void ModuleHdlnameIndex::index()
+{
+	index_wires();
+	index_cells();
+}
+
+void ModuleHdlnameIndex::index_wires()
+{
+	auto wires = module->wires();
+	index_items(wires.begin(), wires.end(), [](Wire *) { return true; });
+}
+
+void ModuleHdlnameIndex::index_cells()
+{
+	auto cells = module->cells();
+	index_items(cells.begin(), cells.end(), [](Cell *) { return true; });
+}
+
+void ModuleHdlnameIndex::index_scopeinfo_cells()
+{
+	auto cells = module->cells();
+	index_items(cells.begin(), cells.end(), [](Cell *cell) { return cell->type == ID($scopeinfo); });
+}
+
+std::vector<std::string> ModuleHdlnameIndex::scope_sources(Cursor cursor)
+{
+	std::vector<std::string> result;
+
+	for (; !cursor.is_root(); cursor = cursor.parent()) {
+		if (!cursor.has_entry()) {
+			result.push_back("");
+			result.push_back("");
+			continue;
+		}
+		Cell *cell = cursor.entry().cell();
+		if (cell == nullptr || cell->type != ID($scopeinfo)) {
+			result.push_back("");
+			result.push_back("");
+			continue;
+		}
+		result.push_back(scopeinfo_get_attribute(cell, ScopeinfoAttrs::Module, ID::src).decode_string());
+		result.push_back(scopeinfo_get_attribute(cell, ScopeinfoAttrs::Cell, ID::src).decode_string());
+	}
+
+	result.push_back(module->get_src_attribute());
+
+	std::reverse(result.begin(), result.end());
+
+	return result;
+}
+
+static const char *attr_prefix(ScopeinfoAttrs attrs)
+{
+	switch (attrs) {
+	case ScopeinfoAttrs::Cell:
+		return "\\cell_";
+	case ScopeinfoAttrs::Module:
+		return "\\module_";
+	default:
+		log_abort();
+	}
+}
+
+bool scopeinfo_has_attribute(const RTLIL::Cell *scopeinfo, ScopeinfoAttrs attrs, const RTLIL::IdString &id)
+{
+	log_assert(scopeinfo->type == ID($scopeinfo));
+	return scopeinfo->has_attribute(attr_prefix(attrs) + RTLIL::unescape_id(id));
+}
+
+RTLIL::Const scopeinfo_get_attribute(const RTLIL::Cell *scopeinfo, ScopeinfoAttrs attrs, const RTLIL::IdString &id)
+{
+	log_assert(scopeinfo->type == ID($scopeinfo));
+	auto found = scopeinfo->attributes.find(attr_prefix(attrs) + RTLIL::unescape_id(id));
+	if (found == scopeinfo->attributes.end())
+		return RTLIL::Const();
+	return found->second;
+}
+
+dict<RTLIL::IdString, RTLIL::Const> scopeinfo_attributes(const RTLIL::Cell *scopeinfo, ScopeinfoAttrs attrs)
+{
+	dict<RTLIL::IdString, RTLIL::Const> attributes;
+
+	const char *prefix = attr_prefix(attrs);
+	int prefix_len = strlen(prefix);
+
+	for (auto const &entry : scopeinfo->attributes)
+		if (entry.first.begins_with(prefix))
+			attributes.emplace(RTLIL::escape_id(entry.first.c_str() + prefix_len), entry.second);
+
+	return attributes;
+}
+
+YOSYS_NAMESPACE_END

kernel/scopeinfo.h

@@ -0,0 +1,432 @@
+/*
+ *  yosys -- Yosys Open SYnthesis Suite
+ *
+ *  Copyright (C) 2024  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.
+ *
+ */
+
+#ifndef SCOPEINFO_H
+#define SCOPEINFO_H
+
+#include <vector>
+#include <algorithm>
+
+#include "kernel/yosys.h"
+#include "kernel/celltypes.h"
+
+YOSYS_NAMESPACE_BEGIN
+
+template<typename T>
+class IdTree
+{
+public:
+	struct Cursor;
+
+protected:
+	IdTree *parent = nullptr;
+	IdString scope_name;
+	int depth = 0;
+
+	pool<IdString> names;
+	dict<IdString, T> entries;
+public: // XXX
+	dict<IdString, std::unique_ptr<IdTree>> subtrees;
+
+	template<typename P, typename T_ref>
+	static Cursor do_insert(IdTree *tree, P begin, P end, T_ref &&value)
+	{
+		log_assert(begin != end && "path must be non-empty");
+		while (true) {
+			IdString name = *begin;
+			++begin;
+			log_assert(!name.empty());
+			tree->names.insert(name);
+			if (begin == end) {
+				tree->entries.emplace(name, std::forward<T_ref>(value));
+				return Cursor(tree, name);
+			}
+			auto &unique = tree->subtrees[name];
+			if (!unique) {
+				unique.reset(new IdTree);
+				unique->scope_name = name;
+				unique->parent = tree;
+				unique->depth = tree->depth + 1;
+			}
+			tree = unique.get();
+		}
+	}
+
+public:
+	IdTree() = default;
+	IdTree(const IdTree &) = delete;
+	IdTree(IdTree &&) = delete;
+
+	// A cursor remains valid as long as the (sub-)IdTree it points at is alive
+	struct Cursor
+	{
+		friend class IdTree;
+	protected:
+	public:
+		IdTree *target;
+		IdString scope_name;
+
+		Cursor() : target(nullptr) {}
+		Cursor(IdTree *target, IdString scope_name) : target(target), scope_name(scope_name) {
+			if (scope_name.empty())
+				log_assert(target->parent == nullptr);
+		}
+
+		Cursor do_first_child() {
+			IdTree *tree = nullptr;
+			if (scope_name.empty()) {
+				tree = target;
+			} else {
+				auto found = target->subtrees.find(scope_name);
+				if (found != target->subtrees.end()) {
+					tree = found->second.get();
+				} else {
+					return Cursor();
+				}
+			}
+			if (tree->names.empty()) {
+				return Cursor();
+			}
+			return Cursor(tree, *tree->names.begin());
+		}
+
+		Cursor do_next_sibling() {
+			if (scope_name.empty())
+				return Cursor();
+			auto found = target->names.find(scope_name);
+			if (found == target->names.end())
+				return Cursor();
+			++found;
+			if (found == target->names.end())
+				return Cursor();
+			return Cursor(target, *found);
+		}
+
+		Cursor do_parent() {
+			if (scope_name.empty())
+				return Cursor();
+			if (target->parent != nullptr)
+				return Cursor(target->parent, target->scope_name);
+			return Cursor(target, IdString());
+		}
+
+		Cursor do_next_preorder() {
+			Cursor current = *this;
+			Cursor next = current.do_first_child();
+			if (next.valid())
+				return next;
+			while (current.valid()) {
+				if (next.valid())
+					return next;
+				next = current.do_next_sibling();
+				if (next.valid())
+					return next;
+				current = current.do_parent();
+			}
+			return current;
+		}
+
+		Cursor do_child(IdString name) {
+			IdTree *tree = nullptr;
+			if (scope_name.empty()) {
+				tree = target;
+			} else {
+				auto found = target->subtrees.find(scope_name);
+				if (found != target->subtrees.end()) {
+					tree = found->second.get();
+				} else {
+					return Cursor();
+				}
+			}
+			auto found = tree->names.find(name);
+			if (found == tree->names.end()) {
+				return Cursor();
+			}
+			return Cursor(tree, *found);
+		}
+
+	public:
+		bool operator==(const Cursor &other) const {
+			return target == other.target && scope_name == other.scope_name;
+		}
+		bool operator!=(const Cursor &other) const {
+			return !(*this == other);
+		}
+
+		bool valid() const {
+			return target != nullptr;
+		}
+
+		int depth() const {
+			log_assert(valid());
+			return target->depth + !scope_name.empty();
+		}
+
+		bool is_root() const {
+			return target != nullptr && scope_name.empty();
+		}
+
+		bool has_entry() const {
+			log_assert(valid());
+			return !scope_name.empty() && target->entries.count(scope_name);
+		}
+
+		T &entry() {
+			log_assert(!scope_name.empty());
+			return target->entries.at(scope_name);
+		}
+
+		void assign_path_to(std::vector<IdString> &out_path) {
+			log_assert(valid());
+			out_path.clear();
+			if (scope_name.empty())
+				return;
+			out_path.push_back(scope_name);
+			IdTree *current = target;
+			while (current->parent) {
+				out_path.push_back(current->scope_name);
+				current = current->parent;
+			}
+			std::reverse(out_path.begin(), out_path.end());
+		}
+
+		std::vector<IdString> path() {
+			std::vector<IdString> result;
+			assign_path_to(result);
+			return result;
+		}
+
+		std::string path_str() {
+			std::string result;
+			for (const auto &item : path()) {
+				if (!result.empty())
+					result.push_back(' ');
+				result += RTLIL::unescape_id(item);
+			}
+			return result;
+		}
+
+		Cursor first_child() {
+			log_assert(valid());
+			return do_first_child();
+		}
+
+		Cursor next_preorder() {
+			log_assert(valid());
+			return do_next_preorder();
+		}
+
+		Cursor parent() {
+			log_assert(valid());
+			return do_parent();
+		}
+
+		Cursor child(IdString name) {
+			log_assert(valid());
+			return do_child(name);
+		}
+
+		Cursor common_ancestor(Cursor other) {
+			Cursor current = *this;
+
+			while (current != other) {
+				if (!current.valid() || !other.valid())
+					return Cursor();
+				int delta = current.depth() - other.depth();
+				if (delta >= 0)
+					current = current.do_parent();
+				if (delta <= 0)
+					other = other.do_parent();
+			}
+			return current;
+		}
+	};
+
+	template<typename P>
+	Cursor insert(P begin, P end, const T &value) {
+		return do_insert(this, begin, end, value);
+	}
+
+	template<typename P>
+	Cursor insert(P begin, P end, T &&value) {
+		return do_insert(this, begin, end, std::move(value));
+	}
+
+	template<typename P>
+	Cursor insert(const P &path, const T &value) {
+		return do_insert(this, path.begin(), path.end(), value);
+	}
+
+	template<typename P>
+	Cursor insert(const P &path, T &&value) {
+		return do_insert(this, path.begin(), path.end(), std::move(value));
+	}
+
+	Cursor cursor() {
+		return parent ? Cursor(this->parent, this->scope_name) : Cursor(this, IdString());
+	}
+
+	template<typename P>
+	Cursor cursor(P begin, P end) {
+		Cursor current = cursor();
+		for (; begin != end; ++begin) {
+			current = current.do_child(*begin);
+			if (!current.valid())
+				break;
+		}
+		return current;
+	}
+
+	template<typename P>
+	Cursor cursor(const P &path) {
+		return cursor(path.begin(), path.end());
+	}
+};
+
+
+struct ModuleItem {
+	enum class Type {
+		Wire,
+		Cell,
+	};
+	Type type;
+	void *ptr;
+
+	ModuleItem(Wire *wire) : type(Type::Wire), ptr(wire) {}
+	ModuleItem(Cell *cell) : type(Type::Cell), ptr(cell) {}
+
+	bool is_wire() const { return type == Type::Wire; }
+	bool is_cell() const { return type == Type::Cell; }
+
+	Wire *wire() const { return type == Type::Wire ? static_cast<Wire *>(ptr) : nullptr; }
+	Cell *cell() const { return type == Type::Cell ? static_cast<Cell *>(ptr) : nullptr; }
+
+	bool operator==(const ModuleItem &other) const { return ptr == other.ptr && type == other.type; }
+	unsigned int hash() const { return (uintptr_t)ptr; }
+};
+
+static inline void log_dump_val_worker(typename IdTree<ModuleItem>::Cursor cursor ) { log("%p %s", cursor.target, log_id(cursor.scope_name)); }
+
+template<typename T>
+static inline void log_dump_val_worker(const typename std::unique_ptr<T> &cursor ) { log("unique %p", cursor.get()); }
+
+template<typename O>
+std::vector<IdString> parse_hdlname(const O* object)
+{
+	std::vector<IdString> path;
+	if (!object->name.isPublic())
+		return path;
+	for (auto const &item : object->get_hdlname_attribute())
+		path.push_back("\\" + item);
+	if (path.empty())
+		path.push_back(object->name);
+	return path;
+}
+
+template<typename O>
+std::pair<std::vector<IdString>, IdString> parse_scopename(const O* object)
+{
+	std::vector<IdString> path;
+	IdString trailing = object->name;
+	if (object->name.isPublic()) {
+		for (auto const &item : object->get_hdlname_attribute())
+			path.push_back("\\" + item);
+		if (!path.empty()) {
+			trailing = path.back();
+			path.pop_back();
+		}
+	} else {
+		for (auto const &item : split_tokens(object->get_string_attribute(ID(scopename)), " "))
+			path.push_back("\\" + item);
+
+	}
+	return {path, trailing};
+}
+
+struct ModuleHdlnameIndex {
+	typedef IdTree<ModuleItem>::Cursor Cursor;
+
+	RTLIL::Module *module;
+	IdTree<ModuleItem> tree;
+	dict<ModuleItem, Cursor> lookup;
+
+	ModuleHdlnameIndex(RTLIL::Module *module) : module(module) {}
+
+private:
+	template<typename I, typename Filter>
+	void index_items(I begin, I end, Filter filter);
+
+public:
+	// Index all wires and cells of the module
+	void index();
+
+	// Index all wires of the module
+	void index_wires();
+
+	// Index all cells of the module
+	void index_cells();
+
+	// Index only the $scopeinfo cells of the module.
+	// This is sufficient when using `containing_scope`.
+	void index_scopeinfo_cells();
+
+
+	// Return the cursor for the containing scope of some RTLIL object (Wire/Cell/...)
+	template<typename O>
+	std::pair<Cursor, IdString> containing_scope(O *object) {
+		auto pair = parse_scopename(object);
+		return {tree.cursor(pair.first), pair.second};
+	}
+
+	// Return a vector of source locations starting from the indexed module to
+	// the scope represented by the cursor. The vector alternates module and
+	// module item source locations, using empty strings for missing src
+	// attributes.
+	std::vector<std::string> scope_sources(Cursor cursor);
+
+	// Return a vector of source locations starting from the indexed module to
+	// the passed RTLIL object (Wire/Cell/...). The vector alternates module
+	// and module item source locations, using empty strings for missing src
+	// attributes.
+	template<typename O>
+	std::vector<std::string> sources(O *object) {
+		auto pair = parse_scopename(object);
+		std::vector<std::string> result = scope_sources(tree.cursor(pair.first));
+		result.push_back(object->get_src_attribute());
+		return result;
+	}
+};
+
+enum class ScopeinfoAttrs {
+	Module,
+	Cell,
+};
+
+// Check whether the flattened module or flattened cell corresponding to a $scopeinfo cell had a specific attribute.
+bool scopeinfo_has_attribute(const RTLIL::Cell *scopeinfo, ScopeinfoAttrs attrs, const RTLIL::IdString &id);
+
+// Get a specific attribute from the flattened module or flattened cell corresponding to a $scopeinfo cell.
+RTLIL::Const scopeinfo_get_attribute(const RTLIL::Cell *scopeinfo, ScopeinfoAttrs attrs, const RTLIL::IdString &id);
+
+// Get all attribute from the flattened module or flattened cell corresponding to a $scopeinfo cell.
+dict<RTLIL::IdString, RTLIL::Const> scopeinfo_attributes(const RTLIL::Cell *scopeinfo, ScopeinfoAttrs attrs);
+
+YOSYS_NAMESPACE_END
+
+#endif

kernel/yosys.cc

@@ -436,6 +436,25 @@ std::string make_temp_dir(std::string template_str)
 #endif
 }
 
+bool check_directory_exists(const std::string& dirname)
+{
+#if defined(_WIN32)
+	struct _stat info;
+	if (_stat(dirname.c_str(), &info) != 0)
+	{
+		return false;
+	}
+	return (info.st_mode & _S_IFDIR) != 0;
+#else
+	struct stat info;
+	if (stat(dirname.c_str(), &info) != 0)
+	{
+		return false;
+	}
+	return (info.st_mode & S_IFDIR) != 0;
+#endif
+}
+
 #ifdef _WIN32
 bool check_file_exists(std::string filename, bool)
 {
@@ -481,6 +500,48 @@ void remove_directory(std::string dirname)
 #endif
 }
 
+bool create_directory(const std::string& dirname)
+{
+#if defined(_WIN32)
+	int ret = _mkdir(dirname.c_str());
+#else
+	mode_t mode = 0755;
+	int ret = mkdir(dirname.c_str(), mode);
+#endif
+	if (ret == 0)
+		return true;
+
+	switch (errno)
+	{
+	case ENOENT:
+		// parent didn't exist, try to create it
+		{
+			std::string::size_type pos = dirname.find_last_of('/');
+			if (pos == std::string::npos)
+#if defined(_WIN32)
+				pos = dirname.find_last_of('\\');
+			if (pos == std::string::npos)
+#endif
+				return false;
+			if (!create_directory( dirname.substr(0, pos) ))
+				return false;
+		}
+		// now, try to create again
+#if defined(_WIN32)
+		return 0 == _mkdir(dirname.c_str());
+#else
+		return 0 == mkdir(dirname.c_str(), mode);
+#endif
+
+	case EEXIST:
+		// done!
+		return check_directory_exists(dirname);
+
+	default:
+		return false;
+	}
+}
+
 std::string escape_filename_spaces(const std::string& filename)
 {
 	std::string out;
@@ -781,10 +842,10 @@ static int tcl_yosys_cmd(ClientData, Tcl_Interp *interp, int argc, const char *a
 
 int yosys_tcl_iterp_init(Tcl_Interp *interp)
 {
-    if (Tcl_Init(interp)!=TCL_OK)
+	if (Tcl_Init(interp)!=TCL_OK)
 		log_warning("Tcl_Init() call failed - %s\n",Tcl_ErrnoMsg(Tcl_GetErrno()));
 	Tcl_CreateCommand(interp, "yosys", tcl_yosys_cmd, NULL, NULL);
-    return TCL_OK ;
+	return TCL_OK ;
 }
 
 void yosys_tcl_activate_repl()

kernel/yosys.h

@@ -66,6 +66,8 @@
 #include <stdint.h>
 #include <stdio.h>
 #include <limits.h>
+#include <sys/stat.h>
+#include <errno.h>
 
 #ifdef WITH_PYTHON
 #include <Python.h>
@@ -341,8 +343,10 @@ std::string get_base_tmpdir();
 std::string make_temp_file(std::string template_str = get_base_tmpdir() + "/yosys_XXXXXX");
 std::string make_temp_dir(std::string template_str = get_base_tmpdir() + "/yosys_XXXXXX");
 bool check_file_exists(std::string filename, bool is_exec = false);
+bool check_directory_exists(const std::string& dirname);
 bool is_absolute_path(std::string filename);
 void remove_directory(std::string dirname);
+bool create_directory(const std::string& dirname);
 std::string escape_filename_spaces(const std::string& filename);
 
 template<typename T> int GetSize(const T &obj) { return obj.size(); }

misc/py_wrap_generator.py

@@ -1257,6 +1257,7 @@ class WFunction:
 		func.is_static = False
 		func.is_inline = False
 		func.is_virtual = False
+		func.is_const = False
 		func.ret_attr_type = attr_types.default
 		func.is_operator = False
 		func.member_of = None
@@ -1334,6 +1335,11 @@ class WFunction:
 		found = find_closing(str_def, "(", ")")
 		if found == -1:
 			return None
+
+		post_qualifiers = str_def[found + 1:].lstrip().replace("{", " {") + " "
+		if post_qualifiers.startswith("const "):
+			func.is_const = True
+
 		str_def = str_def[0:found]
 		if func.name in blacklist_methods:
 			return None
@@ -1379,6 +1385,12 @@ class WFunction:
 	def gen_alias(self):
 		self.alias = self.mangled_name
 
+	def gen_post_qualifiers(self, derived=False):
+		if self.member_of != None and self.member_of.link_type == link_types.derive and self.is_virtual and derived:
+			# we drop the qualifiers when deriving callbacks to be implemented in Python
+			return ''
+		return ' const' if self.is_const else ''
+
 	def gen_decl(self):
 		if self.duplicate:
 			return ""
@@ -1392,7 +1404,7 @@ class WFunction:
 			text += ", "
 		if len(self.args) > 0:
 			text = text[:-2]
-		text += ");\n"
+		text += f"){self.gen_post_qualifiers()};\n"
 		return text
 
 	def gen_decl_virtual(self):
@@ -1411,12 +1423,18 @@ class WFunction:
 		if len(self.args) > 0:
 			text = text[:-2]
 		text += ")"
-		if len(self.args) == 0:
+		if len(self.args) == 0 and self.ret_type.name == "void":
 			text += "{}"
 		else:
 			text += "\n\t\t{"
 			for arg in self.args:
 				text += "\n\t\t\t(void)" + arg.gen_varname() + ";"
+			if self.ret_type.name == "void":
+				pass
+			elif self.ret_type.name == "bool":
+				text += "\n\t\t\treturn false;"
+			else:
+				raise NotImplementedError(self.ret_type.name)
 			text += "\n\t\t}\n"
 		text += "\n\t\tvirtual "
 		if self.is_static:
@@ -1427,7 +1445,7 @@ class WFunction:
 			text += ", "
 		if len(self.args) > 0:
 			text = text[:-2]
-		text += ") override;\n"
+		text += f"){self.gen_post_qualifiers()} override;\n"
 		return text
 
 	def gen_decl_hash_py(self):
@@ -1452,7 +1470,7 @@ class WFunction:
 			text += ", "
 		if len(self.args) > 0:
 			text = text[:-2]
-		text +=")\n\t{"
+		text += f"){self.gen_post_qualifiers()}\n\t{{"
 		for arg in self.args:
 			text += arg.gen_translation()
 		text += "\n\t\t"
@@ -1507,16 +1525,17 @@ class WFunction:
 			text += ", "
 		if len(self.args) > 0:
 			text = text[:-2]
-		text += ")\n\t{"
+		text += f"){self.gen_post_qualifiers()}\n\t{{"
 		for arg in self.args:
 			text += arg.gen_translation_cpp()
-		text += "\n\t\t"
+		return_stmt = "return " if self.ret_type.name != "void" else ""
+		text += f"\n\t\t{return_stmt}"
 		if self.member_of == None:
 			text += "::" + self.namespace + "::" + self.alias + "("
 		elif self.is_static:
 			text += self.member_of.namespace + "::" + self.member_of.name + "::" + self.name + "("
 		else:
-			text += "py_" + self.alias + "("
+			text += f"const_cast<{self.member_of.name}*>(this)->py_" + self.alias + "("
 		for arg in self.args:
 			text += arg.gen_call_cpp() + ", "
 		if len(self.args) > 0:
@@ -1547,11 +1566,13 @@ class WFunction:
 			call_string = call_string[0:-2]
 		call_string += ");"
 
+		return_stmt = "return " if self.ret_type.name != "void" else ""
+
 		text += ")\n\t\t{"
-		text += "\n\t\t\tif(boost::python::override py_" + self.alias + " = this->get_override(\"py_" + self.alias + "\"))"
-		text += "\n\t\t\t\t" + call_string
+		text += "\n\t\t\tif (boost::python::override py_" + self.alias + " = this->get_override(\"py_" + self.alias + "\"))"
+		text += f"\n\t\t\t\t{return_stmt}" + call_string
 		text += "\n\t\t\telse"
-		text += "\n\t\t\t\t" + self.member_of.name + "::" + call_string
+		text += f"\n\t\t\t\t{return_stmt}" + self.member_of.name + "::" + call_string
 		text += "\n\t\t}"
 
 		text += "\n\n\t\t" + self.ret_type.gen_text() + " default_py_" + self.alias + "("
@@ -1559,8 +1580,8 @@ class WFunction:
 			text += arg.gen_listitem() + ", "
 		if len(self.args) > 0:
 			text = text[:-2]
-		text += ")\n\t\t{"
-		text += "\n\t\t\tthis->" + self.member_of.name + "::" + call_string
+		text += f")\n\t\t{{"
+		text += f"\n\t\t\t{return_stmt}this->" + self.member_of.name + "::" + call_string
 		text += "\n\t\t}"
 		return text
 
@@ -1584,9 +1605,9 @@ class WFunction:
 			for a in self.args:
 				text += a.gen_listitem_hash() + ", "
 			if len(self.args) > 0:
-				text = text[0:-2] + ")>"
+				text = text[0:-2] + f"){self.gen_post_qualifiers(True)}>"
 			else:
-				text += "void)>"
+				text += f"void){self.gen_post_qualifiers(True)}>"
 
 		if self.is_operator:
 			text += "(\"" + wrappable_operators[self.name.replace("operator","")] + "\""

passes/cmds/chformal.cc

@@ -23,6 +23,52 @@
 USING_YOSYS_NAMESPACE
 PRIVATE_NAMESPACE_BEGIN
 
+static RTLIL::IdString formal_flavor(RTLIL::Cell *cell)
+{
+	if (cell->type != ID($check))
+		return cell->type;
+
+	std::string flavor_param = cell->getParam(ID(FLAVOR)).decode_string();
+	if (flavor_param == "assert")
+		return ID($assert);
+	else if (flavor_param == "assume")
+		return ID($assume);
+	else if (flavor_param == "cover")
+		return ID($cover);
+	else if (flavor_param == "live")
+		return ID($live);
+	else if (flavor_param == "fair")
+		return ID($fair);
+	else
+		log_abort();
+}
+
+static void set_formal_flavor(RTLIL::Cell *cell, RTLIL::IdString flavor)
+{
+	if (cell->type != ID($check)) {
+		cell->type = flavor;
+		return;
+	}
+
+	if (flavor == ID($assert))
+		cell->setParam(ID(FLAVOR), std::string("assert"));
+	else if (flavor == ID($assume))
+		cell->setParam(ID(FLAVOR), std::string("assume"));
+	else if (flavor == ID($cover))
+		cell->setParam(ID(FLAVOR), std::string("cover"));
+	else if (flavor == ID($live))
+		cell->setParam(ID(FLAVOR), std::string("live"));
+	else if (flavor == ID($fair))
+		cell->setParam(ID(FLAVOR), std::string("fair"));
+	else
+		log_abort();
+}
+
+static bool is_triggered_check_cell(RTLIL::Cell * cell)
+{
+	return cell->type == ID($check) && cell->getParam(ID(TRG_ENABLE)).as_bool();
+}
+
 struct ChformalPass : public Pass {
 	ChformalPass() : Pass("chformal", "change formal constraints of the design") { }
 	void help() override
@@ -41,13 +87,18 @@ struct ChformalPass : public Pass {
 		log("    -fair         $fair cells, representing assume(s_eventually ...)\n");
 		log("    -cover        $cover cells, representing cover() statements\n");
 		log("\n");
+		log("    Additionally chformal will operate on $check cells corresponding to the\n");
+		log("    selected constraint types.\n");
+		log("\n");
 		log("Exactly one of the following modes must be specified:\n");
 		log("\n");
 		log("    -remove\n");
 		log("        remove the cells and thus constraints from the design\n");
 		log("\n");
 		log("    -early\n");
-		log("        bypass FFs that only delay the activation of a constraint\n");
+		log("        bypass FFs that only delay the activation of a constraint. When inputs\n");
+		log("        of the bypassed FFs do not remain stable between clock edges, this may\n");
+		log("        result in unexpected behavior.\n");
 		log("\n");
 		log("    -delay <N>\n");
 		log("        delay activation of the constraint by <N> clock cycles\n");
@@ -69,6 +120,11 @@ struct ChformalPass : public Pass {
 		log("    -fair2live\n");
 		log("        change the roles of cells as indicated. these options can be combined\n");
 		log("\n");
+		log("    -lower\n");
+		log("        convert each $check cell into an $assert, $assume, $live, $fair or\n");
+		log("        $cover cell. If the $check cell contains a message, also produce a\n");
+		log("        $print cell.\n");
+		log("\n");
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
@@ -146,6 +202,10 @@ struct ChformalPass : public Pass {
 				mode = 'c';
 				continue;
 			}
+			if (mode == 0 && args[argidx] == "-lower") {
+				mode = 'l';
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
@@ -166,7 +226,7 @@ struct ChformalPass : public Pass {
 			vector<Cell*> constr_cells;
 
 			for (auto cell : module->selected_cells())
-				if (constr_types.count(cell->type))
+				if (constr_types.count(formal_flavor(cell)))
 					constr_cells.push_back(cell);
 
 			if (mode == 'r')
@@ -216,6 +276,18 @@ struct ChformalPass : public Pass {
 				}
 
 				for (auto cell : constr_cells)
+				{
+					if (is_triggered_check_cell(cell)) {
+						if (cell->getParam(ID::TRG_WIDTH).as_int() != 1)
+							continue;
+						cell->setPort(ID::TRG, SigSpec());
+						cell->setParam(ID::TRG_ENABLE, false);
+						cell->setParam(ID::TRG_WIDTH, 0);
+						cell->setParam(ID::TRG_POLARITY, false);
+					}
+
+					IdString flavor = formal_flavor(cell);
+
 					while (true)
 					{
 						SigSpec A = sigmap(cell->getPort(ID::A));
@@ -225,8 +297,8 @@ struct ChformalPass : public Pass {
 							break;
 
 						if (!init_zero.count(EN)) {
-							if (cell->type == ID($cover)) break;
-							if (cell->type.in(ID($assert), ID($assume)) && !init_one.count(A)) break;
+							if (flavor == ID($cover)) break;
+							if (flavor.in(ID($assert), ID($assume)) && !init_one.count(A)) break;
 						}
 
 						const auto &A_map = ffmap.at(A);
@@ -238,25 +310,31 @@ struct ChformalPass : public Pass {
 						cell->setPort(ID::A, A_map.first);
 						cell->setPort(ID::EN, EN_map.first);
 					}
+				}
 			}
 			else
 			if (mode == 'd')
 			{
 				for (auto cell : constr_cells)
-				for (int i = 0; i < mode_arg; i++)
 				{
-					SigSpec orig_a = cell->getPort(ID::A);
-					SigSpec orig_en = cell->getPort(ID::EN);
+					if (is_triggered_check_cell(cell))
+						log_error("Cannot delay edge triggered $check cell %s, run async2sync or clk2fflogic first.\n", log_id(cell));
 
-					Wire *new_a = module->addWire(NEW_ID);
-					Wire *new_en = module->addWire(NEW_ID);
-					new_en->attributes[ID::init] = State::S0;
+					for (int i = 0; i < mode_arg; i++)
+					{
+						SigSpec orig_a = cell->getPort(ID::A);
+						SigSpec orig_en = cell->getPort(ID::EN);
 
-					module->addFf(NEW_ID, orig_a, new_a);
-					module->addFf(NEW_ID, orig_en, new_en);
+						Wire *new_a = module->addWire(NEW_ID);
+						Wire *new_en = module->addWire(NEW_ID);
+						new_en->attributes[ID::init] = State::S0;
 
-					cell->setPort(ID::A, new_a);
-					cell->setPort(ID::EN, new_en);
+						module->addFf(NEW_ID, orig_a, new_a);
+						module->addFf(NEW_ID, orig_en, new_en);
+
+						cell->setPort(ID::A, new_a);
+						cell->setPort(ID::EN, new_en);
+					}
 				}
 			}
 			else
@@ -278,21 +356,76 @@ struct ChformalPass : public Pass {
 			if (mode =='p')
 			{
 				for (auto cell : constr_cells)
-					module->addCover(NEW_ID_SUFFIX("coverenable"),
-						cell->getPort(ID::EN), State::S1, cell->get_src_attribute());
+				{
+					if (cell->type == ID($check)) {
+						Cell *cover = module->addCell(NEW_ID_SUFFIX("coverenable"), ID($check));
+						cover->attributes = cell->attributes;
+						cover->parameters = cell->parameters;
+						cover->setParam(ID(FLAVOR), Const("cover"));
+
+						for (auto const &conn : cell->connections())
+							if (!conn.first.in(ID::A, ID::EN))
+								cover->setPort(conn.first, conn.second);
+						cover->setPort(ID::A, cell->getPort(ID::EN));
+						cover->setPort(ID::EN, State::S1);
+					} else {
+						module->addCover(NEW_ID_SUFFIX("coverenable"),
+							cell->getPort(ID::EN), State::S1, cell->get_src_attribute());
+					}
+				}
 			}
 			else
 			if (mode == 'c')
 			{
-				for (auto cell : constr_cells)
-					if (assert2assume && cell->type == ID($assert))
-						cell->type = ID($assume);
-					else if (assume2assert && cell->type == ID($assume))
-						cell->type = ID($assert);
-					else if (live2fair && cell->type == ID($live))
-						cell->type = ID($fair);
-					else if (fair2live && cell->type == ID($fair))
-						cell->type = ID($live);
+				for (auto cell : constr_cells) {
+					IdString flavor = formal_flavor(cell);
+					if (assert2assume && flavor == ID($assert))
+						set_formal_flavor(cell, ID($assume));
+					else if (assume2assert && flavor == ID($assume))
+						set_formal_flavor(cell, ID($assert));
+					else if (live2fair && flavor == ID($live))
+						set_formal_flavor(cell, ID($fair));
+					else if (fair2live && flavor == ID($fair))
+						set_formal_flavor(cell, ID($live));
+				}
+			}
+			else
+			if (mode == 'l')
+			{
+				for (auto cell : constr_cells) {
+					if (cell->type != ID($check))
+						continue;
+
+					if (is_triggered_check_cell(cell))
+						log_error("Cannot lower edge triggered $check cell %s, run async2sync or clk2fflogic first.\n", log_id(cell));
+
+
+					Cell *plain_cell = module->addCell(NEW_ID, formal_flavor(cell));
+
+					plain_cell->attributes = cell->attributes;
+
+					SigBit sig_a = cell->getPort(ID::A);
+					SigBit sig_en = cell->getPort(ID::EN);
+
+					plain_cell->setPort(ID::A, sig_a);
+					plain_cell->setPort(ID::EN, sig_en);
+
+					if (plain_cell->type.in(ID($assert), ID($assume)))
+						sig_a = module->Not(NEW_ID, sig_a);
+
+					SigBit combined_en = module->And(NEW_ID, sig_a, sig_en);
+
+					module->swap_names(cell, plain_cell);
+
+					if (cell->getPort(ID::ARGS).empty()) {
+						module->remove(cell);
+					} else {
+						cell->type = ID($print);
+						cell->setPort(ID::EN, combined_en);
+						cell->unsetPort(ID::A);
+						cell->unsetParam(ID(FLAVOR));
+					}
+				}
 			}
 		}
 	}

passes/cmds/plugin.cc

@@ -103,7 +103,6 @@ void load_plugin(std::string filename, std::vector<std::string> aliases)
 
 			loaded_plugins[orig_filename] = hdl;
 			Pass::init_register();
-
 		}
 	}
 

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];
@@ -1006,6 +1006,18 @@ struct HierarchyPass : public Pass {
 				if (mod->get_bool_attribute(ID::top))
 					top_mod = mod;
 
+		if (top_mod == nullptr)
+		{
+			std::vector<IdString> abstract_ids;
+			for (auto module : design->modules())
+				if (module->name.begins_with("$abstract"))
+					abstract_ids.push_back(module->name);
+			for (auto abstract_id : abstract_ids)
+				design->module(abstract_id)->derive(design, {});
+			for (auto abstract_id : abstract_ids)
+				design->remove(design->module(abstract_id));
+		}
+
 		if (top_mod == nullptr && auto_top_mode) {
 			log_header(design, "Finding top of design hierarchy..\n");
 			dict<Module*, int> db;

passes/opt/opt_clean.cc

@@ -35,10 +35,12 @@ struct keep_cache_t
 {
 	Design *design;
 	dict<Module*, bool> cache;
+	bool purge_mode = false;
 
-	void reset(Design *design = nullptr)
+	void reset(Design *design = nullptr, bool purge_mode = false)
 	{
 		this->design = design;
+		this->purge_mode = purge_mode;
 		cache.clear();
 	}
 
@@ -82,12 +84,15 @@ 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())
 			return true;
 
+		if (!purge_mode && cell->type == ID($scopeinfo))
+			return true;
+
 		if (cell->module && cell->module->design)
 			return query(cell->module->design->module(cell->type));
 
@@ -236,10 +241,13 @@ int count_nontrivial_wire_attrs(RTLIL::Wire *w)
 {
 	int count = w->attributes.size();
 	count -= w->attributes.count(ID::src);
+	count -= w->attributes.count(ID::hdlname);
+	count -= w->attributes.count(ID(scopename));
 	count -= w->attributes.count(ID::unused_bits);
 	return count;
 }
 
+// Should we pick `s2` over `s1` to represent a signal?
 bool compare_signals(RTLIL::SigBit &s1, RTLIL::SigBit &s2, SigPool &regs, SigPool &conns, pool<RTLIL::Wire*> &direct_wires)
 {
 	RTLIL::Wire *w1 = s1.wire;
@@ -292,9 +300,10 @@ bool check_public_name(RTLIL::IdString id)
 
 bool rmunused_module_signals(RTLIL::Module *module, bool purge_mode, bool verbose)
 {
+	// `register_signals` and `connected_signals` will help us decide later on
+	// on picking representatives out of groups of connected signals
 	SigPool register_signals;
 	SigPool connected_signals;
-
 	if (!purge_mode)
 		for (auto &it : module->cells_) {
 			RTLIL::Cell *cell = it.second;
@@ -309,20 +318,27 @@ bool rmunused_module_signals(RTLIL::Module *module, bool purge_mode, bool verbos
 		}
 
 	SigMap assign_map(module);
-	pool<RTLIL::SigSpec> direct_sigs;
+
+	// construct a pool of wires which are directly driven by a known celltype,
+	// this will influence our choice of representatives
 	pool<RTLIL::Wire*> direct_wires;
-	for (auto &it : module->cells_) {
-		RTLIL::Cell *cell = it.second;
-		if (ct_all.cell_known(cell->type))
-			for (auto &it2 : cell->connections())
-				if (ct_all.cell_output(cell->type, it2.first))
-					direct_sigs.insert(assign_map(it2.second));
-	}
-	for (auto &it : module->wires_) {
-		if (direct_sigs.count(assign_map(it.second)) || it.second->port_input)
-			direct_wires.insert(it.second);
+	{
+		pool<RTLIL::SigSpec> direct_sigs;
+		for (auto &it : module->cells_) {
+			RTLIL::Cell *cell = it.second;
+			if (ct_all.cell_known(cell->type))
+				for (auto &it2 : cell->connections())
+					if (ct_all.cell_output(cell->type, it2.first))
+						direct_sigs.insert(assign_map(it2.second));
+		}
+		for (auto &it : module->wires_) {
+			if (direct_sigs.count(assign_map(it.second)) || it.second->port_input)
+				direct_wires.insert(it.second);
+		}
 	}
 
+	// weight all options for representatives with `compare_signals`,
+	// the one that wins will be what `assign_map` maps to
 	for (auto &it : module->wires_) {
 		RTLIL::Wire *wire = it.second;
 		for (int i = 0; i < wire->width; i++) {
@@ -332,21 +348,30 @@ bool rmunused_module_signals(RTLIL::Module *module, bool purge_mode, bool verbos
 		}
 	}
 
+	// we are removing all connections
 	module->connections_.clear();
 
+	// used signals sigmapped
 	SigPool used_signals;
+	// used signals pre-sigmapped
 	SigPool raw_used_signals;
+	// used signals sigmapped, ignoring drivers (we keep track of this to set `unused_bits`)
 	SigPool used_signals_nodrivers;
+
+	// gather the usage information for cells
 	for (auto &it : module->cells_) {
 		RTLIL::Cell *cell = it.second;
 		for (auto &it2 : cell->connections_) {
-			assign_map.apply(it2.second);
+			assign_map.apply(it2.second); // modify the cell connection in place
 			raw_used_signals.add(it2.second);
 			used_signals.add(it2.second);
 			if (!ct_all.cell_output(cell->type, it2.first))
 				used_signals_nodrivers.add(it2.second);
 		}
 	}
+
+	// gather the usage information for ports, wires with `keep`,
+	// also gather init bits
 	dict<RTLIL::SigBit, RTLIL::State> init_bits;
 	for (auto &it : module->wires_) {
 		RTLIL::Wire *wire = it.second;
@@ -374,6 +399,7 @@ bool rmunused_module_signals(RTLIL::Module *module, bool purge_mode, bool verbos
 		}
 	}
 
+	// set init attributes on all wires of a connected group
 	for (auto wire : module->wires()) {
 		bool found = false;
 		Const val(State::Sx, wire->width);
@@ -388,6 +414,7 @@ bool rmunused_module_signals(RTLIL::Module *module, bool purge_mode, bool verbos
 			wire->attributes[ID::init] = val;
 	}
 
+	// now decide for each wire if we should be deleting it
 	pool<RTLIL::Wire*> del_wires_queue;
 	for (auto wire : module->wires())
 	{
@@ -418,6 +445,9 @@ bool rmunused_module_signals(RTLIL::Module *module, bool purge_mode, bool verbos
 			goto delete_this_wire;
 		} else
 		if (!used_signals.check_any(s2)) {
+			// this path shouldn't be possible: this wire is used directly (otherwise it would get cleaned up above), and indirectly
+			// used wires are a superset of those used directly
+			log_assert(false);
 			// delete wires that aren't used by anything indirectly, even though other wires may alias it
 			goto delete_this_wire;
 		}
@@ -638,7 +668,7 @@ struct OptCleanPass : public Pass {
 		}
 		extra_args(args, argidx, design);
 
-		keep_cache.reset(design);
+		keep_cache.reset(design, purge_mode);
 
 		ct_reg.setup_internals_mem();
 		ct_reg.setup_internals_anyinit();

passes/opt/opt_dff.cc

@@ -353,7 +353,7 @@ struct OptDffWorker
 					// Try a more complex conversion to plain async reset.
 					State val_neutral = ff.pol_set ? State::S0 : State::S1;
 					Const val_arst;
-					SigSpec sig_arst;
+					SigBit sig_arst;
 					if (ff.sig_clr[0] == val_neutral)
 						sig_arst = ff.sig_set[0];
 					else

passes/opt/opt_ffinv.cc

@@ -38,6 +38,7 @@ struct OptFfInvWorker
 	// - ... which has no other users
 	// - all users of FF are LUTs
 	bool push_d_inv(FfData &ff) {
+		log_assert(ff.width == 1);
 		if (index.query_is_input(ff.sig_d))
 			return false;
 		if (index.query_is_output(ff.sig_d))
@@ -90,7 +91,7 @@ struct OptFfInvWorker
 				int flip_mask = 0;
 				SigSpec sig_a = lut->getPort(ID::A);
 				for (int i = 0; i < GetSize(sig_a); i++) {
-					if (index.sigmap(sig_a[i]) == index.sigmap(ff.sig_q)) {
+					if (index.sigmap(sig_a[i]) == index.sigmap(ff.sig_q[0])) {
 						flip_mask |= 1 << i;
 					}
 				}

passes/opt/opt_lut.cc

@@ -167,7 +167,11 @@ struct OptLutWorker
 							legal = false;
 							break;
 						}
-						if (sigmap(lut_input[dlogic_conn.first]) != sigmap(lut_dlogic.second->getPort(dlogic_conn.second)))
+
+						if (lut_dlogic.second->getPort(dlogic_conn.second).size() != 1)
+							continue;
+
+						if (sigmap(lut_input[dlogic_conn.first]) != sigmap(lut_dlogic.second->getPort(dlogic_conn.second)[0]))
 						{
 							log_debug("  LUT has illegal connection to %s cell %s.%s.\n", lut_dlogic.second->type.c_str(), log_id(module), log_id(lut_dlogic.second));
 							log_debug("    LUT input A[%d] (wire %s) not connected to %s port %s (wire %s).\n", dlogic_conn.first, log_signal(lut_input[dlogic_conn.first]), lut_dlogic.second->type.c_str(), dlogic_conn.second.c_str(), log_signal(lut_dlogic.second->getPort(dlogic_conn.second)));
@@ -314,7 +318,7 @@ struct OptLutWorker
 
 			auto lutA = worklist.pop();
 			SigSpec lutA_input = sigmap(lutA->getPort(ID::A));
-			SigSpec lutA_output = sigmap(lutA->getPort(ID::Y)[0]);
+			SigBit lutA_output = sigmap(lutA->getPort(ID::Y)[0]);
 			int lutA_width = lutA->getParam(ID::WIDTH).as_int();
 			int lutA_arity = luts_arity[lutA];
 			pool<int> &lutA_dlogic_inputs = luts_dlogic_inputs[lutA];
@@ -529,12 +533,6 @@ struct OptLutPass : public Pass {
 		log("\n");
 		log("This pass combines cascaded $lut cells with unused inputs.\n");
 		log("\n");
-		log("    -dlogic <type>:<cell-port>=<LUT-input>[:<cell-port>=<LUT-input>...]\n");
-		log("        preserve connections to dedicated logic cell <type> that has ports\n");
-		log("        <cell-port> connected to LUT inputs <LUT-input>. this includes\n");
-		log("        the case where both LUT and dedicated logic input are connected to\n");
-		log("        the same constant.\n");
-		log("\n");
 		log("	-tech ice40\n");
 		log("        treat the design as a LUT-mapped circuit for the iCE40 architecture\n");
 		log("        and preserve connections to SB_CARRY as appropriate\n");

passes/opt/opt_merge.cc

@@ -272,6 +272,9 @@ struct OptMergeWorker
 				if ((!mode_share_all && !ct.cell_known(cell->type)) || !cell->known())
 					continue;
 
+				if (cell->type == ID($scopeinfo))
+					continue;
+
 				uint64_t hash = hash_cell_parameters_and_connections(cell);
 				auto r = sharemap.insert(std::make_pair(hash, cell));
 				if (!r.second) {

passes/pmgen/ice40_dsp.pmg

@@ -346,7 +346,7 @@ endmatch
 code argQ argD
 {
 	if (clock != SigBit()) {
-		if (port(ff, \CLK) != clock)
+		if (port(ff, \CLK)[0] != clock)
 			reject;
 		if (param(ff, \CLK_POLARITY).as_bool() != clock_pol)
 			reject;
@@ -393,7 +393,7 @@ endmatch
 code argQ
 	if (ff) {
 		if (clock != SigBit()) {
-			if (port(ff, \CLK) != clock)
+			if (port(ff, \CLK)[0] != clock)
 				reject;
 			if (param(ff, \CLK_POLARITY).as_bool() != clock_pol)
 				reject;

passes/pmgen/peepopt_shiftadd.pmg

@@ -103,8 +103,20 @@ code
 		new_a.append(old_a);
 	} else {
 		// data >> (...+c) transformed to data[MAX:c] >> (...)
-		new_a.append(old_a.extract_end(offset));
-
+		if(offset < GetSize(old_a)) { // some signal bits left?
+			new_a.append(old_a.extract_end(offset));
+		} else {
+			// warn user in case data is empty (no bits left)
+			std::string location = shift->get_src_attribute();
+			if (location.empty())
+				location = shift->name.str();
+			if(shift->type.in($shiftx))
+				log_warning("at %s: result of indexed part-selection is always constant (selecting from '%s' with index '%s + %d')\n", \
+							location.c_str(), log_signal(old_a), log_signal(var_signal), offset);
+			else
+				log_warning("at %s: result of shift operation is always constant (shifting '%s' by '%s + %d'-bits)\n", \
+							location.c_str(), log_signal(old_a), log_signal(var_signal), offset);
+		}
 	}
 
 	SigSpec new_b = {var_signal, SigSpec(State::S0, log2scale)};

passes/pmgen/xilinx_dsp.pmg

@@ -415,7 +415,7 @@ match ff
 	filter GetSize(port(ff, \Q)) >= offset + GetSize(argQ)
 	filter port(ff, \Q).extract(offset, GetSize(argQ)) == argQ
 
-	filter clock == SigBit() || port(ff, \CLK) == clock
+	filter clock == SigBit() || port(ff, \CLK)[0] == clock
 endmatch
 
 code argQ
@@ -465,7 +465,7 @@ match ff
 	filter GetSize(port(ff, \D)) >= offset + GetSize(argD)
 	filter port(ff, \D).extract(offset, GetSize(argD)) == argD
 
-	filter clock == SigBit() || port(ff, \CLK) == clock
+	filter clock == SigBit() || port(ff, \CLK)[0] == clock
 endmatch
 
 code argQ

passes/pmgen/xilinx_dsp48a.pmg

@@ -354,7 +354,7 @@ match ff
 	filter GetSize(port(ff, \Q)) >= offset + GetSize(argQ)
 	filter port(ff, \Q).extract(offset, GetSize(argQ)) == argQ
 
-	filter clock == SigBit() || port(ff, \CLK) == clock
+	filter clock == SigBit() || port(ff, \CLK)[0] == clock
 endmatch
 
 code argQ
@@ -404,7 +404,7 @@ match ff
 	filter GetSize(port(ff, \D)) >= offset + GetSize(argD)
 	filter port(ff, \D).extract(offset, GetSize(argD)) == argD
 
-	filter clock == SigBit() || port(ff, \CLK) == clock
+	filter clock == SigBit() || port(ff, \CLK)[0] == clock
 endmatch
 
 code argQ

passes/pmgen/xilinx_dsp_CREG.pmg

@@ -135,7 +135,7 @@ match ff
 	filter GetSize(port(ff, \Q)) >= offset + GetSize(argQ)
 	filter port(ff, \Q).extract(offset, GetSize(argQ)) == argQ
 
-	filter clock == SigBit() || port(ff, \CLK) == clock
+	filter clock == SigBit() || port(ff, \CLK)[0] == clock
 endmatch
 
 code argQ

passes/pmgen/xilinx_dsp_cascade.pmg

@@ -46,7 +46,7 @@ pattern xilinx_dsp_cascade
 udata <std::function<SigSpec(const SigSpec&)>> unextend
 udata <vector<std::tuple<Cell*,int,int,int>>> chain longest_chain
 state <Cell*> next
-state <SigSpec> clock
+state <SigBit> clock
 state <int> AREG BREG
 
 // Variables used for subpatterns
@@ -395,7 +395,7 @@ match ff
 	filter GetSize(port(ff, \Q)) >= offset + GetSize(argQ)
 	filter port(ff, \Q).extract(offset, GetSize(argQ)) == argQ
 
-	filter clock == SigBit() || port(ff, \CLK) == clock
+	filter clock == SigBit() || port(ff, \CLK)[0] == clock
 endmatch
 
 code argQ

passes/sat/async2sync.cc

@@ -41,31 +41,88 @@ struct Async2syncPass : public Pass {
 		log("reset value in the next cycle regardless of the data-in value at the time of\n");
 		log("the clock edge.\n");
 		log("\n");
+		log("    -nolower\n");
+		log("        Do not automatically run 'chformal -lower' to lower $check cells.\n");
+		log("\n");
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
-		// bool flag_noinit = false;
+		bool flag_nolower = false;
 
 		log_header(design, "Executing ASYNC2SYNC pass.\n");
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
 		{
-			// if (args[argidx] == "-noinit") {
-			// 	flag_noinit = true;
-			// 	continue;
-			// }
+			if (args[argidx] == "-nolower") {
+				flag_nolower = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
 
+		bool have_check_cells = false;
+
 		for (auto module : design->selected_modules())
 		{
 			SigMap sigmap(module);
 			FfInitVals initvals(&sigmap, module);
 
+			SigBit initstate;
+
 			for (auto cell : vector<Cell*>(module->selected_cells()))
 			{
+				if (cell->type.in(ID($print), ID($check)))
+				{
+					if (cell->type == ID($check))
+						have_check_cells = true;
+
+					bool trg_enable = cell->getParam(ID(TRG_ENABLE)).as_bool();
+					if (!trg_enable)
+						continue;
+
+					int trg_width = cell->getParam(ID(TRG_WIDTH)).as_int();
+
+					if (trg_width > 1)
+						log_error("$check cell %s with TRG_WIDTH > 1 is not support by async2sync, use clk2fflogic.\n", log_id(cell));
+
+					if (trg_width == 0) {
+						if (initstate == State::S0)
+							initstate = module->Initstate(NEW_ID);
+
+						SigBit sig_en = cell->getPort(ID::EN);
+						cell->setPort(ID::EN, module->And(NEW_ID, sig_en, initstate));
+					} else {
+						SigBit sig_en = cell->getPort(ID::EN);
+						SigSpec sig_args = cell->getPort(ID::ARGS);
+						bool trg_polarity = cell->getParam(ID(TRG_POLARITY)).as_bool();
+						SigBit sig_trg = cell->getPort(ID::TRG);
+						Wire *sig_en_q = module->addWire(NEW_ID);
+						Wire *sig_args_q = module->addWire(NEW_ID, GetSize(sig_args));
+						sig_en_q->attributes.emplace(ID::init, State::S0);
+						module->addDff(NEW_ID, sig_trg, sig_en, sig_en_q, trg_polarity, cell->get_src_attribute());
+						module->addDff(NEW_ID, sig_trg, sig_args, sig_args_q, trg_polarity, cell->get_src_attribute());
+						cell->setPort(ID::EN, sig_en_q);
+						cell->setPort(ID::ARGS, sig_args_q);
+						if (cell->type == ID($check)) {
+							SigBit sig_a = cell->getPort(ID::A);
+							Wire *sig_a_q = module->addWire(NEW_ID);
+							sig_a_q->attributes.emplace(ID::init, State::S1);
+							module->addDff(NEW_ID, sig_trg, sig_a, sig_a_q, trg_polarity, cell->get_src_attribute());
+							cell->setPort(ID::A, sig_a_q);
+						}
+					}
+
+					cell->setPort(ID::TRG, SigSpec());
+
+					cell->setParam(ID::TRG_ENABLE, false);
+					cell->setParam(ID::TRG_WIDTH, 0);
+					cell->setParam(ID::TRG_POLARITY, false);
+					cell->set_bool_attribute(ID(trg_on_gclk));
+					continue;
+				}
+
 				if (!RTLIL::builtin_ff_cell_types().count(cell->type))
 					continue;
 
@@ -273,6 +330,12 @@ struct Async2syncPass : public Pass {
 				ff.emit();
 			}
 		}
+
+		if (have_check_cells && !flag_nolower) {
+			log_push();
+			Pass::call(design, "chformal -lower");
+			log_pop();
+		}
 	}
 } Async2syncPass;
 

passes/sat/clk2fflogic.cc

@@ -48,6 +48,9 @@ struct Clk2fflogicPass : public Pass {
 		log("reset value in the next cycle regardless of the data-in value at the time of\n");
 		log("the clock edge.\n");
 		log("\n");
+		log("    -nolower\n");
+		log("        Do not automatically run 'chformal -lower' to lower $check cells.\n");
+		log("\n");
 	}
 	// Active-high sampled and current value of a level-triggered control signal. Initial sampled values is low/non-asserted.
 	SampledSig sample_control(Module *module, SigSpec sig, bool polarity, bool is_fine) {
@@ -117,21 +120,23 @@ struct Clk2fflogicPass : public Pass {
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
-		// bool flag_noinit = false;
+		bool flag_nolower = false;
 
 		log_header(design, "Executing CLK2FFLOGIC pass (convert clocked FFs to generic $ff cells).\n");
 
 		size_t argidx;
 		for (argidx = 1; argidx < args.size(); argidx++)
 		{
-			// if (args[argidx] == "-noinit") {
-			// 	flag_noinit = true;
-			// 	continue;
-			// }
+			if (args[argidx] == "-nolower") {
+				flag_nolower = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);
 
+		bool have_check_cells = false;
+
 		for (auto module : design->selected_modules())
 		{
 			SigMap sigmap(module);
@@ -194,79 +199,138 @@ struct Clk2fflogicPass : public Pass {
 				mem.emit();
 			}
 
+			SigBit initstate;
+
 			for (auto cell : vector<Cell*>(module->selected_cells()))
 			{
-				SigSpec qval;
-				if (RTLIL::builtin_ff_cell_types().count(cell->type)) {
-					FfData ff(&initvals, cell);
+				if (cell->type.in(ID($print), ID($check)))
+				{
+					if (cell->type == ID($check))
+						have_check_cells = true;
 
-					if (ff.has_gclk) {
-						// Already a $ff or $_FF_ cell.
+					bool trg_enable = cell->getParam(ID(TRG_ENABLE)).as_bool();
+					if (!trg_enable)
 						continue;
-					}
 
-					if (ff.has_clk) {
-						log("Replacing %s.%s (%s): CLK=%s, D=%s, Q=%s\n",
-								log_id(module), log_id(cell), log_id(cell->type),
-								log_signal(ff.sig_clk), log_signal(ff.sig_d), log_signal(ff.sig_q));
-					} else if (ff.has_aload) {
-						log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n",
-								log_id(module), log_id(cell), log_id(cell->type),
-								log_signal(ff.sig_aload), log_signal(ff.sig_ad), log_signal(ff.sig_q));
+					int trg_width = cell->getParam(ID(TRG_WIDTH)).as_int();
+
+					if (trg_width == 0) {
+						if (initstate == State::S0)
+							initstate = module->Initstate(NEW_ID);
+
+						SigBit sig_en = cell->getPort(ID::EN);
+						cell->setPort(ID::EN, module->And(NEW_ID, sig_en, initstate));
 					} else {
-						// $sr.
-						log("Replacing %s.%s (%s): SET=%s, CLR=%s, Q=%s\n",
-								log_id(module), log_id(cell), log_id(cell->type),
-								log_signal(ff.sig_set), log_signal(ff.sig_clr), log_signal(ff.sig_q));
+						SigBit sig_en = cell->getPort(ID::EN);
+						SigSpec sig_args = cell->getPort(ID::ARGS);
+						Const trg_polarity = cell->getParam(ID(TRG_POLARITY));
+						SigSpec sig_trg = cell->getPort(ID::TRG);
+
+						SigSpec sig_trg_sampled;
+
+						for (auto const &bit : sig_trg)
+							sig_trg_sampled.append(sample_control_edge(module, bit, trg_polarity[GetSize(sig_trg_sampled)] == State::S1, false));
+						SigSpec sig_args_sampled = sample_data(module, sig_args, Const(State::S0, GetSize(sig_args)), false, false).sampled;
+						SigBit sig_en_sampled = sample_data(module, sig_en, State::S0, false, false).sampled;
+
+						SigBit sig_trg_combined = module->ReduceOr(NEW_ID, sig_trg_sampled);
+
+						cell->setPort(ID::EN, module->And(NEW_ID, sig_en_sampled, sig_trg_combined));
+						cell->setPort(ID::ARGS, sig_args_sampled);
+						if (cell->type == ID($check)) {
+							SigBit sig_a = cell->getPort(ID::A);
+							SigBit sig_a_sampled = sample_data(module, sig_a, State::S1, false, false).sampled;
+							cell->setPort(ID::A, sig_a_sampled);
+						}
 					}
 
-					ff.remove();
+					cell->setPort(ID::TRG, SigSpec());
 
-					if (ff.has_clk)
-						ff.unmap_ce_srst();
+					cell->setParam(ID::TRG_ENABLE, false);
+					cell->setParam(ID::TRG_WIDTH, 0);
+					cell->setParam(ID::TRG_POLARITY, false);
+					cell->set_bool_attribute(ID(trg_on_gclk));
 
-					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
-						auto sampled_d = sample_data(module, ff.sig_d, RTLIL::Const(State::S0, ff.width), ff.is_fine);
-						auto clk_edge = sample_control_edge(module, ff.sig_clk, ff.pol_clk, ff.is_fine);
-						next_q = mux(module, next_q, sampled_d.sampled, clk_edge, ff.is_fine);
-					}
-
-					SampledSig sampled_aload, sampled_ad, sampled_set, sampled_clr, sampled_arst;
-					// The check for a constant sig_aload is also done by opt_dff, but when using verific and running
-					// clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids
-					// generating a lot of extra logic.
-					bool has_nonconst_aload = ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1);
-					if (has_nonconst_aload) {
-						sampled_aload = sample_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine);
-						// The init value for the sampled ad is never used, so we can set it to fixed zero, reducing uninit'd FFs
-						sampled_ad = sample_data(module, ff.sig_ad, RTLIL::Const(State::S0, ff.width), ff.is_fine);
-					}
-					if (ff.has_sr) {
-						sampled_set = sample_control(module, ff.sig_set, ff.pol_set, ff.is_fine);
-						sampled_clr = sample_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine);
-					}
-					if (ff.has_arst)
-						sampled_arst = sample_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine);
-
-					// First perform updates using _only_ sampled values, then again using _only_ current values. Unlike the previous
-					// implementation, this approach correctly handles all the cases of multiple signals changing simultaneously.
-					for (int current = 0; current < 2; current++) {
-						if (has_nonconst_aload)
-							next_q = mux(module, next_q, sampled_ad[current], sampled_aload[current], ff.is_fine);
-						if (ff.has_sr)
-							next_q = bitwise_sr(module, next_q, sampled_set[current], sampled_clr[current], ff.is_fine);
-						if (ff.has_arst)
-							next_q = mux(module, next_q, ff.val_arst, sampled_arst[current], ff.is_fine);
-					}
-
-					module->connect(ff.sig_q, next_q);
+					continue;
 				}
+
+				if (!RTLIL::builtin_ff_cell_types().count(cell->type))
+					continue;
+
+				FfData ff(&initvals, cell);
+
+				if (ff.has_gclk) {
+					// Already a $ff or $_FF_ cell.
+					continue;
+				}
+
+				if (ff.has_clk) {
+					log("Replacing %s.%s (%s): CLK=%s, D=%s, Q=%s\n",
+							log_id(module), log_id(cell), log_id(cell->type),
+							log_signal(ff.sig_clk), log_signal(ff.sig_d), log_signal(ff.sig_q));
+				} else if (ff.has_aload) {
+					log("Replacing %s.%s (%s): EN=%s, D=%s, Q=%s\n",
+							log_id(module), log_id(cell), log_id(cell->type),
+							log_signal(ff.sig_aload), log_signal(ff.sig_ad), log_signal(ff.sig_q));
+				} else {
+					// $sr.
+					log("Replacing %s.%s (%s): SET=%s, CLR=%s, Q=%s\n",
+							log_id(module), log_id(cell), log_id(cell->type),
+							log_signal(ff.sig_set), log_signal(ff.sig_clr), log_signal(ff.sig_q));
+				}
+
+				ff.remove();
+
+				if (ff.has_clk)
+					ff.unmap_ce_srst();
+
+				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
+					auto sampled_d = sample_data(module, ff.sig_d, RTLIL::Const(State::S0, ff.width), ff.is_fine);
+					auto clk_edge = sample_control_edge(module, ff.sig_clk, ff.pol_clk, ff.is_fine);
+					next_q = mux(module, next_q, sampled_d.sampled, clk_edge, ff.is_fine);
+				}
+
+				SampledSig sampled_aload, sampled_ad, sampled_set, sampled_clr, sampled_arst;
+				// The check for a constant sig_aload is also done by opt_dff, but when using verific and running
+				// clk2fflogic before opt_dff (which does more and possibly unwanted optimizations) this check avoids
+				// generating a lot of extra logic.
+				bool has_nonconst_aload = ff.has_aload && ff.sig_aload != (ff.pol_aload ? State::S0 : State::S1);
+				if (has_nonconst_aload) {
+					sampled_aload = sample_control(module, ff.sig_aload, ff.pol_aload, ff.is_fine);
+					// The init value for the sampled ad is never used, so we can set it to fixed zero, reducing uninit'd FFs
+					sampled_ad = sample_data(module, ff.sig_ad, RTLIL::Const(State::S0, ff.width), ff.is_fine);
+				}
+				if (ff.has_sr) {
+					sampled_set = sample_control(module, ff.sig_set, ff.pol_set, ff.is_fine);
+					sampled_clr = sample_control(module, ff.sig_clr, ff.pol_clr, ff.is_fine);
+				}
+				if (ff.has_arst)
+					sampled_arst = sample_control(module, ff.sig_arst, ff.pol_arst, ff.is_fine);
+
+				// First perform updates using _only_ sampled values, then again using _only_ current values. Unlike the previous
+				// implementation, this approach correctly handles all the cases of multiple signals changing simultaneously.
+				for (int current = 0; current < 2; current++) {
+					if (has_nonconst_aload)
+						next_q = mux(module, next_q, sampled_ad[current], sampled_aload[current], ff.is_fine);
+					if (ff.has_sr)
+						next_q = bitwise_sr(module, next_q, sampled_set[current], sampled_clr[current], ff.is_fine);
+					if (ff.has_arst)
+						next_q = mux(module, next_q, ff.val_arst, sampled_arst[current], ff.is_fine);
+				}
+
+				module->connect(ff.sig_q, next_q);
+
 			}
 		}
 
+		if (have_check_cells && !flag_nolower) {
+			log_push();
+			Pass::call(design, "chformal -lower");
+			log_pop();
+		}
 	}
 } Clk2fflogicPass;
 

passes/sat/sim.cc

@@ -813,7 +813,7 @@ struct SimInstance
 		}
 	}
 
-	void update_ph3(bool check_assertions)
+	void update_ph3(bool gclk_trigger)
 	{
 		for (auto &it : ff_database)
 		{
@@ -858,49 +858,53 @@ struct SimInstance
 			Const en = get_state(cell->getPort(ID::EN));
 			Const args = get_state(cell->getPort(ID::ARGS));
 
-			if (!en.as_bool())
-				goto update_print;
+			bool sampled = trg_en && trg.size() > 0;
 
-			if (trg.size() > 0 && trg_en) {
-				Const trg_pol = cell->getParam(ID::TRG_POLARITY);
-				for (int i = 0; i < trg.size(); i++) {
-					bool pol = trg_pol[i] == State::S1;
-					State curr = trg[i], past = print.past_trg[i];
-					if (pol && curr == State::S1 && past == State::S0)
+			if (sampled ? print.past_en.as_bool() : en.as_bool()) {
+				if (sampled) {
+					sampled = true;
+					Const trg_pol = cell->getParam(ID::TRG_POLARITY);
+					for (int i = 0; i < trg.size(); i++) {
+						bool pol = trg_pol[i] == State::S1;
+						State curr = trg[i], past = print.past_trg[i];
+						if (pol && curr == State::S1 && past == State::S0)
+							triggered = true;
+						if (!pol && curr == State::S0 && past == State::S1)
+							triggered = true;
+					}
+				} else if (trg_en) {
+					// initial $print (TRG width = 0, TRG_ENABLE = true)
+					if (!print.initial_done && en != print.past_en)
 						triggered = true;
-					if (!pol && curr == State::S0 && past == State::S1)
+				} else if (cell->get_bool_attribute(ID(trg_on_gclk))) {
+					// unified $print for cycle based FV semantics
+					triggered = gclk_trigger;
+				} else {
+					// always @(*) $print
+					if (args != print.past_args || en != print.past_en)
 						triggered = true;
 				}
-			} else if (trg_en) {
-				// initial $print (TRG width = 0, TRG_ENABLE = true)
-				if (!print.initial_done && en != print.past_en)
-					triggered = true;
-			} else {
-				// always @(*) $print
-				if (args != print.past_args || en != print.past_en)
-					triggered = true;
-			}
 
-			if (triggered) {
-				int pos = 0;
-				for (auto &part : print.fmt.parts) {
-					part.sig = args.extract(pos, part.sig.size());
-					pos += part.sig.size();
+				if (triggered) {
+					int pos = 0;
+					for (auto &part : print.fmt.parts) {
+						part.sig = (sampled ? print.past_args : args).extract(pos, part.sig.size());
+						pos += part.sig.size();
+					}
+
+					std::string rendered = print.fmt.render();
+					log("%s", rendered.c_str());
+					shared->display_output.emplace_back(shared->step, this, cell, rendered);
 				}
-
-				std::string rendered = print.fmt.render();
-				log("%s", rendered.c_str());
-				shared->display_output.emplace_back(shared->step, this, cell, rendered);
 			}
 
-		update_print:
 			print.past_trg = trg;
 			print.past_en = en;
 			print.past_args = args;
 			print.initial_done = true;
 		}
 
-		if (check_assertions)
+		if (gclk_trigger)
 		{
 			for (auto cell : formal_database)
 			{
@@ -932,7 +936,7 @@ struct SimInstance
 		}
 
 		for (auto it : children)
-			it.second->update_ph3(check_assertions);
+			it.second->update_ph3(gclk_trigger);
 	}
 
 	void set_initstate_outputs(State state)

passes/techmap/extract_fa.cc

@@ -281,7 +281,7 @@ struct ExtractFaWorker
 	void assign_new_driver(SigBit bit, SigBit new_driver)
 	{
 		Cell *cell = driver.at(bit);
-		if (sigmap(cell->getPort(ID::Y)) == bit) {
+		if (sigmap(cell->getPort(ID::Y)) == SigSpec(bit)) {
 			cell->setPort(ID::Y, module->addWire(NEW_ID));
 			module->connect(bit, new_driver);
 		}

passes/techmap/flatten.cc

@@ -46,24 +46,6 @@ IdString map_name(RTLIL::Cell *cell, T *object)
 	return cell->module->uniquify(concat_name(cell, object->name));
 }
 
-template<class T>
-void map_attributes(RTLIL::Cell *cell, T *object, IdString orig_object_name)
-{
-	if (object->has_attribute(ID::src))
-		object->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src));
-
-	// Preserve original names via the hdlname attribute, but only for objects with a fully public name.
-	if (cell->name[0] == '\\' && (object->has_attribute(ID::hdlname) || orig_object_name[0] == '\\')) {
-		std::vector<std::string> hierarchy;
-		if (object->has_attribute(ID::hdlname))
-			hierarchy = object->get_hdlname_attribute();
-		else
-			hierarchy.push_back(orig_object_name.str().substr(1));
-		hierarchy.insert(hierarchy.begin(), cell->name.str().substr(1));
-		object->set_hdlname_attribute(hierarchy);
-	}
-}
-
 void map_sigspec(const dict<RTLIL::Wire*, RTLIL::Wire*> &map, RTLIL::SigSpec &sig, RTLIL::Module *into = nullptr)
 {
 	vector<SigChunk> chunks = sig;
@@ -76,6 +58,54 @@ void map_sigspec(const dict<RTLIL::Wire*, RTLIL::Wire*> &map, RTLIL::SigSpec &si
 struct FlattenWorker
 {
 	bool ignore_wb = false;
+	bool create_scopeinfo = true;
+	bool create_scopename = false;
+
+	template<class T>
+	void map_attributes(RTLIL::Cell *cell, T *object, IdString orig_object_name)
+	{
+		if (!create_scopeinfo && object->has_attribute(ID::src))
+			object->add_strpool_attribute(ID::src, cell->get_strpool_attribute(ID::src));
+
+		// Preserve original names via the hdlname attribute, but only for objects with a fully public name.
+		// If the '-scopename' option is used, also preserve the containing scope of private objects if their scope is fully public.
+		if (cell->name[0] == '\\') {
+			if (object->has_attribute(ID::hdlname) || orig_object_name[0] == '\\') {
+				std::string new_hdlname;
+
+				if (cell->has_attribute(ID::hdlname)) {
+					new_hdlname = cell->get_string_attribute(ID(hdlname));
+				} else {
+					log_assert(!cell->name.empty());
+					new_hdlname = cell->name.c_str() + 1;
+				}
+				new_hdlname += ' ';
+
+				if (object->has_attribute(ID::hdlname)) {
+					new_hdlname += object->get_string_attribute(ID(hdlname));
+				} else {
+					log_assert(!orig_object_name.empty());
+					new_hdlname += orig_object_name.c_str() + 1;
+				}
+				object->set_string_attribute(ID(hdlname), new_hdlname);
+			} else if (object->has_attribute(ID(scopename))) {
+				std::string new_scopename;
+
+				if (cell->has_attribute(ID::hdlname)) {
+					new_scopename = cell->get_string_attribute(ID(hdlname));
+				} else {
+					log_assert(!cell->name.empty());
+					new_scopename = cell->name.c_str() + 1;
+				}
+				new_scopename += ' ';
+				new_scopename += object->get_string_attribute(ID(scopename));
+				object->set_string_attribute(ID(scopename), new_scopename);
+			} else if (create_scopename) {
+				log_assert(!cell->name.empty());
+				object->set_string_attribute(ID(scopename), cell->name.c_str() + 1);
+			}
+		}
+	}
 
 	void flatten_cell(RTLIL::Design *design, RTLIL::Module *module, RTLIL::Cell *cell, RTLIL::Module *tpl, SigMap &sigmap, std::vector<RTLIL::Cell*> &new_cells)
 	{
@@ -220,7 +250,33 @@ struct FlattenWorker
 			sigmap.add(new_conn.first, new_conn.second);
 		}
 
+		RTLIL::Cell *scopeinfo = nullptr;
+		RTLIL::IdString cell_name = cell->name;
+
+		if (create_scopeinfo && cell_name.isPublic())
+		{
+			// The $scopeinfo's name will be changed below after removing the flattened cell
+			scopeinfo = module->addCell(NEW_ID, ID($scopeinfo));
+			scopeinfo->setParam(ID::TYPE, RTLIL::Const("module"));
+
+			for (auto const &attr : cell->attributes)
+			{
+				if (attr.first == ID::hdlname)
+					scopeinfo->attributes.insert(attr);
+				else
+					scopeinfo->attributes.emplace(stringf("\\cell_%s", RTLIL::unescape_id(attr.first).c_str()), attr.second);
+			}
+
+			for (auto const &attr : tpl->attributes)
+				scopeinfo->attributes.emplace(stringf("\\module_%s", RTLIL::unescape_id(attr.first).c_str()), attr.second);
+
+			scopeinfo->attributes.emplace(ID(module), RTLIL::unescape_id(tpl->name));
+		}
+
 		module->remove(cell);
+
+		if (scopeinfo != nullptr)
+			module->rename(scopeinfo, cell_name);
 	}
 
 	void flatten_module(RTLIL::Design *design, RTLIL::Module *module, pool<RTLIL::Module*> &used_modules)
@@ -275,6 +331,20 @@ struct FlattenPass : public Pass {
 		log("    -wb\n");
 		log("        Ignore the 'whitebox' attribute on cell implementations.\n");
 		log("\n");
+		log("    -noscopeinfo\n");
+		log("        Do not create '$scopeinfo' cells that preserve attributes of cells and\n");
+		log("        modules that were removed during flattening. With this option, the\n");
+		log("        'src' attribute of a given cell is merged into all objects replacing\n");
+		log("        that cell, with multiple distinct 'src' locations separated by '|'.\n");
+		log("        Without this option these 'src' locations can be found via the\n");
+		log("        cell_src' and 'module_src' attribute of '$scopeinfo' cells.\n");
+		log("\n");
+		log("    -scopename\n");
+		log("        Create 'scopename' attributes for objects with a private name. This\n");
+		log("        attribute records the 'hdlname' of the enclosing scope. For objects\n");
+		log("        with a public name the enclosing scope can be found via their\n");
+		log("        'hdlname' attribute.\n");
+		log("\n");
 	}
 	void execute(std::vector<std::string> args, RTLIL::Design *design) override
 	{
@@ -289,6 +359,14 @@ struct FlattenPass : public Pass {
 				worker.ignore_wb = true;
 				continue;
 			}
+			if (args[argidx] == "-noscopeinfo") {
+				worker.create_scopeinfo = false;
+				continue;
+			}
+			if (args[argidx] == "-scopename") {
+				worker.create_scopename = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(args, argidx, design);

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
 
@@ -2741,3 +2763,10 @@ assign Y = A;
 endmodule
 
 // --------------------------------------------------------
+
+(* noblackbox *)
+module \$scopeinfo ();
+
+parameter TYPE = "";
+
+endmodule

techlibs/common/synth.cc

@@ -60,7 +60,7 @@ struct SynthPass : public ScriptPass {
 		log("        do not run abc (as if yosys was compiled without ABC support)\n");
 		log("\n");
 		log("    -booth\n");
-		log("        run the booth pass to convert $mul to Booth encoded multipliers");
+		log("        run the booth pass to map $mul to Booth encoded multipliers\n");
 		log("\n");
 		log("    -noalumacc\n");
 		log("        do not run 'alumacc' pass. i.e. keep arithmetic operators in\n");
@@ -230,13 +230,13 @@ struct SynthPass : public ScriptPass {
 
 		if (check_label("coarse")) {
 			run("proc");
-			if (help_mode || flatten)
+			if (flatten || help_mode)
 				run("flatten", "  (if -flatten)");
 			run("opt_expr");
 			run("opt_clean");
 			run("check");
 			run("opt -nodffe -nosdff");
-			if (!nofsm)
+			if (!nofsm || help_mode)
 				run("fsm" + fsm_opts, "      (unless -nofsm)");
 			run("opt");
 			run("wreduce");
@@ -246,8 +246,8 @@ struct SynthPass : public ScriptPass {
 				run("techmap -map +/cmp2lut.v -map +/cmp2lcu.v", " (if -lut)");
 			else if (lut)
 				run(stringf("techmap -map +/cmp2lut.v -map +/cmp2lcu.v -D LUT_WIDTH=%d", lut));
-			if (booth)
-				run("booth");
+			if (booth || help_mode)
+				run("booth", "    (if -booth)");
 			if (!noalumacc)
 				run("alumacc", "  (unless -noalumacc)");
 			if (!noshare)
@@ -274,7 +274,7 @@ struct SynthPass : public ScriptPass {
 			}
 			run("opt -fast");
 
-			if (!noabc && !flowmap) {
+			if ((!noabc && !flowmap) || help_mode) {
 #ifdef YOSYS_ENABLE_ABC
 				if (help_mode) {
 					run(abc + " -fast", "       (unless -noabc, unless -lut)");

techlibs/gowin/brams.txt

@@ -1,13 +1,11 @@
 ram block $__GOWIN_SP_ {
 	abits 14;
 	widths 1 2 4 9 18 36 per_port;
-	byte 9;
 	cost 128;
 	init no_undef;
 	port srsw "A" {
 		clock posedge;
 		clken;
-		wrbe_separate;
 		option "RESET_MODE" "SYNC" {
 			rdsrst zero ungated;
 		}
@@ -30,13 +28,11 @@ ram block $__GOWIN_SP_ {
 ram block $__GOWIN_DP_ {
 	abits 14;
 	widths 1 2 4 9 18 per_port;
-	byte 9;
 	cost 128;
 	init no_undef;
 	port srsw "A" "B" {
 		clock posedge;
 		clken;
-		wrbe_separate;
 		option "RESET_MODE" "SYNC" {
 			rdsrst zero ungated;
 		}
@@ -59,7 +55,6 @@ ram block $__GOWIN_DP_ {
 ram block $__GOWIN_SDP_ {
 	abits 14;
 	widths 1 2 4 9 18 36 per_port;
-	byte 9;
 	cost 128;
 	init no_undef;
 	port sr "R" {
@@ -76,6 +71,5 @@ ram block $__GOWIN_SDP_ {
 	port sw "W" {
 		clock posedge;
 		clken;
-		wrbe_separate;
 	}
 }

techlibs/gowin/brams_map.v

@@ -14,8 +14,7 @@
 `define x8_width(width) (width / 9 * 8 + width % 9)
 `define x8_rd_data(data) {1'bx, data[31:24], 1'bx, data[23:16], 1'bx, data[15:8], 1'bx, data[7:0]}
 `define x8_wr_data(data) {data[34:27], data[25:18], data[16:9], data[7:0]}
-`define wre(width, wr_en, wr_be) (width < 18 ? wr_en | wr_be[0] : wr_en)
-`define addrbe(width, addr, wr_be) (width < 18 ? addr : {addr[13:4], wr_be})
+`define addrbe_always(width, addr) (width < 18 ? addr :  width == 18 ? {addr[13:4], 4'b0011} : {addr[13:5], 5'b01111})
 
 
 `define INIT(func) \
@@ -90,7 +89,6 @@ parameter INIT = 0;
 parameter OPTION_RESET_MODE = "SYNC";
 
 parameter PORT_A_WIDTH = 36;
-parameter PORT_A_WR_BE_WIDTH = 4;
 parameter PORT_A_OPTION_WRITE_MODE = 0;
 
 input PORT_A_CLK;
@@ -99,15 +97,13 @@ input PORT_A_WR_EN;
 input PORT_A_RD_SRST;
 input PORT_A_RD_ARST;
 input [13:0] PORT_A_ADDR;
-input [PORT_A_WR_BE_WIDTH-1:0] PORT_A_WR_BE;
 input [PORT_A_WIDTH-1:0] PORT_A_WR_DATA;
 output [PORT_A_WIDTH-1:0] PORT_A_RD_DATA;
 
 `DEF_FUNCS
 
 wire RST = OPTION_RESET_MODE == "SYNC" ? PORT_A_RD_SRST : PORT_A_RD_ARST;
-wire WRE = `wre(PORT_A_WIDTH, PORT_A_WR_EN, PORT_A_WR_BE);
-wire [13:0] AD = `addrbe(PORT_A_WIDTH, PORT_A_ADDR, PORT_A_WR_BE);
+wire [13:0] AD = `addrbe_always(PORT_A_WIDTH, PORT_A_ADDR);
 
 generate
 
@@ -129,7 +125,7 @@ if (PORT_A_WIDTH < 9) begin
 		.BLKSEL(3'b000),
 		.CLK(PORT_A_CLK),
 		.CE(PORT_A_CLK_EN),
-		.WRE(WRE),
+		.WRE(PORT_A_WR_EN),
 		.RESET(RST),
 		.OCE(1'b1),
 		.AD(AD),
@@ -155,7 +151,7 @@ end else begin
 		.BLKSEL(3'b000),
 		.CLK(PORT_A_CLK),
 		.CE(PORT_A_CLK_EN),
-		.WRE(WRE),
+		.WRE(PORT_A_WR_EN),
 		.RESET(RST),
 		.OCE(1'b1),
 		.AD(AD),
@@ -176,11 +172,9 @@ parameter INIT = 0;
 parameter OPTION_RESET_MODE = "SYNC";
 
 parameter PORT_A_WIDTH = 18;
-parameter PORT_A_WR_BE_WIDTH = 2;
 parameter PORT_A_OPTION_WRITE_MODE = 0;
 
 parameter PORT_B_WIDTH = 18;
-parameter PORT_B_WR_BE_WIDTH = 2;
 parameter PORT_B_OPTION_WRITE_MODE = 0;
 
 input PORT_A_CLK;
@@ -189,7 +183,6 @@ input PORT_A_WR_EN;
 input PORT_A_RD_SRST;
 input PORT_A_RD_ARST;
 input [13:0] PORT_A_ADDR;
-input [PORT_A_WR_BE_WIDTH-1:0] PORT_A_WR_BE;
 input [PORT_A_WIDTH-1:0] PORT_A_WR_DATA;
 output [PORT_A_WIDTH-1:0] PORT_A_RD_DATA;
 
@@ -199,7 +192,6 @@ input PORT_B_WR_EN;
 input PORT_B_RD_SRST;
 input PORT_B_RD_ARST;
 input [13:0] PORT_B_ADDR;
-input [PORT_A_WR_BE_WIDTH-1:0] PORT_B_WR_BE;
 input [PORT_A_WIDTH-1:0] PORT_B_WR_DATA;
 output [PORT_A_WIDTH-1:0] PORT_B_RD_DATA;
 
@@ -207,10 +199,8 @@ output [PORT_A_WIDTH-1:0] PORT_B_RD_DATA;
 
 wire RSTA = OPTION_RESET_MODE == "SYNC" ? PORT_A_RD_SRST : PORT_A_RD_ARST;
 wire RSTB = OPTION_RESET_MODE == "SYNC" ? PORT_B_RD_SRST : PORT_B_RD_ARST;
-wire WREA = `wre(PORT_A_WIDTH, PORT_A_WR_EN, PORT_A_WR_BE);
-wire WREB = `wre(PORT_B_WIDTH, PORT_B_WR_EN, PORT_B_WR_BE);
-wire [13:0] ADA = `addrbe(PORT_A_WIDTH, PORT_A_ADDR, PORT_A_WR_BE);
-wire [13:0] ADB = `addrbe(PORT_B_WIDTH, PORT_B_ADDR, PORT_B_WR_BE);
+wire [13:0] ADA = `addrbe_always(PORT_A_WIDTH, PORT_A_ADDR);
+wire [13:0] ADB = `addrbe_always(PORT_B_WIDTH, PORT_B_ADDR);
 
 generate
 
@@ -241,7 +231,7 @@ if (PORT_A_WIDTH < 9 || PORT_B_WIDTH < 9) begin
 
 		.CLKA(PORT_A_CLK),
 		.CEA(PORT_A_CLK_EN),
-		.WREA(WREA),
+		.WREA(PORT_A_WR_EN),
 		.RESETA(RSTA),
 		.OCEA(1'b1),
 		.ADA(ADA),
@@ -250,7 +240,7 @@ if (PORT_A_WIDTH < 9 || PORT_B_WIDTH < 9) begin
 
 		.CLKB(PORT_B_CLK),
 		.CEB(PORT_B_CLK_EN),
-		.WREB(WREB),
+		.WREB(PORT_B_WR_EN),
 		.RESETB(RSTB),
 		.OCEB(1'b1),
 		.ADB(ADB),
@@ -285,7 +275,7 @@ end else begin
 
 		.CLKA(PORT_A_CLK),
 		.CEA(PORT_A_CLK_EN),
-		.WREA(WREA),
+		.WREA(PORT_A_WR_EN),
 		.RESETA(RSTA),
 		.OCEA(1'b1),
 		.ADA(ADA),
@@ -294,7 +284,7 @@ end else begin
 
 		.CLKB(PORT_B_CLK),
 		.CEB(PORT_B_CLK_EN),
-		.WREB(WREB),
+		.WREB(PORT_B_WR_EN),
 		.RESETB(RSTB),
 		.OCEB(1'b1),
 		.ADB(ADB),
@@ -315,9 +305,7 @@ parameter INIT = 0;
 parameter OPTION_RESET_MODE = "SYNC";
 
 parameter PORT_R_WIDTH = 18;
-
 parameter PORT_W_WIDTH = 18;
-parameter PORT_W_WR_BE_WIDTH = 2;
 
 input PORT_R_CLK;
 input PORT_R_CLK_EN;
@@ -330,14 +318,13 @@ input PORT_W_CLK;
 input PORT_W_CLK_EN;
 input PORT_W_WR_EN;
 input [13:0] PORT_W_ADDR;
-input [PORT_W_WR_BE_WIDTH-1:0] PORT_W_WR_BE;
 input [PORT_W_WIDTH-1:0] PORT_W_WR_DATA;
 
 `DEF_FUNCS
 
 wire RST = OPTION_RESET_MODE == "SYNC" ? PORT_R_RD_SRST : PORT_R_RD_ARST;
-wire WRE = `wre(PORT_W_WIDTH, PORT_W_WR_EN, PORT_W_WR_BE);
-wire [13:0] ADW = `addrbe(PORT_W_WIDTH, PORT_W_ADDR, PORT_W_WR_BE);
+wire [13:0] ADW = `addrbe_always(PORT_W_WIDTH, PORT_W_ADDR);
+wire WRE = PORT_W_CLK_EN & PORT_W_WR_EN;
 
 generate
 
@@ -361,7 +348,7 @@ if (PORT_W_WIDTH < 9 || PORT_R_WIDTH < 9) begin
 		.BLKSELB(3'b000),
 
 		.CLKA(PORT_W_CLK),
-		.CEA(PORT_W_CLK_EN),
+		.CEA(WRE),
 		.RESETA(1'b0),
 		.ADA(ADW),
 		.DI(DI),
@@ -394,7 +381,7 @@ end else begin
 		.BLKSELB(3'b000),
 
 		.CLKA(PORT_W_CLK),
-		.CEA(PORT_W_CLK_EN),
+		.CEA(WRE),
 		.RESETA(1'b0),
 		.ADA(ADW),
 		.DI(DI),

tests/arch/quicklogic/qlf_k6n10f/dsp.ys

@@ -107,7 +107,7 @@ reg [7:0] i = 0;
 always @(posedge clk) begin
 	if (i < VECTORLEN) begin
 		// FIXME: for some reason the first assert fails (despite comparing zero to zero)
-		if (i > 0) 
+		if (i > 0)
 			assert(y == y_expected);
 		i <= i + 1;
 	end
@@ -117,4 +117,5 @@ EOF
 read_verilog +/quicklogic/qlf_k6n10f/dsp_sim.v
 hierarchy -top testbench
 proc
+async2sync
 sim -assert -q -clock clk -n 20

tests/arch/quicklogic/qlf_k6n10f/mem_gen.py

@@ -36,7 +36,7 @@ blockram_tests: "list[tuple[list[tuple[str, int]], str, list[str]]]" = [
     ([("ADDRESS_WIDTH", 14), ("DATA_WIDTH",  2)], "sync_ram_*dp", ["-assert-count 1 t:TDP36K", "-assert-count 1 t:TDP36K a:port_a_width=2 %i"]),
     ([("ADDRESS_WIDTH", 15), ("DATA_WIDTH",  1)], "sync_ram_*dp", ["-assert-count 1 t:TDP36K", "-assert-count 1 t:TDP36K a:port_a_width=1 %i"]),
 
-    # 2x asymmetric (1024x36bit write / 2048x18bit read or vice versa = 1TDP36K) 
+    # 2x asymmetric (1024x36bit write / 2048x18bit read or vice versa = 1TDP36K)
     ([("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 18), ("SHIFT_VAL", 1)], "sync_ram_sdp_w*r", ["-assert-count 1 t:TDP36K"]),
     ([("ADDRESS_WIDTH", 11), ("DATA_WIDTH", 16), ("SHIFT_VAL", 1)], "sync_ram_sdp_w*r", ["-assert-count 1 t:TDP36K"]),
     ([("ADDRESS_WIDTH", 12), ("DATA_WIDTH",  9), ("SHIFT_VAL", 1)], "sync_ram_sdp_w*r", ["-assert-count 1 t:TDP36K"]),
@@ -131,6 +131,7 @@ read_verilog -defer -formal mem_tb.v
 chparam{param_str} -set VECTORLEN {vectorlen} TB
 hierarchy -top TB -check
 prep
+async2sync
 log ** CHECKING SIMULATION FOR TEST {top} WITH PARAMS{param_str}
 sim -clock clk -n {vectorlen} -assert
 """
@@ -254,16 +255,16 @@ sim_tests: list[TestClass] = [
             {"rq_a": 0x5678},
         ]
     ),
-    TestClass( # basic TDP test 
+    TestClass( # basic TDP test
         # note that the testbench uses ra and wa, while the common TDP model
         # uses a shared address
         params={"ADDRESS_WIDTH": 10, "DATA_WIDTH": 36},
         top="sync_ram_tdp",
         assertions=[],
         test_steps=[
-            {"wce_a": 1, "ra_a": 0x0A,      "wce_b": 1, "ra_b": 0xBA, 
+            {"wce_a": 1, "ra_a": 0x0A,      "wce_b": 1, "ra_b": 0xBA,
              "wd_a": 0xdeadbeef,            "wd_b": 0x5a5a5a5a},
-            {"wce_a": 1, "ra_a": 0xFF, 
+            {"wce_a": 1, "ra_a": 0xFF,
              "wd_a": 0},
             {"rce_a": 1, "ra_a": 0x0A,      "rce_b": 1, "ra_b": 0x0A},
             {"rq_a": 0xdeadbeef,            "rq_b": 0xdeadbeef},
@@ -276,9 +277,9 @@ sim_tests: list[TestClass] = [
         top="sync_ram_tdp",
         assertions=[],
         test_steps=[
-            {"wce_a": 1, "ra_a": 0x0F,      "wce_b": 1, "ra_b": 0xBA, 
+            {"wce_a": 1, "ra_a": 0x0F,      "wce_b": 1, "ra_b": 0xBA,
              "wd_a": 0xdeadbeef,            "wd_b": 0x5a5a5a5a},
-            {"wce_a": 1, "ra_a": 0xFF, 
+            {"wce_a": 1, "ra_a": 0xFF,
              "wd_a": 0},
             {"rce_a": 1, "ra_a": 0x0F,      "rce_b": 1, "ra_b": 0x0A},
             {"rq_a": 0,                     "rq_b": 0x00005a5a},
@@ -291,7 +292,7 @@ sim_tests: list[TestClass] = [
         top="sync_ram_tdp",
         assertions=[],
         test_steps=[
-            {"wce_a": 1, "ra_a": 0x0A,      "wce_b": 1, "ra_b": 0xBA, 
+            {"wce_a": 1, "ra_a": 0x0A,      "wce_b": 1, "ra_b": 0xBA,
              "wd_a": 0xdeadbeef,            "wd_b": 0x5a5a5a5a},
             {"wce_a": 1, "ra_a": 0xBA,      "rce_b": 1, "ra_b": 0xBA,
              "wd_a": 0xa5a5a5a5},
@@ -409,7 +410,7 @@ for sim_test in sim_tests:
             fn = f"t_mem{i}.ys"
             f = open(fn, mode="w")
             j = 0
-        
+
         # output yosys script test file
         print(
             blockram_template.format(param_str=param_str, top=top),

tests/arch/quicklogic/qlf_k6n10f/meminit.ys

@@ -10,5 +10,6 @@ select -assert-count 1 t:TDP36K a:is_split=0 %i
 select -assert-count 1 t:TDP36K a:was_split_candidate=0 %i
 read_verilog +/quicklogic/common/cells_sim.v +/quicklogic/qlf_k6n10f/cells_sim.v +/quicklogic/qlf_k6n10f/brams_sim.v +/quicklogic/qlf_k6n10f/sram1024x18_mem.v +/quicklogic/qlf_k6n10f/ufifo_ctl.v +/quicklogic/qlf_k6n10f/TDP18K_FIFO.v
 prep
+async2sync
 hierarchy -top top
 sim -assert -q -n 12 -clock clk

tests/arch/xilinx/dsp_abc9.ys

@@ -30,6 +30,7 @@ module top(output [42:0] P);
 assert property (P == 42*42);
 endmodule
 EOT
+async2sync
 techmap -map +/xilinx/xc7_dsp_map.v
 verilog_defaults -add -D ALLOW_WHITEBOX_DSP48E1
 synth_xilinx -abc9

tests/gen-tests-makefile.sh

@@ -75,7 +75,7 @@ generate_tests() {
 	if [[ $do_sv = true ]]; then
 		for x in *.sv; do
 			if [ ! -f "${x%.sv}.ys"  ]; then
-				generate_ys_test "$x" "-p \"prep -top top; sat -enable_undef -verify -prove-asserts\" $yosys_args"
+				generate_ys_test "$x" "-p \"prep -top top; async2sync; sat -enable_undef -verify -prove-asserts\" $yosys_args"
 			fi;
 		done
 	fi;

tests/sat/asserts.ys

@@ -1,3 +1,3 @@
 read_verilog -sv asserts.v
-hierarchy; proc; opt
+hierarchy; proc; opt; async2sync
 sat -verify -seq 1 -set-at 1 rst 1 -tempinduct -prove-asserts

tests/sat/asserts_seq.ys

@@ -1,5 +1,5 @@
 read_verilog -sv asserts_seq.v
-hierarchy; proc; opt
+hierarchy; proc; opt; async2sync
 
 sat -verify  -prove-asserts -tempinduct -seq 1 test_001
 sat -falsify -prove-asserts -tempinduct -seq 1 test_002

tests/sat/initval.ys

@@ -1,5 +1,5 @@
 read_verilog -sv initval.v
-proc;;
+proc; async2sync;;
 
 sat -seq 10 -prove-asserts
 

tests/sat/sizebits.sv

@@ -10,23 +10,41 @@ wire [3:0]z[7:2][2:9];
 //wire [$size(y)-1:0]y_size;
 //wire [$size(z)-1:0]z_size;
 
+assert property ($dimensions(t) == 1);
+assert property ($dimensions(x) == 1);
+assert property ($dimensions({3{x}}) == 1);
+assert property ($dimensions(y) == 2);
+assert property ($dimensions(y[2]) == 1);
+assert property ($dimensions(z) == 3);
+assert property ($dimensions(z[3]) == 2);
+assert property ($dimensions(z[3][3]) == 1);
+
+assert property ($unpacked_dimensions(t) == 0);
+assert property ($unpacked_dimensions(x) == 0);
+assert property ($unpacked_dimensions({3{x}}) == 0);
+assert property ($unpacked_dimensions(y) == 1);
+assert property ($unpacked_dimensions(y[2]) == 0);
+assert property ($unpacked_dimensions(z) == 2);
+assert property ($unpacked_dimensions(z[3]) == 1);
+assert property ($unpacked_dimensions(z[3][3]) == 0);
+
 assert property ($size(t) == 1);
 assert property ($size(x) == 4);
 assert property ($size({3{x}}) == 3*4);
 assert property ($size(y) == 6);
 assert property ($size(y, 1) == 6);
 assert property ($size(y, (1+1)) == 4);
+assert property ($size(y[2], 1) == 4);
 // This is unsupported at the moment
-//assert property ($size(y[2], 1) == 4);
 //assert property ($size(y[2][1], 1) == 1);
 
 assert property ($size(z) == 6);
 assert property ($size(z, 1) == 6);
 assert property ($size(z, 2) == 8);
 assert property ($size(z, 3) == 4);
-// This is unsupported at the moment
 assert property ($size(z[3], 1) == 8);
 assert property ($size(z[3][3], 1) == 4);
+// This is unsupported at the moment
 //assert property ($size(z[3][3][3], 1) == 1);
 // This should trigger an error if enabled (it does).
 //assert property ($size(z, 4) == 4);
@@ -90,4 +108,17 @@ assert property ($right(z, 3) == 0);
 assert property ($right(z[3]) == 9);
 assert property ($right(z[3][3]) == 0);
 assert property ($right(z[3], 2) == 0);
+
+assert property ($increment(x) == 1);
+assert property ($increment(y) == -1);
+assert property ($increment(y, 1) == -1);
+assert property ($increment(y, (1+1)) == 1);
+
+assert property ($increment(z) == 1);
+assert property ($increment(z, 1) == 1);
+assert property ($increment(z, 2) == -1);
+assert property ($increment(z, 3) == 1);
+assert property ($increment(z[3]) == -1);
+assert property ($increment(z[3][3]) == 1);
+assert property ($increment(z[3], 2) == 1);
 endmodule

tests/sat/sizebits.ys

@@ -1,2 +1,2 @@
 read_verilog -sv sizebits.sv
-prep; sat -verify -prove-asserts
+prep; async2sync; sat -verify -prove-asserts

tests/simple/arrays03.sv

@@ -0,0 +1,49 @@
+// Test multidimensional packed arrays
+
+typedef logic [0:3][7:0] reg2dim_t;
+typedef logic  [7:0] reg8_t;
+typedef reg8_t [0:3] reg2dim1_t;
+
+module pcktest1 (
+    input  logic  clk,
+    input  logic [0:3][7:0] in,
+    input  logic [1:0] ix,
+    output reg8_t out
+);
+    always_ff @(posedge clk) begin
+        out <= in[ix];
+    end
+endmodule
+
+module pcktest2 (
+    input  logic  clk,
+    input  reg8_t [0:3] in,
+    input  logic [1:0] ix,
+    output reg8_t out
+);
+    always_ff @(posedge clk) begin
+        out <= in[ix];
+    end
+endmodule
+
+module pcktest3 (
+    input  logic  clk,
+    input  reg2dim_t in,
+    input  logic [1:0] ix,
+    output reg8_t out
+);
+    always_ff @(posedge clk) begin
+        out <= in[ix];
+    end
+endmodule
+
+module pcktest4 (
+    input  logic  clk,
+    input  reg2dim1_t in,
+    input  logic [1:0] ix,
+    output reg8_t out
+);
+    always_ff @(posedge clk) begin
+        out <= in[ix];
+    end
+endmodule

tests/simple/memory.v

@@ -44,6 +44,7 @@ input [2:0] bit;
 output reg y1, y2;
 output y3, y4;
 
+(* nomem2reg *)
 reg [7:0] mem1 [3:0];
 
 (* mem2reg *)

tests/svtypes/enum_simple.ys

@@ -1,5 +1,5 @@
 
 read_verilog -sv enum_simple.sv
-hierarchy; proc; opt
+hierarchy; proc; opt; async2sync
 sat -verify -seq 1 -set-at 1 rst 1 -tempinduct -prove-asserts -show-all
 

tests/svtypes/multirange_array.sv

@@ -8,9 +8,21 @@ module top;
 	logic a [3];
 	logic b [3][5];
 	logic c [3][5][7];
+	logic [2:0] d;
+	logic [2:0][4:0] e;
+	logic [2:0][4:0][6:0] f;
+	logic [2:0] g [3];
+	logic [2:0][4:0] h [3][5];
+	logic [2:0][4:0][6:0] i [3][5][7];
 
 	`STATIC_ASSERT($bits(a) == 3);
 	`STATIC_ASSERT($bits(b) == 15);
 	`STATIC_ASSERT($bits(c) == 105);
+	`STATIC_ASSERT($bits(d) == 3);
+	`STATIC_ASSERT($bits(e) == 15);
+	`STATIC_ASSERT($bits(f) == 105);
+	`STATIC_ASSERT($bits(g) == 9);
+	`STATIC_ASSERT($bits(h) == 225);
+	`STATIC_ASSERT($bits(i) == 11025);
 
 endmodule

tests/svtypes/struct_array.sv

@@ -23,6 +23,29 @@ module top;
 	always_comb assert(s.b[23:16]===8'hxx);
 	always_comb assert(s.b[19:12]===8'hxf);
 
+	// Same as s, but defining dimensions in stages with typedef
+	typedef bit [7:0] bit8_t;
+	struct packed {
+		bit8_t [5:0] a;		// 6 element packed array of bytes
+		bit [15:0] b;		// filler for non-zero offset
+	} s_s;
+
+	initial begin
+		s_s = '0;
+
+		s_s.a[2:1] = 16'h1234;
+		s_s.a[5] = 8'h42;
+		s_s.a[-1] = '0;
+
+		s_s.b = '1;
+		s_s.b[1:0] = '0;
+	end
+
+	always_comb assert(s_s==64'h4200_0012_3400_FFFC);
+	always_comb assert(s_s.a[0][3:-4]===8'h0x);
+	always_comb assert(s_s.b[23:16]===8'hxx);
+	always_comb assert(s_s.b[19:12]===8'hxf);
+
 	struct packed {
 		bit [7:0] [7:0] a;	// 8 element packed array of bytes
 		bit [15:0] b;		// filler for non-zero offset
@@ -125,6 +148,28 @@ module top;
 
 	always_comb assert(s3_lbl==80'hFC00_4200_0012_3400_FFFC);
 
+	// Same as s3_lbl, but defining dimensions in stages with typedef
+	typedef bit [0:3] bit3l_t;
+	struct packed {
+		bit3l_t [0:7] [1:0] a;
+		bit [0:15] b;		// filler for non-zero offset
+	} s3_lbl_s;
+
+	initial begin
+		s3_lbl_s = '0;
+
+		s3_lbl_s.a[5:6] = 16'h1234;
+		s3_lbl_s.a[2] = 8'h42;
+
+		s3_lbl_s.a[0] = '1;
+		s3_lbl_s.a[0][0][2:3] = '0;
+
+		s3_lbl_s.b = '1;
+		s3_lbl_s.b[14:15] = '0;
+	end
+
+	always_comb assert(s3_lbl_s==80'hFC00_4200_0012_3400_FFFC);
+
 	struct packed {
 		bit [0:7] [0:1] [3:0] a;
 		bit [0:15] b;		// filler for non-zero offset

tests/svtypes/struct_dynamic_range.ys

@@ -4,4 +4,5 @@ select -assert-count 2 t:$shift
 select -assert-count 2 t:$shiftx
 prep -top top
 flatten
+async2sync
 sat -enable_undef -verify -prove-asserts

tests/svtypes/struct_sizebits.sv

@@ -25,6 +25,18 @@ struct packed {
 //wire [$bits({s.x, s.x})-1:0]xx_bits;
 
 always_comb begin
+	assert ($dimensions(s) == 1);
+	assert ($dimensions(s.x) == 1);
+`ifndef VERIFIC
+	assert ($dimensions(s.t) == 1);
+	assert ($dimensions({3{s.x}}) == 1);
+`endif
+	assert ($dimensions(s.sy.y) == 2);
+	assert ($dimensions(s.sy.y[2]) == 1);
+	assert ($dimensions(s.sz.z) == 3);
+	assert ($dimensions(s.sz.z[3]) == 2);
+	assert ($dimensions(s.sz.z[3][3]) == 1);
+
 	assert ($size(s) == $size(s.t) + $size(s.x) + $size(s.sy) + $size(s.sz));
 	assert ($size(s) == 1 + 4 + 6*4 + 6*8*4);
 
@@ -107,6 +119,19 @@ always_comb begin
 	assert ($right(s.sz.z[3]) == 9);
 	assert ($right(s.sz.z[3][3]) == 4);
 	assert ($right(s.sz.z[3], 2) == 4);
+
+	assert ($increment(s.x) == 1);
+	assert ($increment(s.sy.y) == -1);
+	assert ($increment(s.sy.y, 1) == -1);
+	assert ($increment(s.sy.y, (1+1)) == 1);
+
+	assert ($increment(s.sz.z) == 1);
+	assert ($increment(s.sz.z, 1) == 1);
+	assert ($increment(s.sz.z, 2) == -1);
+	assert ($increment(s.sz.z, 3) == -1);
+	assert ($increment(s.sz.z[3]) == -1);
+	assert ($increment(s.sz.z[3][3]) == -1);
+	assert ($increment(s.sz.z[3], 2) == -1);
 end
 
 endmodule

tests/svtypes/typedef_initial_and_assign.ys

@@ -9,6 +9,6 @@ logger -expect warning "reg '\\var_18' is assigned in a continuous assignment" 1
 logger -expect warning "reg '\\var_19' is assigned in a continuous assignment" 1
 
 read_verilog -sv typedef_initial_and_assign.sv
-hierarchy; proc; opt
+hierarchy; proc; opt; async2sync
 select -module top
-sat -verify -seq 1 -tempinduct -prove-asserts -show-all
+sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/svtypes/typedef_struct_port.ys

@@ -1,5 +1,5 @@
 read_verilog -sv typedef_struct_port.sv
-hierarchy; proc; opt
+hierarchy; proc; opt; async2sync
 select -module top
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all
 select -module test_parser

tests/various/bug4082.ys

@@ -0,0 +1,8 @@
+read_verilog <<EOF
+module top;
+  wire a;
+  wire b;
+  assign a = b;
+endmodule
+EOF
+delete w:a

tests/various/chformal_check.ys

@@ -0,0 +1,68 @@
+read_verilog -formal <<EOT
+
+module top(input clk, a, en);
+    wire a_q = '0;
+    wire en_q = '0;
+
+    always @(posedge clk) begin
+        a_q <= a;
+        en_q <= en;
+    end
+
+    always @(posedge clk)
+        if (en_q)
+            assert(a_q);
+endmodule
+EOT
+
+prep
+
+design -save prep
+
+select -assert-count 1 t:$check r:FLAVOR=assert %i
+
+chformal -assert2assume
+
+select -assert-count 1 t:$check r:FLAVOR=assume %i
+
+chformal -assume2assert
+
+select -assert-count 1 t:$check r:FLAVOR=assert %i
+
+async2sync
+
+chformal -lower
+select -assert-count 1 t:$assert
+
+design -load prep
+
+chformal -assert2assume
+async2sync
+chformal -lower
+chformal -assume -early
+
+rename -enumerate -pattern assume_% t:$assume
+expose -evert t:$assume
+
+design -save gold
+
+design -load prep
+
+chformal -assert2assume
+chformal -assume -early
+async2sync
+chformal -lower
+
+rename -enumerate -pattern assume_% t:$assume
+expose -evert t:$assume
+
+design -save gate
+
+design -reset
+
+design -copy-from gold -as gold top
+design -copy-from gate -as gate top
+
+miter -equiv -flatten -make_assert gold gate miter
+
+sat -verify -prove-asserts -tempinduct miter

tests/various/chformal_coverenable.ys

@@ -2,10 +2,10 @@ read_verilog -formal <<EOT
 module top(input a, b, c, d);
 
     always @* begin
-        if (a) assert (b == c);
-        if (!a) assert (b != c);
-        if (b) assume (c);
-        if (c) cover (d);
+        if (a) c0: assert (b == c);
+        if (!a) c1: assert (b != c);
+        if (b) c2: assume (c);
+        if (c) c3: cover (d);
     end
 
 endmodule
@@ -13,6 +13,10 @@ EOT
 
 prep -top top
 
+design -save prep
+
+async2sync
+
 select -assert-count 1 t:$cover
 
 chformal -cover -coverenable
@@ -23,3 +27,36 @@ select -assert-count 4 t:$cover
 
 chformal -assume -coverenable
 select -assert-count 5 t:$cover
+
+autoname */t:$cover
+expose -evert */c? */c?_EN_$cover_*
+
+design -save a2s_first
+
+design -load prep
+select -assert-count 1 r:FLAVOR=cover
+
+chformal -cover -coverenable
+select -assert-count 2 r:FLAVOR=cover
+
+chformal -assert -coverenable
+select -assert-count 4 r:FLAVOR=cover
+
+chformal -assume -coverenable
+select -assert-count 5 r:FLAVOR=cover
+
+async2sync
+
+autoname */t:$cover
+expose -evert */c? */c?_EN_$cover_*
+
+design -save a2s_last
+
+design -reset
+
+design -copy-from a2s_first -as gold top
+design -copy-from a2s_last -as gate top
+
+miter -equiv -flatten -make_assert gold gate miter
+
+sat -verify -prove-asserts -tempinduct miter

tests/various/chparam.sh

@@ -37,14 +37,17 @@ EOT
 
 if ../../yosys -q -p 'verific -sv chparam1.sv'; then
 	../../yosys -q -p 'verific -sv chparam1.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
+			-p 'async2sync' \
 			-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
 			-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
 
 	../../yosys -q -p 'verific -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
+			-p 'async2sync' \
 			-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
 			-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
 fi
 ../../yosys -q -p 'read_verilog -sv chparam2.sv; hierarchy -chparam X 123123123 -top top; prep -flatten' \
+		-p 'async2sync' \
 		-p 'sat -verify -prove-asserts -show-ports -set din[0] 1' \
 		-p 'sat -falsify -prove-asserts -show-ports -set din[0] 0'
 

tests/various/clk2fflogic_effects.sh

@@ -0,0 +1,35 @@
+#!/usr/bin/env bash
+set -e
+
+# TODO: when sim gets native $check support, remove the -DNO_ASSERT here
+echo Running yosys sim
+../../yosys -q -p "
+read_verilog -formal -DNO_ASSERT clk2fflogic_effects.sv
+hierarchy -top top; proc;;
+
+tee -q -o clk2fflogic_effects.sim.log sim -q -n 32
+"
+echo Running yosys clk2fflogic sim
+../../yosys -q -p "
+read_verilog -formal clk2fflogic_effects.sv
+hierarchy -top top; proc;;
+clk2fflogic;;
+
+logger -nowarn ^Assertion
+tee -q -o clk2fflogic_effects.clk2fflogic.log sim -q -n 32
+"
+
+echo Running iverilog sim
+iverilog -g2012 -DNO_ASSERT -o clk2fflogic_effects.iv.out clk2fflogic_effects.sv
+
+
+./clk2fflogic_effects.iv.out > clk2fflogic_effects.iv.log
+
+gawk '/([0-9]+):/{T=$1;print};/^Failed/{print T,$0}' clk2fflogic_effects.iv.log | sort > clk2fflogic_effects.iv.sorted.log
+gawk '/([0-9]+):/{T=$1;print};/^Failed/{print T,$0}' clk2fflogic_effects.sim.log | sort > clk2fflogic_effects.sim.sorted.log
+gawk '/([0-9]+):/{T=$1;print};/^Failed/{print T,$0}' clk2fflogic_effects.clk2fflogic.log | sort > clk2fflogic_effects.clk2fflogic.sorted.log
+
+echo Comparing iverilog sim vs yosys sim
+cmp clk2fflogic_effects.iv.sorted.log clk2fflogic_effects.sim.sorted.log
+echo Comparing iverilog sim vs yosys clk2fflogic sim
+cmp clk2fflogic_effects.iv.sorted.log clk2fflogic_effects.clk2fflogic.sorted.log

tests/various/clk2fflogic_effects.sv

@@ -0,0 +1,101 @@
+module top;
+
+(* gclk *)
+reg gclk;
+
+reg clk = 0;
+always @(posedge gclk)
+    clk <= !clk;
+
+reg [5:0] counter = 0;
+
+reg eff_0_trg = '0;
+reg eff_0_en = '0;
+
+reg eff_1_trgA = '0;
+reg eff_1_trgB = '0;
+reg eff_1_en = '0;
+
+reg eff_2_trgA = '0;
+reg eff_2_trgB = '0;
+reg eff_2_en = '0;
+
+reg eff_3_trg = '0;
+reg eff_3_en = '0;
+reg eff_3_a = '0;
+
+`ifdef FAST
+always @(posedge gclk) begin
+`else
+always @(posedge clk) begin
+`endif
+    counter <= counter + 1;
+
+    eff_0_trg = 32'b00000000000000110011001100101010 >> counter;
+    eff_0_en <= 32'b00000000000001100000110110110110 >> counter;
+
+    eff_1_trgA = 32'b00000000000000000011110000011110 >> counter;
+    eff_1_trgB = 32'b00000000000000001111000001111000 >> counter;
+    eff_1_en  <= 32'b00000000000000001010101010101010 >> counter;
+
+    eff_2_trgA = counter[0];
+    eff_2_trgB = !counter[0];
+    eff_2_en  <= 32'b00000000000000000000001111111100 >> counter;
+
+    eff_3_trg  = 32'b10101010101010101010101010101010 >> counter;
+    eff_3_en  <= 32'b11101110010001001110111001000100 >> counter;
+    eff_3_a   <= 32'b11111010111110100101000001010000 >> counter;
+end
+
+always @(posedge eff_0_trg)
+    if (eff_0_en)
+        $display("%02d: eff0 +", counter);
+
+always @(negedge eff_0_trg)
+    if (eff_0_en)
+        $display("%02d: eff0 -", counter);
+
+always @(posedge eff_0_trg, negedge eff_0_trg)
+    if (eff_0_en)
+        $display("%02d: eff0 *", counter);
+
+always @(posedge eff_1_trgA, posedge eff_1_trgB)
+    if (eff_1_en)
+        $display("%02d: eff1 ++", counter);
+
+always @(posedge eff_1_trgA, negedge eff_1_trgB)
+    if (eff_1_en)
+        $display("%02d: eff1 +-", counter);
+
+always @(negedge eff_1_trgA, posedge eff_1_trgB)
+    if (eff_1_en)
+        $display("%02d: eff1 -+", counter);
+
+always @(negedge eff_1_trgA, negedge eff_1_trgB)
+    if (eff_1_en)
+        $display("%02d: eff1 --", counter);
+
+always @(posedge eff_2_trgA, posedge eff_2_trgB)
+    if (eff_2_en)
+        $display("repeated");
+
+always @(posedge eff_3_trg)
+    if (eff_3_en) begin
+        $display("%02d: eff3 vvv", counter);
+`ifdef NO_ASSERT
+        if (!eff_3_a)
+            $display("Failed assertion eff3 at");
+`else
+        eff3: assert(eff_3_a);
+`endif
+    end
+
+`ifdef __ICARUS__
+initial gclk = 0;
+always @(gclk) gclk <= #5 !gclk;
+always @(posedge gclk)
+    if (counter == 32)
+        $finish(0);
+`endif
+
+endmodule

tests/various/const_arg_loop.ys

@@ -3,4 +3,5 @@ hierarchy
 proc
 opt -full
 select -module top
+async2sync
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/various/const_func.ys

@@ -4,4 +4,5 @@ proc
 flatten
 opt -full
 select -module top
+async2sync
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/various/countbits.ys

@@ -4,4 +4,5 @@ proc
 flatten
 opt -full
 select -module top
+async2sync
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/various/param_struct.ys

@@ -47,4 +47,5 @@ end
 endmodule
 EOF
 hierarchy; proc; opt
+async2sync
 sat -verify -seq 1 -tempinduct -prove-asserts -show-all

tests/various/scopeinfo.ys

@@ -0,0 +1,110 @@
+read_verilog <<EOT
+(* module_attr = "module_attr" *)
+module some_mod(input a, output y);
+    assign y = a;
+endmodule
+
+module top(input a, output y);
+    (* inst_attr = "inst_attr" *)
+    some_mod some_inst(.a(a), .y(y));
+endmodule
+EOT
+
+hierarchy -top top
+flatten
+
+select -assert-count 1 top/n:some_inst top/t:$scopeinfo %i
+select -assert-count 1 top/n:some_inst top/r:TYPE=module %i
+select -assert-count 1 top/n:some_inst top/a:cell_inst_attr=inst_attr %i
+select -assert-count 1 top/n:some_inst top/a:module_module_attr=module_attr %i
+select -assert-count 1 top/n:some_inst top/a:cell_src %i
+select -assert-count 1 top/n:some_inst top/a:module_src %i
+
+opt_clean
+select -assert-count 1 top/t:$scopeinfo
+opt_clean -purge
+select -assert-count 0 top/t:$scopeinfo
+
+design -reset
+
+read_verilog <<EOT
+(* module_attr = "module_attr_deep" *)
+module some_mod_deep(input a, output y);
+    assign y = a;
+endmodule
+
+(* module_attr = "module_attr" *)
+module some_mod(input a, output y);
+    (* inst_attr = "inst_attr_deep" *)
+    some_mod_deep some_inst_deep(.a(a), .y(y));
+endmodule
+
+module top(input a, output y);
+    (* inst_attr = "inst_attr" *)
+    some_mod some_inst(.a(a), .y(y));
+endmodule
+EOT
+
+hierarchy -top top
+flatten
+
+select -assert-count 2 top/t:$scopeinfo
+select -assert-count 1 top/n:some_inst top/t:$scopeinfo %i
+select -assert-count 1 top/a:hdlname=some_inst?some_inst_deep
+
+select -assert-count 1 top/n:some_inst top/r:TYPE=module %i
+select -assert-count 1 top/n:some_inst top/a:cell_inst_attr=inst_attr %i
+select -assert-count 1 top/n:some_inst top/a:module_module_attr=module_attr %i
+select -assert-count 1 top/n:some_inst top/a:cell_src %i
+select -assert-count 1 top/n:some_inst top/a:module_src %i
+
+select -assert-count 1 top/a:hdlname=some_inst?some_inst_deep top/r:TYPE=module %i
+select -assert-count 1 top/a:hdlname=some_inst?some_inst_deep top/a:cell_inst_attr=inst_attr_deep %i
+select -assert-count 1 top/a:hdlname=some_inst?some_inst_deep top/a:module_module_attr=module_attr_deep %i
+select -assert-count 1 top/a:hdlname=some_inst?some_inst_deep top/a:cell_src %i
+select -assert-count 1 top/a:hdlname=some_inst?some_inst_deep top/a:module_src %i
+
+
+design -reset
+
+read_verilog <<EOT
+(* module_attr = "module_attr_deep" *)
+(* keep_hierarchy *)
+module some_mod_deep(input a, output y);
+    assign y = a;
+endmodule
+
+(* module_attr = "module_attr" *)
+module some_mod(input a, output y);
+    (* inst_attr = "inst_attr_deep" *)
+    some_mod_deep some_inst_deep(.a(a), .y(y));
+endmodule
+
+module top(input a, output y);
+    (* inst_attr = "inst_attr" *)
+    some_mod some_inst(.a(a), .y(y));
+endmodule
+EOT
+
+hierarchy -top top
+flatten top
+
+select -assert-count 1 top/t:$scopeinfo
+setattr -mod -unset keep_hierarchy *
+flatten
+
+select -assert-count 2 top/t:$scopeinfo
+select -assert-count 1 top/n:some_inst top/t:$scopeinfo %i
+select -assert-count 1 top/a:hdlname=some_inst?some_inst_deep
+
+select -assert-count 1 top/n:some_inst top/r:TYPE=module %i
+select -assert-count 1 top/n:some_inst top/a:cell_inst_attr=inst_attr %i
+select -assert-count 1 top/n:some_inst top/a:module_module_attr=module_attr %i
+select -assert-count 1 top/n:some_inst top/a:cell_src %i
+select -assert-count 1 top/n:some_inst top/a:module_src %i
+
+select -assert-count 1 top/a:hdlname=some_inst?some_inst_deep top/r:TYPE=module %i
+select -assert-count 1 top/a:hdlname=some_inst?some_inst_deep top/a:cell_inst_attr=inst_attr_deep %i
+select -assert-count 1 top/a:hdlname=some_inst?some_inst_deep top/a:module_module_attr=module_attr_deep %i
+select -assert-count 1 top/a:hdlname=some_inst?some_inst_deep top/a:cell_src %i
+select -assert-count 1 top/a:hdlname=some_inst?some_inst_deep top/a:module_src %i