From d4b6042e439f2e8c8059820501c0bcaad7576155 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 13 Apr 2024 11:20:36 +1200 Subject: [PATCH 1/9] Makefile: Separate docs/usage stderr and stdout --- Makefile | 25 ++++++++++++++++++------- 1 file changed, 18 insertions(+), 7 deletions(-) diff --git a/Makefile b/Makefile index 6d7bb2cec..5e9f2163d 100644 --- a/Makefile +++ b/Makefile @@ -985,16 +985,27 @@ docs/gen_images: $(Q) $(MAKE) -C docs images DOCS_GUIDELINE_FILES := GettingStarted CodingStyle -docs/guidelines: +docs/guidelines docs/source/temp: $(Q) mkdir -p docs/source/temp $(Q) cp -f $(addprefix guidelines/,$(DOCS_GUIDELINE_FILES)) docs/source/temp -# many of these will return an error which can be safely ignored, so we prefix -# the command with a '-' -DOCS_USAGE_PROGS := yosys yosys-config yosys-filterlib yosys-abc yosys-smtbmc yosys-witness -docs/usage: $(addprefix docs/source/temp/,$(DOCS_USAGE_PROGS)) -docs/source/temp/%: docs/guidelines - -$(Q) ./$(PROGRAM_PREFIX)$* --help > $@ 2>&1 +# some commands return an error and print the usage text to stderr +define DOC_USAGE_STDERR +docs/source/temp/$(1): $(PROGRAM_PREFIX)$(1) docs/source/temp + -$(Q) ./$$< --help 2> $$@ +endef +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/temp/$(1): $(PROGRAM_PREFIX)$(1) docs/source/temp + $(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/temp/,$(DOCS_USAGE_STDOUT) $(DOCS_USAGE_STDERR)) docs/reqs: $(Q) $(MAKE) -C docs reqs From 1d7b7ddfd7c7b1322bb5ab0ec98eeaf184f410ce Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 13 Apr 2024 11:29:11 +1200 Subject: [PATCH 2/9] Docs: Skip footer in logs --- docs/source/code_examples/extensions/Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/source/code_examples/extensions/Makefile b/docs/source/code_examples/extensions/Makefile index 288983ed3..5a7994874 100644 --- a/docs/source/code_examples/extensions/Makefile +++ b/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' 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' 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' sigmap_test.v mv test2.log_new test2.log .PHONY: clean From b3024289c6e6984cbc4111e42901dce9e01bdc0a Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Sat, 13 Apr 2024 11:33:04 +1200 Subject: [PATCH 3/9] Docs: Force read_verilog to avoid verific header --- docs/source/code_examples/extensions/Makefile | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/docs/source/code_examples/extensions/Makefile b/docs/source/code_examples/extensions/Makefile index 5a7994874..8b5fa106a 100644 --- a/docs/source/code_examples/extensions/Makefile +++ b/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) -QTl 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) -QTl 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) -QTl 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 From 953f5bbe6ca8ce8b4612383482e42f6b7978fd85 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 15 Apr 2024 09:50:46 +1200 Subject: [PATCH 4/9] Docs: Remove end-before tag for yosys-abc --- docs/source/appendix/auxprogs.rst | 1 - 1 file changed, 1 deletion(-) diff --git a/docs/source/appendix/auxprogs.rst b/docs/source/appendix/auxprogs.rst index b6defbe80..05a2c646d 100644 --- a/docs/source/appendix/auxprogs.rst +++ b/docs/source/appendix/auxprogs.rst @@ -38,7 +38,6 @@ two. .. literalinclude:: /temp/yosys-abc :start-at: usage - :end-before: UC Berkeley yosys-smtbmc ------------ From 73d021562f57ab9217a65ee2c7c6e21909378ba3 Mon Sep 17 00:00:00 2001 From: Krystine Sherwin <93062060+KrystalDelusion@users.noreply.github.com> Date: Mon, 15 Apr 2024 10:13:22 +1200 Subject: [PATCH 5/9] Docs: Rename source/temp to source/generated --- Makefile | 12 ++++++------ docs/.gitignore | 2 +- docs/Makefile | 1 + docs/source/appendix/auxprogs.rst | 10 +++++----- docs/source/cmd_ref.rst | 2 +- 5 files changed, 14 insertions(+), 13 deletions(-) diff --git a/Makefile b/Makefile index 5e9f2163d..acd9e18fa 100644 --- a/Makefile +++ b/Makefile @@ -985,13 +985,13 @@ docs/gen_images: $(Q) $(MAKE) -C docs images DOCS_GUIDELINE_FILES := GettingStarted CodingStyle -docs/guidelines docs/source/temp: - $(Q) mkdir -p docs/source/temp - $(Q) cp -f $(addprefix guidelines/,$(DOCS_GUIDELINE_FILES)) docs/source/temp +docs/guidelines docs/source/generated: + $(Q) mkdir -p docs/source/generated + $(Q) cp -f $(addprefix guidelines/,$(DOCS_GUIDELINE_FILES)) docs/source/generated # some commands return an error and print the usage text to stderr define DOC_USAGE_STDERR -docs/source/temp/$(1): $(PROGRAM_PREFIX)$(1) docs/source/temp +docs/source/generated/$(1): $(PROGRAM_PREFIX)$(1) docs/source/generated -$(Q) ./$$< --help 2> $$@ endef DOCS_USAGE_STDERR := yosys-config yosys-filterlib yosys-abc @@ -999,13 +999,13 @@ $(foreach usage,$(DOCS_USAGE_STDERR),$(eval $(call DOC_USAGE_STDERR,$(usage)))) # others print to stdout define DOC_USAGE_STDOUT -docs/source/temp/$(1): $(PROGRAM_PREFIX)$(1) docs/source/temp +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/temp/,$(DOCS_USAGE_STDOUT) $(DOCS_USAGE_STDERR)) +docs/usage: $(addprefix docs/source/generated/,$(DOCS_USAGE_STDOUT) $(DOCS_USAGE_STDERR)) docs/reqs: $(Q) $(MAKE) -C docs reqs diff --git a/docs/.gitignore b/docs/.gitignore index d7bfd8e95..65bbcdeae 100644 --- a/docs/.gitignore +++ b/docs/.gitignore @@ -1,6 +1,6 @@ /build/ /source/cmd -/source/temp +/source/generated /source/_images/**/*.log /source/_images/**/*.aux /source/_images/**/*.pdf diff --git a/docs/Makefile b/docs/Makefile index a5b2fed6b..701157ee6 100644 --- a/docs/Makefile +++ b/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 diff --git a/docs/source/appendix/auxprogs.rst b/docs/source/appendix/auxprogs.rst index 05a2c646d..c239136b6 100644 --- a/docs/source/appendix/auxprogs.rst +++ b/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,7 +36,7 @@ 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 yosys-smtbmc @@ -45,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 ------------- @@ -54,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. diff --git a/docs/source/cmd_ref.rst b/docs/source/cmd_ref.rst index f0c4eaaf9..acf2d1d41 100644 --- a/docs/source/cmd_ref.rst +++ b/docs/source/cmd_ref.rst @@ -4,7 +4,7 @@ Command line reference ================================================================================ -.. literalinclude:: /temp/yosys +.. literalinclude:: /generated/yosys :start-at: Usage .. toctree:: From 2bd889a59a07a2ce057fa0c941234fb8e521edcc Mon Sep 17 00:00:00 2001 From: Jannis Harder Date: Mon, 15 Apr 2024 11:53:30 +0200 Subject: [PATCH 6/9] formalff -setundef: Fix handling for has_srst FFs The `has_srst`` case was checking `sig_ce` instead of `sig_srst` due to a copy and paste error. This would crash when `has_ce` was false and could incorrectly determine that an initial value is unused when `has_ce` and `has_srst` are both set. --- passes/sat/formalff.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/passes/sat/formalff.cc b/passes/sat/formalff.cc index 264a9fb3b..0eadb69e0 100644 --- a/passes/sat/formalff.cc +++ b/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; From af94123730c13ca5e48b231031873b270542ecba Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Mon, 15 Apr 2024 17:01:07 +0200 Subject: [PATCH 7/9] verific: expose library name as module attribute --- frontends/verific/verific.cc | 1 + 1 file changed, 1 insertion(+) diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index e6c5865b7..81e79f749 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -1430,6 +1430,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); From 40e8f5b69de5063cd2adb6565a00992be83b5515 Mon Sep 17 00:00:00 2001 From: "github-actions[bot]" <41898282+github-actions[bot]@users.noreply.github.com> Date: Tue, 16 Apr 2024 00:15:48 +0000 Subject: [PATCH 8/9] Bump version --- Makefile | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 87c19786d..32ca398c2 100644 --- a/Makefile +++ b/Makefile @@ -142,7 +142,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 From c38bbd7824edee850c328d8798c78494733fd1ef Mon Sep 17 00:00:00 2001 From: Miodrag Milanovic Date: Tue, 16 Apr 2024 07:50:50 +0200 Subject: [PATCH 9/9] Add new verific testing environment CI --- .github/workflows/test-verific.yml | 77 ++++++++++++++++++++++++++++++ 1 file changed, 77 insertions(+) create mode 100644 .github/workflows/test-verific.yml diff --git a/.github/workflows/test-verific.yml b/.github/workflows/test-verific.yml new file mode 100644 index 000000000..b4383eba4 --- /dev/null +++ b/.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