Merge branch 'The-OpenROAD-Project:master' into master

CHANGELOG

@@ -2,9 +2,95 @@
 List of major changes and improvements between releases
 =======================================================
 
-Yosys 0.26 .. Yosys 0.26-dev
+Yosys 0.33 .. Yosys 0.34-dev
 --------------------------
 
+Yosys 0.32 .. Yosys 0.33
+--------------------------
+ * Various
+    - Added "$print" cell, produced by "$display" and "$write"
+      Verilog tasks.
+    - Added "$print" cell handling in CXXRTL.
+
+ * Lattice FPGA support
+    - Added generic "synth_lattice" pass (for now MachXO2/XO3/XO3D)
+    - Removed "synth_machxo2" pass
+    - Pass "ecp5_gsr" renamed to "lattice_gsr"
+    - "synth_machxo2" equivalent is "synth_lattice -family xo2"
+
+Yosys 0.31 .. Yosys 0.32
+--------------------------
+ * Verific support
+    - Added sub option "-lib" to reading commands for VHDL and
+      SystemVerilog, that will later import all units/modules from
+      marked files as blackboxes.
+
+ * Various
+    - Added support for $lt, $le, $gt, $ge to the code generating AIGs.
+
+Yosys 0.30 .. Yosys 0.31
+--------------------------
+ * New commands and options
+    - Added option "-lsbidx" to "write_edif" pass.
+
+ * Various
+    - Added support for $divfloor operator to cxxrtl backend.
+    - dfflegalize: allow setting mince and minsrst args from scratchpad.
+
+Yosys 0.29 .. Yosys 0.30
+--------------------------
+ * New commands and options
+    - Added "recover_names" pass to recover names post-mapping.
+
+ * Gowin support
+    - Added remaining primitives blackboxes.
+
+ * Various
+    - "show -colorattr" will now color the cells, wires, and 
+      connection arrows.
+    - "show -viewer none" will not execute viewer.
+
+Yosys 0.28 .. Yosys 0.29
+--------------------------
+ * New commands and options
+    - Added "synthprop" pass for synthesizable properties.
+
+ * Verific support
+    - Handle conditions on clocked concurrent assertions in unclocked
+      procedural contexts.
+
+ * Verilog
+    - Fix const eval of unbased unsized constants.
+    - Handling of attributes for struct / union variables.
+
+Yosys 0.27 .. Yosys 0.28
+--------------------------
+ * Verilog
+    - Out of bounds checking for struct/union members.
+
+ * Verific support
+    - Fix enum_values support and signed attribute values.
+
+ * ECP5 support
+    - Added "synth_ecp5 -iopad"
+
+ * MachXO2 support
+    - Added "synth_machxo2 -ccu2"
+
+Yosys 0.26 .. Yosys 0.27
+--------------------------
+ * New commands and options
+    - Added option "-make_assert" to "equiv_make" pass.
+    - Added option "-coverenable" to "chformal" pass.
+
+ * Verilog
+    - Resolve package types in interfaces.
+    - Handle range offsets in packed arrays within packed structs.
+    - Support for data and array queries on struct/union item expressions.
+
+ * GateMate support
+    - Enable register initialization.
+
 Yosys 0.25 .. Yosys 0.26
 --------------------------
  * New commands and options

Makefile

@@ -141,31 +141,31 @@ LDLIBS += -lrt
 endif
 endif
 
-YOSYS_VER := 0.26+34
+YOSYS_VER := 0.33+34
 
 # Note: We arrange for .gitcommit to contain the (short) commit hash in
 # tarballs generated with git-archive(1) using .gitattributes. The git repo
 # will have this file in its unexpanded form tough, in which case we fall
 # back to calling git directly.
 TARBALL_GIT_REV := $(shell cat $(YOSYS_SRC)/.gitcommit)
 ifeq ($(TARBALL_GIT_REV),$$Format:%h$$)
-GIT_REV := $(shell git ls-remote $(YOSYS_SRC) HEAD -q | $(AWK) 'BEGIN {R = "UNKNOWN"}; ($$2 == "HEAD") {R = substr($$1, 1, 9); exit} END {print R}')
+GIT_REV := $(shell GIT_DIR=$(YOSYS_SRC)/.git git rev-parse --short=9 HEAD || echo UNKNOWN)
 else
 GIT_REV := $(TARBALL_GIT_REV)
 endif
 
 OBJS = kernel/version_$(GIT_REV).o
 
 bumpversion:
-	sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 7e58866.. | wc -l`/;" Makefile
+	sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 2584903.. | wc -l`/;" Makefile
 
 # set 'ABCREV = default' to use abc/ as it is
 #
 # Note: If you do ABC development, make sure that 'abc' in this directory
 # is just a symlink to your actual ABC working directory, as 'make mrproper'
 # will remove the 'abc' directory and you do not want to accidentally
 # delete your work on ABC..
-ABCREV = a8f0ef2
+ABCREV = daad9ed
 ABCPULL = 1
 ABCURL ?= https://github.com/YosysHQ/abc
 ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q)
@@ -523,6 +523,7 @@ CXXFLAGS += -I$(GHDL_INCLUDE_DIR) -DYOSYS_ENABLE_GHDL
 LDLIBS += $(GHDL_LIB_DIR)/libghdl.a $(file <$(GHDL_LIB_DIR)/libghdl.link)
 endif
 
+LDLIBS_VERIFIC =
 ifeq ($(ENABLE_VERIFIC),1)
 VERIFIC_DIR ?= /usr/local/src/verific_lib
 VERIFIC_COMPONENTS ?= verilog database util containers hier_tree
@@ -548,9 +549,9 @@ CXXFLAGS += -DYOSYSHQ_VERIFIC_EXTENSIONS
 endif
 CXXFLAGS += $(patsubst %,-I$(VERIFIC_DIR)/%,$(VERIFIC_COMPONENTS)) -DYOSYS_ENABLE_VERIFIC
 ifeq ($(OS), Darwin)
-LDLIBS += $(patsubst %,$(VERIFIC_DIR)/%/*-mac.a,$(VERIFIC_COMPONENTS)) -lz
+LDLIBS_VERIFIC += $(foreach comp,$(patsubst %,$(VERIFIC_DIR)/%/*-mac.a,$(VERIFIC_COMPONENTS)),-Wl,-force_load $(comp)) -lz
 else
-LDLIBS += $(patsubst %,$(VERIFIC_DIR)/%/*-linux.a,$(VERIFIC_COMPONENTS)) -lz
+LDLIBS_VERIFIC += -Wl,--whole-archive $(patsubst %,$(VERIFIC_DIR)/%/*-linux.a,$(VERIFIC_COMPONENTS)) -Wl,--no-whole-archive -lz
 endif
 endif
 
@@ -611,6 +612,7 @@ $(eval $(call add_include_file,kernel/log.h))
 $(eval $(call add_include_file,kernel/rtlil.h))
 $(eval $(call add_include_file,kernel/binding.h))
 $(eval $(call add_include_file,kernel/register.h))
+$(eval $(call add_include_file,kernel/cellaigs.h))
 $(eval $(call add_include_file,kernel/celltypes.h))
 $(eval $(call add_include_file,kernel/celledges.h))
 $(eval $(call add_include_file,kernel/consteval.h))
@@ -627,6 +629,8 @@ ifeq ($(ENABLE_ZLIB),1)
 $(eval $(call add_include_file,kernel/fstdata.h))
 endif
 $(eval $(call add_include_file,kernel/mem.h))
+$(eval $(call add_include_file,kernel/yw.h))
+$(eval $(call add_include_file,kernel/json.h))
 $(eval $(call add_include_file,libs/ezsat/ezsat.h))
 $(eval $(call add_include_file,libs/ezsat/ezminisat.h))
 ifeq ($(ENABLE_ZLIB),1)
@@ -648,12 +652,7 @@ $(eval $(call add_include_file,backends/cxxrtl/cxxrtl_vcd_capi.h))
 
 OBJS += kernel/driver.o kernel/register.o kernel/rtlil.o kernel/log.o kernel/calc.o kernel/yosys.o
 OBJS += kernel/binding.o
-ifeq ($(ENABLE_ABC),1)
-ifneq ($(ABCEXTERNAL),)
-kernel/yosys.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"'
-endif
-endif
-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
+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
 ifeq ($(ENABLE_ZLIB),1)
 OBJS += kernel/fstdata.o
 endif
@@ -665,6 +664,11 @@ endif
 
 kernel/log.o: CXXFLAGS += -DYOSYS_SRC='"$(YOSYS_SRC)"'
 kernel/yosys.o: CXXFLAGS += -DYOSYS_DATDIR='"$(DATDIR)"' -DYOSYS_PROGRAM_PREFIX='"$(PROGRAM_PREFIX)"'
+ifeq ($(ENABLE_ABC),1)
+ifneq ($(ABCEXTERNAL),)
+kernel/yosys.o: CXXFLAGS += -DABCEXTERNAL='"$(ABCEXTERNAL)"'
+endif
+endif
 
 OBJS += libs/bigint/BigIntegerAlgorithms.o libs/bigint/BigInteger.o libs/bigint/BigIntegerUtils.o
 OBJS += libs/bigint/BigUnsigned.o libs/bigint/BigUnsignedInABase.o
@@ -740,13 +744,13 @@ yosys.js: $(filter-out yosysjs-$(YOSYS_VER).zip,$(EXTRA_TARGETS))
 endif
 
 $(PROGRAM_PREFIX)yosys$(EXE): $(OBJS)
-	$(P) $(LD) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LDFLAGS) $(LDFLAGS) $(OBJS) $(LDLIBS)
+	$(P) $(LD) -o $(PROGRAM_PREFIX)yosys$(EXE) $(EXE_LDFLAGS) $(LDFLAGS) $(OBJS) $(LDLIBS) $(LDLIBS_VERIFIC)
 
 libyosys.so: $(filter-out kernel/driver.o,$(OBJS))
 ifeq ($(OS), Darwin)
-	$(P) $(LD) -o libyosys.so -shared -Wl,-install_name,$(LIBDIR)/libyosys.so $(LDFLAGS) $^ $(LDLIBS)
+	$(P) $(LD) -o libyosys.so -shared -Wl,-install_name,$(LIBDIR)/libyosys.so $(LDFLAGS) $^ $(LDLIBS) $(LDLIBS_VERIFIC)
 else
-	$(P) $(LD) -o libyosys.so -shared -Wl,-soname,$(LIBDIR)/libyosys.so $(LDFLAGS) $^ $(LDLIBS)
+	$(P) $(LD) -o libyosys.so -shared -Wl,-soname,$(LIBDIR)/libyosys.so $(LDFLAGS) $^ $(LDLIBS) $(LDLIBS_VERIFIC)
 endif
 
 %.o: %.cc
@@ -797,13 +801,13 @@ ifneq ($(ABCREV),default)
 	$(Q) if test -d abc && test -d abc/.git && ! git -C abc diff-index --quiet HEAD; then \
 		echo 'REEBE: NOP pbagnvaf ybpny zbqvsvpngvbaf! Frg NOPERI=qrsnhyg va Lbflf Znxrsvyr!' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; false; \
 	fi
-	$(Q) if test -d abc && ! test -d abc/.git && ! test "`cat abc/.gitcommit | cut -c1-7`" == "$(ABCREV)"; then \
+	$(Q) if test -d abc && ! test -d abc/.git && ! test "`cat abc/.gitcommit | cut -c1-7`" = "$(ABCREV)"; then \
 		echo 'REEBE: Qbjaybnqrq NOP irefvbaf qbrf abg zngpu! Qbjaybnq sebz:' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; echo $(ABCURL)/archive/$(ABCREV).tar.gz; false; \
 	fi
 # set a variable so the test fails if git fails to run - when comparing outputs directly, empty string would match empty string
-	$(Q) if test -d abc && ! test -d abc/.git && test "`cat abc/.gitcommit | cut -c1-7`" == "$(ABCREV)"; then \
+	$(Q) if test -d abc && ! test -d abc/.git && test "`cat abc/.gitcommit | cut -c1-7`" = "$(ABCREV)"; then \
 		echo "Compiling local copy of ABC"; \
-	elif ! (cd abc 2> /dev/null && rev="`git rev-parse $(ABCREV)`" && test "`git rev-parse HEAD`" == "$$rev"); then \
+	elif ! (cd abc 2> /dev/null && rev="`git rev-parse $(ABCREV)`" && test "`git rev-parse HEAD`" = "$$rev"); then \
 		test $(ABCPULL) -ne 0 || { echo 'REEBE: NOP abg hc gb qngr naq NOPCHYY frg gb 0 va Znxrsvyr!' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; exit 1; }; \
 		echo "Pulling ABC from $(ABCURL):"; set -x; \
 		test -d abc || git clone $(ABCURL) abc; \
@@ -837,6 +841,9 @@ ABCOPT=""
 endif
 
 test: $(TARGETS) $(EXTRA_TARGETS)
+ifeq ($(ENABLE_VERIFIC),1)
+	+cd tests/verific && bash run-test.sh $(SEEDOPT)
+endif
 	+cd tests/simple && bash run-test.sh $(SEEDOPT)
 	+cd tests/simple_abc9 && bash run-test.sh $(SEEDOPT)
 	+cd tests/hana && bash run-test.sh $(SEEDOPT)
@@ -875,6 +882,7 @@ test: $(TARGETS) $(EXTRA_TARGETS)
 	+cd tests/memfile && bash run-test.sh
 	+cd tests/verilog && bash run-test.sh
 	+cd tests/xprop && bash run-test.sh $(SEEDOPT)
+	+cd tests/fmt && bash run-test.sh
 	@echo ""
 	@echo "  Passed \"make test\"."
 	@echo ""

README.md

@@ -156,9 +156,10 @@ reading and elaborating the design using the Verilog frontend:
 	yosys> read -sv tests/simple/fiedler-cooley.v
 	yosys> hierarchy -top up3down5
 
-writing the design to the console in Yosys's internal format:
+writing the design to the console in the RTLIL format used by Yosys
+internally:
 
-	yosys> write_ilang
+	yosys> write_rtlil
 
 convert processes (``always`` blocks) to netlist elements and perform
 some simple optimizations:

backends/aiger/aiger.cc

@@ -119,14 +119,14 @@ struct AigerWriter
 			if (wire->name.isPublic())
 				sigmap.add(wire);
 
-		// promote input wires
+		// promote output wires
 		for (auto wire : module->wires())
-			if (wire->port_input)
+			if (wire->port_output)
 				sigmap.add(wire);
 
-		// promote output wires
+		// promote input wires
 		for (auto wire : module->wires())
-			if (wire->port_output)
+			if (wire->port_input)
 				sigmap.add(wire);
 
 		for (auto wire : module->wires())
@@ -706,6 +706,9 @@ struct AigerWriter
 		for (auto &it : latch_lines)
 			f << it.second;
 
+		if (initstate_ff)
+			f << stringf("ninitff %d\n", ((initstate_ff >> 1)-1-aig_i));
+
 		wire_lines.sort();
 		for (auto &it : wire_lines)
 			f << it.second;
@@ -733,6 +736,9 @@ struct AigerWriter
 				auto sig_qy = cell->getPort(cell->type.in(ID($anyconst), ID($anyseq)) ? ID::Y : ID::Q);
 				SigSpec sig = sigmap(sig_qy);
 
+				if (cell->get_bool_attribute(ID(clk2fflogic)))
+					sig_qy = cell->getPort(ID::D); // For a clk2fflogic $_FF_ the named signal is the D input not the Q output
+
 				for (int i = 0; i < GetSize(sig_qy); i++) {
 					if (sig_qy[i].wire == nullptr || sig[i].wire == nullptr)
 						continue;

backends/aiger/xaiger.cc

@@ -274,14 +274,18 @@ struct XAigerWriter
 						continue;
 					auto offset = i.first.offset;
 
+					auto rhs = cell->getPort(i.first.name);
+					if (offset >= rhs.size())
+						continue;
+
 #ifndef NDEBUG
 					if (ys_debug(1)) {
 						static pool<std::pair<IdString,TimingInfo::NameBit>> seen;
 						if (seen.emplace(inst_module->name, i.first).second) log("%s.%s[%d] abc9_arrival = %d\n",
 								log_id(cell->type), log_id(i.first.name), offset, d);
 					}
 #endif
-					arrival_times[cell->getPort(i.first.name)[offset]] = d;
+					arrival_times[rhs[offset]] = d;
 				}
 
 				if (abc9_flop)

backends/blif/blif.cc

@@ -512,8 +512,8 @@ struct BlifBackend : public Backend {
 		log("        suppresses the generation of this nets without fanout.\n");
 		log("\n");
 		log("The following options can be useful when the generated file is not going to be\n");
-		log("read by a BLIF parser but a custom tool. It is recommended to not name the\n");
-		log("output file *.blif when any of this options is used.\n");
+		log("read by a BLIF parser but a custom tool. It is recommended not to name the\n");
+		log("output file *.blif when any of these options are used.\n");
 		log("\n");
 		log("    -icells\n");
 		log("        do not translate Yosys's internal gates to generic BLIF logic\n");

backends/btor/btor.cc

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