Squashed 'yosys/' changes from f7a8284c7b..f3c6b41050

f3c6b41050 Release version 0.31
25d4b3a5dc Bump version
2be5c0786f Merge pull request #3826 from nakengelhardt/nak/mem_libmap_print_attr
57de249881 memory_libmap: print additional debug messages when no valid mapping is found
14d50a176d Merge pull request #3676 from nakengelhardt/dfflegalize_scratchpad_minarg
a6be7b4751 memory_libmap: add debug messages for some reasons for rejecting mappings
b5b0b7e839 Bump version
7542146fc5 memory_libmap: print message about attributes forcing ram kind
eb397592f0 cxxrtl: add `$divfloor`.
911a76affa Merge pull request #3825 from jix/abc-fold-s
a7bccdfe8d Update ABC version
596da3f2a6 Merge pull request #3815 from charlottia/py312-syntax
6be5f6449c Merge pull request #3816 from jix/smtbmc-cover-keepgoing
b87af9cec0 Merge pull request #3817 from jix/constant_drive_conflict
2310a0ea9a Bump version
9ba7170919 Merge pull request #3818 from nakengelhardt/nak/verific_import_mem_access_src_loc
21686f0d9d verific: import src attribute on $memrd/$memwr cells
a07f8ac38a check: Also check for conflicts with constant drivers
f9744fdfcd smtbmc: Make cover mode respect --keep-going
3f29bdbbc5 smt2: py3.12+: avoid SyntaxWarning.
f9257d3192 Merge pull request #3811 from YosysHQ/micko/defaultvalue
8f7a9a0b66 Bump version
51e627686a Merge pull request #3812 from charlottia/iterator-invalidation
aff0065646 Use defaultvalue for init values of input ports
63e4114233 proc_prune: avoid using invalidated iterator
941fa70ce1 Merge pull request #3809 from YosysHQ/nak/show_escape
f573aebdd3 Merge pull request #3810 from charlottia/docs-celllib-minor
0c0171bd60 docs: RD_DATA is an output, not input
104edb4587 Bump version
48cafd5ccf Merge pull request #1489 from YosysHQ/clifford/ediflsbidx
9c7f0e7670 show: truncate very long module names
22c9237716 show: escape angle brackets
cff3195caa Improve EDIF lib_cell_ports scan
fb9e12761b Add "write_edif -lsbidx"
25954715f0 Bump version
d3ee4eba5b Merge pull request #3797 from charlottia/one-length-memories
3fa83ca195 Merge pull request #3808 from YosysHQ/krys/docs
d1b86d2fcf docs: reflow memory map
c9d31c3c87 smt2: abits needs to be at least 1 for BitVec
8b2a001021 Bump version
06f06c7be2 Merge pull request #3801 from jix/witness-aiw2yw-xbits
a310bd2d23 Merge pull request #3802 from YosysHQ/micko/build_full
8b74e8ad3a Merge pull request #3796 from YosysHQ/micko/update_abc
34a6bef768 link verific where appropriate and link full archives
75cf79588e Add ability for user plugin to add new verific log callback
dcc4d6e90b yosys-witness: Don't treat aiw x-bits as don't change
236e15f3b0 Merge pull request #3783 from YosysHQ/krys/docs
bac4c55ed6 Merge pull request #3723 from povik/pygen-const
e6f7cf3b29 Update tests
5813809ad9 Bump version
0d4a670267 Update ABC
b623888f6a Update ABC to latest
c5e4eec3ba Next dev cycle
3aee765793 Initial version of memory mapping doc
bd06338172 py_wrap_generator: Fix handling of method name collisions
f94f544b50 Fix the python generator for a bunch of const cases
b562b54c14 dfflegalize: allow setting mince and minsrst args from scratchpad

git-subtree-dir: yosys
git-subtree-split: f3c6b41050f388634a1e781e0734675dfc5fa505

Author: poname

CHANGELOG

@@ -2,6 +2,15 @@
 List of major changes and improvements between releases
 =======================================================
 
+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

Makefile

@@ -141,7 +141,7 @@ LDLIBS += -lrt
 endif
 endif
 
-YOSYS_VER := 0.30
+YOSYS_VER := 0.31
 
 # Note: We arrange for .gitcommit to contain the (short) commit hash in
 # tarballs generated with git-archive(1) using .gitattributes. The git repo
@@ -157,15 +157,15 @@ endif
 OBJS = kernel/version_$(GIT_REV).o
 
 bumpversion:
-#	sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 9c5a60e.. | wc -l`/;" Makefile
+#	sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline f7a8284.. | 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 = 2c1c83f
+ABCREV = bb64142
 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
 
@@ -740,13 +741,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

backends/cxxrtl/cxxrtl.h

@@ -1595,6 +1595,25 @@ value<BitsY> modfloor_ss(const value<BitsA> &a, const value<BitsB> &b) {
 	return r;
 }
 
+template<size_t BitsY, size_t BitsA, size_t BitsB>
+CXXRTL_ALWAYS_INLINE
+value<BitsY> divfloor_uu(const value<BitsA> &a, const value<BitsB> &b) {
+	return divmod_uu<BitsY>(a, b).first;
+}
+
+// Divfloor. Similar to above: returns q=a//b, where q has the sign of a*b and a=b*q+N.
+// In other words, returns (truncating) a/b, except if a and b have different signs
+// and there's non-zero remainder, subtract one more towards floor.
+template<size_t BitsY, size_t BitsA, size_t BitsB>
+CXXRTL_ALWAYS_INLINE
+value<BitsY> divfloor_ss(const value<BitsA> &a, const value<BitsB> &b) {
+	value<BitsY> q, r;
+	std::tie(q, r) = divmod_ss<BitsY>(a, b);
+	if ((b.is_neg() != a.is_neg()) && !r.is_zero())
+		return sub_uu<BitsY>(q, value<1> { 1u });
+	return q;
+
+}
 
 // Memory helper
 struct memory_index {

backends/cxxrtl/cxxrtl_backend.cc

@@ -185,7 +185,7 @@ bool is_binary_cell(RTLIL::IdString type)
 		ID($and), ID($or), ID($xor), ID($xnor), ID($logic_and), ID($logic_or),
 		ID($shl), ID($sshl), ID($shr), ID($sshr), ID($shift), ID($shiftx),
 		ID($eq), ID($ne), ID($eqx), ID($nex), ID($gt), ID($ge), ID($lt), ID($le),
-		ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($modfloor));
+		ID($add), ID($sub), ID($mul), ID($div), ID($mod), ID($modfloor), ID($divfloor));
 }
 
 bool is_extending_cell(RTLIL::IdString type)

backends/edif/edif.cc

@@ -120,6 +120,9 @@ struct EdifBackend : public Backend {
 		log("        sets the delimiting character for module port rename clauses to\n");
 		log("        parentheses, square brackets, or angle brackets.\n");
 		log("\n");
+		log("    -lsbidx\n");
+		log("        use index 0 for the LSB bit of a net or port instead of MSB.\n");
+		log("\n");
 		log("Unfortunately there are different \"flavors\" of the EDIF file format. This\n");
 		log("command generates EDIF files for the Xilinx place&route tools. It might be\n");
 		log("necessary to make small modifications to this command when a different tool\n");
@@ -132,6 +135,7 @@ struct EdifBackend : public Backend {
 		std::string top_module_name;
 		bool port_rename = false;
 		bool attr_properties = false;
+		bool lsbidx = false;
 		std::map<RTLIL::IdString, std::map<RTLIL::IdString, int>> lib_cell_ports;
 		bool nogndvcc = false, gndvccy = false, keepmode = false;
 		CellTypes ct(design);
@@ -173,6 +177,10 @@ struct EdifBackend : public Backend {
 				}
 				continue;
 			}
+			if (args[argidx] == "-lsbidx") {
+				lsbidx = true;
+				continue;
+			}
 			break;
 		}
 		extra_args(f, filename, args, argidx);
@@ -184,6 +192,14 @@ struct EdifBackend : public Backend {
 
 		for (auto module : design->modules())
 		{
+			lib_cell_ports[module->name];
+
+			for (auto port : module->ports)
+			{
+				Wire *wire = module->wire(port);
+				lib_cell_ports[module->name][port] = std::max(lib_cell_ports[module->name][port], GetSize(wire));
+			}
+
 			if (module->get_blackbox_attribute())
 				continue;
 
@@ -200,7 +216,7 @@ struct EdifBackend : public Backend {
 				if (design->module(cell->type) == nullptr || design->module(cell->type)->get_blackbox_attribute()) {
 					lib_cell_ports[cell->type];
 					for (auto p : cell->connections())
-						lib_cell_ports[cell->type][p.first] = GetSize(p.second);
+						lib_cell_ports[cell->type][p.first] = std::max(lib_cell_ports[cell->type][p.first], GetSize(p.second));
 				}
 			}
 		}
@@ -437,7 +453,7 @@ struct EdifBackend : public Backend {
 					*f << ")\n";
 					for (int i = 0; i < wire->width; i++) {
 						RTLIL::SigSpec sig = sigmap(RTLIL::SigSpec(wire, i));
-						net_join_db[sig].insert(make_pair(stringf("(portRef (member %s %d))", EDIF_REF(wire->name), GetSize(wire)-i-1), wire->port_input));
+						net_join_db[sig].insert(make_pair(stringf("(portRef (member %s %d))", EDIF_REF(wire->name), lsbidx ? i : GetSize(wire)-i-1), wire->port_input));
 					}
 				}
 			}
@@ -468,13 +484,13 @@ struct EdifBackend : public Backend {
 							log_warning("Bit %d of cell port %s.%s.%s driven by %s will be left unconnected in EDIF output.\n",
 									i, log_id(module), log_id(cell), log_id(p.first), log_signal(sig[i]));
 						else {
-							int member_idx = GetSize(sig)-i-1;
+							int member_idx = lsbidx ? i : GetSize(sig)-i-1;
 							auto m = design->module(cell->type);
 							int width = sig.size();
 							if (m) {
 								auto w = m->wire(p.first);
 								if (w) {
-									member_idx = GetSize(w)-i-1;
+									member_idx = lsbidx ? i : GetSize(w)-i-1;
 									width = GetSize(w);
 								}
 							}

backends/smt2/smt2.cc

@@ -773,7 +773,7 @@ struct Smt2Worker
 			int arrayid = idcounter++;
 			memarrays[mem] = arrayid;
 
-			int abits = ceil_log2(mem->size);
+			int abits = max(1, ceil_log2(mem->size));
 
 			bool has_sync_wr = false;
 			bool has_async_wr = false;
@@ -1220,7 +1220,7 @@ struct Smt2Worker
 			{
 				int arrayid = memarrays.at(mem);
 
-				int abits = ceil_log2(mem->size);;
+				int abits = max(1, ceil_log2(mem->size));
 
 				bool has_sync_wr = false;
 				bool has_async_wr = false;

backends/smt2/smtbmc.py

@@ -174,6 +174,8 @@ def help():
         further failed assertions. To output multiple traces
         covering all found failed assertions, the character '%' is
         replaced in all dump filenames with an increasing number.
+        In cover mode, don't stop when a cover trace contains a failed
+        assertion.
 
     --check-witness
         check that the used witness file contains sufficient
@@ -1739,7 +1741,7 @@ def smt_check_sat(expected=["sat", "unsat"]):
             smt_pop()
             smt.write("(define-fun covers_%d ((state |%s_s|)) (_ BitVec %d) (bvand (covers_%d state) #b%s))" % (coveridx, topmod, len(cover_desc), coveridx-1, cover_mask))
 
-        if found_failed_assert:
+        if found_failed_assert and not keep_going:
             break
 
         if "1" not in cover_mask:

backends/smt2/smtio.py

@@ -768,7 +768,7 @@ def check_sat(self, expected=["sat", "unsat", "unknown", "timeout", "interrupted
 
             if self.timeinfo:
                 i = 0
-                s = "/-\|"
+                s = r"/-\|"
 
                 count = 0
                 num_bs = 0
@@ -1171,7 +1171,7 @@ def set_net(self, path, bits):
 
     def escape_name(self, name):
         name = re.sub(r"\[([0-9a-zA-Z_]*[a-zA-Z_][0-9a-zA-Z_]*)\]", r"<\1>", name)
-        if re.match("[\[\]]", name) and name[0] != "\\":
+        if re.match(r"[\[\]]", name) and name[0] != "\\":
             name = "\\" + name
         return name
 

backends/smt2/witness.py

@@ -194,7 +194,7 @@ def aiw2yw(input, mapfile, output):
 
         values = WitnessValues()
         for i, v in enumerate(inline):
-            if v == "x" or outyw.t > 0 and i in aiger_map.init_inputs:
+            if outyw.t > 0 and i in aiger_map.init_inputs:
                 continue
 
             try:

docs/source/CHAPTER_CellLib.rst

@@ -571,7 +571,7 @@ The ``$mem_v2`` cell has the following ports:
 	signals for the read ports.
 
 ``\RD_DATA``
-	This input is ``\RD_PORTS*\WIDTH`` bits wide, containing all data
+	This output is ``\RD_PORTS*\WIDTH`` bits wide, containing all data
 	signals for the read ports.
 
 ``\RD_ARST``