Merge branch 'YosysHQ:main' into master

.github/workflows/test-verific.yml

@@ -0,0 +1,77 @@
+name: Build and run tests with Verific (Linux)
+
+on: [push, pull_request]
+
+jobs:
+  test-verific:
+    runs-on: [self-hosted, linux, x64]
+    steps:
+      - name: Checkout Yosys
+        uses: actions/checkout@v4
+        with:
+          persist-credentials: false
+
+      - name: Runtime environment
+        run: |
+          echo "procs=$(nproc)" >> $GITHUB_ENV
+
+      - name: Build Yosys
+        run: |
+          make config-clang
+          echo "ENABLE_VERIFIC := 1" >> Makefile.conf
+          echo "ENABLE_VERIFIC_EDIF := 1" >> Makefile.conf
+          echo "ENABLE_VERIFIC_LIBERTY := 1" >> Makefile.conf
+          echo "ENABLE_CCACHE := 1" >> Makefile.conf
+          make -j${{ env.procs }}
+
+      - name: Install Yosys
+        run: |
+          make install DESTDIR=${GITHUB_WORKSPACE}/.local PREFIX=
+
+      - name: Checkout Documentation
+        if: ${{ github.ref == 'refs/heads/main' }}
+        uses: actions/checkout@v4
+        with:
+          path: 'yosys-cmd-ref'
+          repository: 'YosysHQ-Docs/yosys-cmd-ref'
+          fetch-depth: 0
+          token: ${{ secrets.CI_DOCS_UPDATE_PAT }}
+          persist-credentials: true
+
+      - name: Update documentation
+        if: ${{ github.ref == 'refs/heads/main' }}
+        run: |
+          make docs
+          rm -rf docs/build
+          cd yosys-cmd-ref
+          rm -rf *
+          git checkout README.md
+          cp -R ../docs/* .
+          rm -rf util/__pycache__
+          git add -A .
+          git diff-index --quiet HEAD || git commit -m "Update"
+          git push
+
+      - name: Checkout SBY
+        uses: actions/checkout@v4
+        with:
+          repository: 'YosysHQ/sby'
+          path: 'sby'
+
+      - name: Build SBY
+        run: |
+          make -C sby install DESTDIR=${GITHUB_WORKSPACE}/.local PREFIX=
+
+      - name: Run Yosys tests
+        run: |
+          make -j${{ env.procs }} test
+
+      - name: Run Verific specific Yosys tests
+        run: |
+          make -C tests/sva
+          cd tests/svtypes && bash run-test.sh
+
+      - name: Run SBY tests
+        if: ${{ github.ref == 'refs/heads/main' }}
+        run: |
+          make -C sby run_ci

Makefile

@@ -141,7 +141,7 @@ LIBS += -lrt
 endif
 endif
 
-YOSYS_VER := 0.40+7
+YOSYS_VER := 0.40+22
 
 # Note: We arrange for .gitcommit to contain the (short) commit hash in
 # tarballs generated with git-archive(1) using .gitattributes. The git repo
@@ -984,16 +984,27 @@ docs/gen_images:
 	$(Q) $(MAKE) -C docs images
 
 DOCS_GUIDELINE_FILES := GettingStarted CodingStyle
-docs/guidelines:
+docs/guidelines docs/source/generated:
-	$(Q) mkdir -p docs/source/temp
+	$(Q) mkdir -p docs/source/generated
-	$(Q) cp -f $(addprefix guidelines/,$(DOCS_GUIDELINE_FILES)) docs/source/temp
+	$(Q) cp -f $(addprefix guidelines/,$(DOCS_GUIDELINE_FILES)) docs/source/generated
 
-# many of these will return an error which can be safely ignored, so we prefix
+# some commands return an error and print the usage text to stderr
-# the command with a '-'
+define DOC_USAGE_STDERR
-DOCS_USAGE_PROGS := yosys yosys-config yosys-filterlib yosys-abc yosys-smtbmc yosys-witness
+docs/source/generated/$(1): $(PROGRAM_PREFIX)$(1) docs/source/generated
-docs/usage: $(addprefix docs/source/temp/,$(DOCS_USAGE_PROGS))
+	-$(Q) ./$$< --help 2> $$@
-docs/source/temp/%: docs/guidelines
+endef
-	-$(Q) ./$(PROGRAM_PREFIX)$* --help > $@ 2>&1
+DOCS_USAGE_STDERR := yosys-config yosys-filterlib yosys-abc
+$(foreach usage,$(DOCS_USAGE_STDERR),$(eval $(call DOC_USAGE_STDERR,$(usage))))
+
+# others print to stdout
+define DOC_USAGE_STDOUT
+docs/source/generated/$(1): $(PROGRAM_PREFIX)$(1) docs/source/generated
+	$(Q) ./$$< --help > $$@
+endef
+DOCS_USAGE_STDOUT := yosys yosys-smtbmc yosys-witness
+$(foreach usage,$(DOCS_USAGE_STDOUT),$(eval $(call DOC_USAGE_STDOUT,$(usage))))
+
+docs/usage: $(addprefix docs/source/generated/,$(DOCS_USAGE_STDOUT) $(DOCS_USAGE_STDERR))
 
 docs/reqs:
 	$(Q) $(MAKE) -C docs reqs

docs/.gitignore

@@ -1,6 +1,6 @@
 /build/
 /source/cmd
-/source/temp
+/source/generated
 /source/_images/**/*.log
 /source/_images/**/*.aux
 /source/_images/**/*.pdf

docs/Makefile

@@ -48,6 +48,7 @@ help:
 clean: clean-examples
 	rm -rf $(BUILDDIR)/*
 	rm -rf source/cmd util/__pycache__
+	rm -rf source/generated
 	$(MAKE) -C source/_images clean
 
 .PHONY: html

docs/source/appendix/auxprogs.rst

@@ -11,7 +11,7 @@ The ``yosys-config`` tool (an auto-generated shell-script) can be used to query
 compiler options and other information needed for building loadable modules for
 Yosys. See :doc:`/yosys_internals/extending_yosys/extensions` for details.
 
-.. literalinclude:: /temp/yosys-config
+.. literalinclude:: /generated/yosys-config
     :start-at: Usage
 
 .. _sec:filterlib:
@@ -25,7 +25,7 @@ The ``yosys-filterlib`` tool is a small utility that can be used to strip or
 extract information from a Liberty file.  This can be useful for removing
 sensitive or proprietary information such as timing or other trade secrets.
 
-.. literalinclude:: /temp/yosys-filterlib
+.. literalinclude:: /generated/yosys-filterlib
     :start-at: Usage
 
 yosys-abc
@@ -36,9 +36,8 @@ been accepted upstream. Not all versions of Yosys work with all versions of ABC.
 So Yosys comes with its own yosys-abc to avoid compatibility issues between the
 two.
 
-.. literalinclude:: /temp/yosys-abc
+.. literalinclude:: /generated/yosys-abc
     :start-at: usage
-    :end-before: UC Berkeley
 
 yosys-smtbmc
 ------------
@@ -46,7 +45,7 @@ yosys-smtbmc
 The ``yosys-smtbmc`` tool is a utility used by SBY for interacting with smt
 solvers.
 
-.. literalinclude:: /temp/yosys-smtbmc
+.. literalinclude:: /generated/yosys-smtbmc
 
 yosys-witness
 -------------
@@ -55,7 +54,7 @@ yosys-witness
 This is used in SBY and SCY for producing traces in a consistent format
 independent of the solver.
 
-.. literalinclude:: /temp/yosys-witness
+.. literalinclude:: /generated/yosys-witness
     :start-at: Usage
 
 .. note:: ``yosys-witness`` requires `click`_ Python package for use.

docs/source/cmd_ref.rst

@@ -4,7 +4,7 @@
 Command line reference
 ================================================================================
 
-.. literalinclude:: /temp/yosys
+.. literalinclude:: /generated/yosys
     :start-at: Usage
 
 .. toctree::

docs/source/code_examples/extensions/Makefile

@@ -13,18 +13,18 @@ my_cmd.so: my_cmd.cc
 	$(YOSYS)-config --exec --cxx $(subst $(DATDIR),../../../../share,$(CXXFLAGS)) --ldflags -o my_cmd.so -shared my_cmd.cc --ldlibs
 
 test0.log: my_cmd.so
-	$(YOSYS) -Ql test0.log_new -m ./my_cmd.so -p 'my_cmd foo bar' absval_ref.v
+	$(YOSYS) -QTl test0.log_new -m ./my_cmd.so -p 'my_cmd foo bar' -f verilog absval_ref.v
 	mv test0.log_new test0.log
 
 test1.log: my_cmd.so
-	$(YOSYS) -Ql test1.log_new -m ./my_cmd.so -p 'clean; test1; dump' absval_ref.v
+	$(YOSYS) -QTl test1.log_new -m ./my_cmd.so -p 'clean; test1; dump' -f verilog absval_ref.v
 	mv test1.log_new test1.log
 
 test1.dot: my_cmd.so
 	$(YOSYS) -m ./my_cmd.so -p 'test1; show -format dot -prefix test1'
 
 test2.log: my_cmd.so
-	$(YOSYS) -Ql test2.log_new -m ./my_cmd.so -p 'hierarchy -top test; test2' sigmap_test.v
+	$(YOSYS) -QTl test2.log_new -m ./my_cmd.so -p 'hierarchy -top test; test2' -f verilog sigmap_test.v
 	mv test2.log_new test2.log
 
 .PHONY: clean

frontends/verific/verific.cc

@@ -1432,6 +1432,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
 	}
 	import_attributes(module->attributes, nl, nl);
 	module->set_string_attribute(ID::hdlname, nl->CellBaseName());
+	module->set_string_attribute(ID(library), nl->Owner()->Owner()->Name());
 #ifdef VERIFIC_VHDL_SUPPORT
 	if (nl->IsFromVhdl()) {
 		NameSpace name_space(0);

passes/sat/formalff.cc

@@ -237,7 +237,7 @@ struct InitValWorker
 					return true;
 				if (ff.has_ce && initconst(ff.sig_ce.as_bit()) == (ff.pol_ce ? State::S0 : State::S1))
 					continue;
-				if (ff.has_srst && initconst(ff.sig_ce.as_bit()) == (ff.pol_srst ? State::S1 : State::S0))
+				if (ff.has_srst && initconst(ff.sig_srst.as_bit()) == (ff.pol_srst ? State::S1 : State::S0))
 					continue;
 
 				return true;