mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-06-20 15:50:27 +00:00
Code Activity

Merge branch 'YosysHQ:main' into master

Browse source
This commit is contained in:
Eder Monteiro 2026-03-04 11:40:58 +00:00 • committed by GitHub
commit 62558e9ce9
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
71 changed files with 1703 additions and 445 deletions
Download patch file Download diff file Expand all files Collapse all files

11
.github/actions/setup-build-env/action.yml vendored
View file

@ -42,7 +42,7 @@ runs:
if: runner.os == 'Linux' && inputs.get-build-deps == 'true'
uses: awalsh128/cache-apt-pkgs-action@v1.6.0
with:
packages: bison clang flex libffi-dev libfl-dev libreadline-dev pkg-config tcl-dev zlib1g-dev
packages: bison clang flex libffi-dev libfl-dev libreadline-dev pkg-config tcl-dev zlib1g-dev libgtest-dev
version: ${{ inputs.runs-on }}-buildys
- name: Linux docs dependencies
@ -52,15 +52,6 @@ runs:
packages: graphviz xdot
version: ${{ inputs.runs-on }}-docsys
# if updating test dependencies, make sure to update
# docs/source/yosys_internals/extending_yosys/test_suites.rst to match.
- name: Linux test dependencies
if: runner.os == 'Linux' && inputs.get-test-deps == 'true'
uses: awalsh128/cache-apt-pkgs-action@v1.6.0
with:
packages: libgtest-dev
version: ${{ inputs.runs-on }}-testys
- name: Install macOS Dependencies
if: runner.os == 'macOS'
shell: bash

1
.github/workflows/extra-builds.yml vendored
View file

@ -103,6 +103,7 @@ jobs:
ENABLE_ZLIB := 0
CXXFLAGS += -I$(pwd)/flex-prefix/include
LINKFLAGS += -Wl,-z,stack-size=8388608 -Wl,--stack-first -Wl,--strip-all
END
make -C build -f ../Makefile CXX=clang -j$(nproc)

5
.github/workflows/test-build.yml vendored
View file

@ -72,6 +72,7 @@ jobs:
cd build
make -f ../Makefile config-$CC
make -f ../Makefile -j$procs
make -f ../Makefile unit-test -j$procs
- name: Log yosys-config output
run: |
@ -81,7 +82,7 @@ jobs:
shell: bash
run: |
cd build
tar -cvf ../build.tar share/ yosys yosys-*
tar -cvf ../build.tar share/ yosys yosys-* libyosys.so
- name: Store build artifact
uses: actions/upload-artifact@v4
@ -131,7 +132,7 @@ jobs:
- name: Run tests
shell: bash
run: |
make -j$procs test TARGETS= EXTRA_TARGETS= CONFIG=$CC
make -j$procs vanilla-test TARGETS= EXTRA_TARGETS= CONFIG=$CC
- name: Report errors
if: ${{ failure() }}

6
.github/workflows/test-sanitizers.yml vendored
View file

@ -65,7 +65,7 @@ jobs:
- name: Run tests
shell: bash
run: |
make -j$procs test TARGETS= EXTRA_TARGETS=
make -j$procs vanilla-test TARGETS= EXTRA_TARGETS=
- name: Report errors
if: ${{ failure() }}
@ -73,7 +73,3 @@ jobs:
run: |
find tests/**/*.err -print -exec cat {} \;
- name: Run unit tests
shell: bash
run: |
make -j$procs unit-test ENABLE_LIBYOSYS=1

109
.github/workflows/test-verific-cfg.yml vendored Normal file
View file

@ -0,0 +1,109 @@
name: Build various Verific configurations
on:
workflow_dispatch:
jobs:
test-verific-cfg:
if: github.repository_owner == 'YosysHQ'
runs-on: [self-hosted, linux, x64, fast]
steps:
- name: Checkout Yosys
uses: actions/checkout@v4
with:
persist-credentials: false
submodules: true
- name: Runtime environment
run: |
echo "procs=$(nproc)" >> $GITHUB_ENV
- name: verific [SV]
run: |
make config-clang
echo "ENABLE_VERIFIC := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_VHDL := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_HIER_TREE := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf
echo "ENABLE_CCACHE := 1" >> Makefile.conf
make -j$procs
- name: verific [VHDL]
run: |
make config-clang
echo "ENABLE_VERIFIC := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_SYSTEMVERILOG := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_HIER_TREE := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf
echo "ENABLE_CCACHE := 1" >> Makefile.conf
make -j$procs
- name: verific [SV + VHDL]
run: |
make config-clang
echo "ENABLE_VERIFIC := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_HIER_TREE := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf
echo "ENABLE_CCACHE := 1" >> Makefile.conf
make -j$procs
- name: verific [SV + HIER]
run: |
make config-clang
echo "ENABLE_VERIFIC := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_VHDL := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_HIER_TREE := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf
echo "ENABLE_CCACHE := 1" >> Makefile.conf
make -j$procs
- name: verific [VHDL + HIER]
run: |
make config-clang
echo "ENABLE_VERIFIC := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_SYSTEMVERILOG := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_HIER_TREE := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf
echo "ENABLE_CCACHE := 1" >> Makefile.conf
make -j$procs
- name: verific [SV + VHDL + HIER]
run: |
make config-clang
echo "ENABLE_VERIFIC := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_HIER_TREE := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_EDIF := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_LIBERTY := 0" >> Makefile.conf
echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf
echo "ENABLE_CCACHE := 1" >> Makefile.conf
make -j$procs
- name: verific [SV + VHDL + HIER + EDIF + LIBERTY]
run: |
make config-clang
echo "ENABLE_VERIFIC := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_SYSTEMVERILOG := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_VHDL := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_HIER_TREE := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_EDIF := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_LIBERTY := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_YOSYSHQ_EXTENSIONS := 0" >> Makefile.conf
echo "ENABLE_CCACHE := 1" >> Makefile.conf
make -j$procs

7
.github/workflows/test-verific.yml vendored
View file

@ -68,7 +68,7 @@ jobs:
- name: Run Yosys tests
run: |
make -j$procs test
make -j$procs vanilla-test
- name: Run Verific specific Yosys tests
run: |
@ -80,11 +80,6 @@ jobs:
run: |
make -C sby run_ci
- name: Run unit tests
shell: bash
run: |
make -j$procs unit-test ENABLE_LTO=1 ENABLE_LIBYOSYS=1
test-pyosys:
needs: pre-job
if: ${{ needs.pre-job.outputs.should_skip != 'true' && github.repository == 'YosysHQ/Yosys' }}

25
.github/workflows/update-flake-lock.yml vendored
View file

@ -1,25 +0,0 @@
name: update-flake-lock
on:
workflow_dispatch: # allows manual triggering
schedule:
- cron: '0 0 * * 0' # runs weekly on Sunday at 00:00
jobs:
lockfile:
if: github.repository == 'YosysHQ/Yosys'
runs-on: ubuntu-latest
steps:
- name: Checkout repository
uses: actions/checkout@v4
with:
persist-credentials: false
- name: Install Nix
uses: DeterminateSystems/nix-installer-action@main
- name: Update flake.lock
uses: DeterminateSystems/update-flake-lock@main
with:
token: ${{CI_CREATE_PR_TOKEN}}
pr-title: "Update flake.lock" # Title of PR to be created
pr-labels: | # Labels to be set on the PR
dependencies
automated

34
.github/workflows/version.yml vendored
View file

@ -1,34 +0,0 @@
name: Bump version
on:
workflow_dispatch:
schedule:
- cron: '0 0 * * *'
jobs:
bump-version:
if: github.repository == 'YosysHQ/Yosys'
runs-on: ubuntu-latest
steps:
- name: Checkout
uses: actions/checkout@v4
with:
fetch-depth: 0
submodules: true
persist-credentials: false
- name: Take last commit
id: log
run: echo "message=$(git log --no-merges -1 --oneline)" >> $GITHUB_OUTPUT
- name: Bump version
if: ${{ !contains(steps.log.outputs.message, 'Bump version') }}
run: |
make bumpversion
git config --local user.email "41898282+github-actions[bot]@users.noreply.github.com"
git config --local user.name "github-actions[bot]"
git add Makefile
git commit -m "Bump version"
- name: Push changes # push the output folder to your repo
if: ${{ !contains(steps.log.outputs.message, 'Bump version') }}
uses: ad-m/github-push-action@master
with:
github_token: ${{ secrets.GITHUB_TOKEN }}

17
CHANGELOG
View file

@ -2,9 +2,24 @@
List of major changes and improvements between releases
=======================================================
Yosys 0.62 .. Yosys 0.63-dev
Yosys 0.63 .. Yosys 0.64-dev
--------------------------
Yosys 0.62 .. Yosys 0.63
--------------------------
* Various
- Added DSP inference for Gowin GW1N and GW2A.
- Added support for subtract in preadder for Xilinx arch.
- Added infrastructure to run a sat solver as a command.
* New commands and options
- Added "-ignore-unknown-cells" option to "equiv_induct"
and "equiv_simple" pass.
- Added "-force-params" option to "memory_libmap" pass.
- Added "-select-solver" option to "sat" pass.
- Added "-default_params" option to "write_verilog" pass.
- Added "-nodsp" option to "synth_gowin" pass.
Yosys 0.61 .. Yosys 0.62
--------------------------
* Various

58
Dockerfile
View file

@ -1,58 +0,0 @@
ARG IMAGE="python:3-slim-buster"
#---
FROM $IMAGE AS base
RUN apt-get update -qq \
&& DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
ca-certificates \
clang \
lld \
curl \
libffi-dev \
libreadline-dev \
tcl-dev \
graphviz \
xdot \
&& apt-get autoclean && apt-get clean && apt-get -y autoremove \
&& update-ca-certificates \
&& rm -rf /var/lib/apt/lists
#---
FROM base AS build
RUN apt-get update -qq \
&& DEBIAN_FRONTEND=noninteractive apt-get -y install --no-install-recommends \
bison \
flex \
gawk \
gcc \
git \
iverilog \
pkg-config \
&& apt-get autoclean && apt-get clean && apt-get -y autoremove \
&& rm -rf /var/lib/apt/lists
COPY . /yosys
ENV PREFIX /opt/yosys
RUN cd /yosys \
&& make \
&& make install \
&& make test
#---
FROM base
COPY --from=build /opt/yosys /opt/yosys
ENV PATH /opt/yosys/bin:$PATH
RUN useradd -m yosys
USER yosys
CMD ["yosys"]

50
Makefile
View file

@ -161,7 +161,19 @@ ifeq ($(OS), Haiku)
CXXFLAGS += -D_DEFAULT_SOURCE
endif
YOSYS_VER := 0.62+9
YOSYS_VER := 0.63
ifneq (, $(shell command -v git 2>/dev/null))
ifneq (, $(shell git rev-parse --git-dir 2>/dev/null))
GIT_COMMIT_COUNT := $(or $(shell git rev-list --count v$(YOSYS_VER)..HEAD 2>/dev/null),0)
ifneq ($(GIT_COMMIT_COUNT),0)
YOSYS_VER := $(YOSYS_VER)+$(GIT_COMMIT_COUNT)
endif
else
YOSYS_VER := $(YOSYS_VER)+post
endif
endif
YOSYS_MAJOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f1)
YOSYS_MINOR := $(shell echo $(YOSYS_VER) | cut -d'.' -f2 | cut -d'+' -f1)
YOSYS_COMMIT := $(shell echo $(YOSYS_VER) | cut -d'+' -f2)
@ -185,9 +197,6 @@ endif
OBJS = kernel/version_$(GIT_REV).o
bumpversion:
sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 7326bb7.. | wc -l`/;" Makefile
ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q)
# set ABCEXTERNAL = <abc-command> to use an external ABC instance
@ -638,6 +647,7 @@ $(eval $(call add_include_file,kernel/yosys_common.h))
$(eval $(call add_include_file,kernel/yw.h))
$(eval $(call add_include_file,libs/ezsat/ezsat.h))
$(eval $(call add_include_file,libs/ezsat/ezminisat.h))
$(eval $(call add_include_file,libs/ezsat/ezcmdline.h))
ifeq ($(ENABLE_ZLIB),1)
$(eval $(call add_include_file,libs/fst/fstapi.h))
endif
@ -683,6 +693,7 @@ OBJS += libs/json11/json11.o
OBJS += libs/ezsat/ezsat.o
OBJS += libs/ezsat/ezminisat.o
OBJS += libs/ezsat/ezcmdline.o
OBJS += libs/minisat/Options.o
OBJS += libs/minisat/SimpSolver.o
@ -791,9 +802,30 @@ endif
$(Q) mkdir -p $(dir $@)
$(P) $(CXX) -o $@ -c $(CPPFLAGS) $(CXXFLAGS) $<
YOSYS_REPO :=
ifneq (, $(shell command -v git 2>/dev/null))
ifneq (, $(shell git rev-parse --git-dir 2>/dev/null))
GIT_REMOTE := $(strip $(shell git config --get remote.origin.url 2>/dev/null | $(AWK) '{print tolower($$0)}'))
ifneq ($(strip $(GIT_REMOTE)),)
YOSYS_REPO := $(strip $(shell echo $(GIT_REMOTE) | $(AWK) -F '[:/]' '{gsub(/\.git$$/, "", $$NF); printf "%s/%s", $$(NF-1), $$NF}'))
endif
ifeq ($(strip $(YOSYS_REPO)),yosyshq/yosys)
YOSYS_REPO :=
endif
GIT_BRANCH := $(shell git rev-parse --abbrev-ref HEAD 2>/dev/null)
ifeq ($(filter main HEAD release/v%,$(GIT_BRANCH)),)
YOSYS_REPO := $(YOSYS_REPO) at $(GIT_BRANCH)
endif
YOSYS_REPO := $(strip $(YOSYS_REPO))
endif
endif
YOSYS_GIT_STR := $(GIT_REV)$(GIT_DIRTY)
YOSYS_COMPILER := $(notdir $(CXX)) $(shell $(CXX) --version | tr ' ()' '\n' | grep '^[0-9]' | head -n1) $(filter -f% -m% -O% -DNDEBUG,$(CXXFLAGS))
YOSYS_VER_STR := Yosys $(YOSYS_VER) (git sha1 $(YOSYS_GIT_STR), $(YOSYS_COMPILER))
ifneq ($(strip $(YOSYS_REPO)),)
YOSYS_VER_STR := $(YOSYS_VER_STR) [$(YOSYS_REPO)]
endif
kernel/version_$(GIT_REV).cc: $(YOSYS_SRC)/Makefile
$(P) rm -f kernel/version_*.o kernel/version_*.d kernel/version_*.cc
@ -977,9 +1009,11 @@ makefile-tests/%: %/run-test.mk $(TARGETS) $(EXTRA_TARGETS)
$(MAKE) -C $* -f run-test.mk
+@echo "...passed tests in $*"
test: makefile-tests abcopt-tests seed-tests
test: vanilla-test unit-test
vanilla-test: makefile-tests abcopt-tests seed-tests
@echo ""
@echo " Passed \"make test\"."
@echo " Passed \"make vanilla-test\"."
ifeq ($(ENABLE_VERIFIC),1)
ifeq ($(YOSYS_NOVERIFIC),1)
@echo " Ran tests without verific support due to YOSYS_NOVERIFIC=1."
@ -1011,11 +1045,11 @@ ystests: $(TARGETS) $(EXTRA_TARGETS)
# Unit test
unit-test: libyosys.so
@$(MAKE) -C $(UNITESTPATH) CXX="$(CXX)" CC="$(CC)" CPPFLAGS="$(CPPFLAGS)" \
@$(MAKE) -f $(UNITESTPATH)/Makefile CXX="$(CXX)" CC="$(CC)" CPPFLAGS="$(CPPFLAGS)" \
CXXFLAGS="$(CXXFLAGS)" LINKFLAGS="$(LINKFLAGS)" LIBS="$(LIBS)" ROOTPATH="$(CURDIR)"
clean-unit-test:
@$(MAKE) -C $(UNITESTPATH) clean
@$(MAKE) -f $(UNITESTPATH)/Makefile clean
install-dev: $(PROGRAM_PREFIX)yosys-config share
$(INSTALL_SUDO) mkdir -p $(DESTDIR)$(BINDIR)

4
README.md
View file

@ -114,8 +114,8 @@ To build Yosys simply type 'make' in this directory.
$ sudo make install
Tests are located in the tests subdirectory and can be executed using the test
target. Note that you need gawk as well as a recent version of iverilog (i.e.
build from git). Then, execute tests via:
target. Note that you need gawk, a recent version of iverilog, and gtest.
Execute tests via:
$ make test

2
abc

@ -1 +1 @@
Subproject commit 734f64d5b907158dc4337ee82b3b74566d74ba08
Subproject commit 8e401543d3ecf65e3a3631c7a271793a4d356cb0

4
backends/aiger/aiger.cc
View file

@ -930,7 +930,9 @@ struct AigerBackend : public Backend {
log(" make indexes zero based, enable using map files with smt solvers.\n");
log("\n");
log(" -ywmap <filename>\n");
log(" write a map file for conversion to and from yosys witness traces.\n");
log(" write a map file for conversion to and from yosys witness traces,\n");
log(" also allows for mapping AIGER bad-state properties and invariant\n");
log(" constraints back to individual formal properties by name.\n");
log("\n");
log(" -I, -O, -B, -L\n");
log(" If the design contains no input/output/assert/flip-flop then create one\n");

23
backends/verilog/verilog_backend.cc
View file

@ -95,7 +95,8 @@ bool VERILOG_BACKEND::id_is_verilog_escaped(const std::string &str) {
PRIVATE_NAMESPACE_BEGIN
bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs, noparallelcase;
bool verbose, norename, noattr, attr2comment, noexpr, nodec, nohex, nostr, extmem, defparam, decimal, siminit, systemverilog, simple_lhs,
noparallelcase, default_params;
int auto_name_counter, auto_name_offset, auto_name_digits, extmem_counter;
dict<RTLIL::IdString, int> auto_name_map;
std::set<RTLIL::IdString> reg_wires;
@ -421,6 +422,13 @@ void dump_attributes(std::ostream &f, std::string indent, dict<RTLIL::IdString,
}
}
void dump_parameter(std::ostream &f, std::string indent, RTLIL::IdString id_string, RTLIL::Const parameter)
{
f << stringf("%sparameter %s = ", indent.c_str(), id(id_string).c_str());
dump_const(f, parameter);
f << ";\n";
}
void dump_wire(std::ostream &f, std::string indent, RTLIL::Wire *wire)
{
dump_attributes(f, indent, wire->attributes, "\n", /*modattr=*/false, /*regattr=*/reg_wires.count(wire->name));
@ -2438,6 +2446,10 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module)
f << indent + " " << "reg " << id(initial_id) << " = 0;\n";
}
if (default_params)
for (auto p : module->parameter_default_values)
dump_parameter(f, indent + " ", p.first, p.second);
// first dump input / output according to their order in module->ports
for (auto port : module->ports)
dump_wire(f, indent + " ", module->wire(port));
@ -2545,6 +2557,10 @@ struct VerilogBackend : public Backend {
log(" use 'defparam' statements instead of the Verilog-2001 syntax for\n");
log(" cell parameters.\n");
log("\n");
log(" -default_params\n");
log(" emit module parameter declarations from\n");
log(" parameter_default_values.\n");
log("\n");
log(" -blackboxes\n");
log(" usually modules with the 'blackbox' attribute are ignored. with\n");
log(" this option set only the modules with the 'blackbox' attribute\n");
@ -2582,6 +2598,7 @@ struct VerilogBackend : public Backend {
siminit = false;
simple_lhs = false;
noparallelcase = false;
default_params = false;
auto_prefix = "";
bool blackboxes = false;
@ -2642,6 +2659,10 @@ struct VerilogBackend : public Backend {
defparam = true;
continue;
}
if (arg == "-defaultparams") {
default_params = true;
continue;
}
if (arg == "-decimal") {
decimal = true;
continue;

2
docs/source/conf.py
View file

@ -6,7 +6,7 @@ import os
project = 'YosysHQ Yosys'
author = 'YosysHQ GmbH'
copyright ='2026 YosysHQ GmbH'
yosys_ver = "0.62"
yosys_ver = "0.63"
# select HTML theme
html_theme = 'furo-ys'

35
docs/source/using_yosys/more_scripting/model_checking.rst
View file

@ -3,9 +3,9 @@ Symbolic model checking
.. todo:: check text context
.. note::
While it is possible to perform model checking directly in Yosys, it
.. note::
While it is possible to perform model checking directly in Yosys, it
is highly recommended to use SBY or EQY for formal hardware verification.
Symbolic Model Checking (SMC) is used to formally prove that a circuit has (or
@ -117,3 +117,32 @@ Result with fixed :file:`axis_master.v`:
Solving problem with 159144 variables and 441626 clauses..
SAT proof finished - no model found: SUCCESS!
Witness framework and per-property tracking
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When using AIGER-based formal verification flows (such as the ``abc`` engine in
SBY), Yosys provides infrastructure for tracking individual formal
properties through the verification pipeline.
The `rename -witness` pass assigns public names to all cells that participate in
the witness framework:
- Witness signal cells: `$anyconst`, `$anyseq`, `$anyinit`,
`$allconst`, `$allseq`
- Formal property cells: `$assert`, `$assume`, `$cover`, `$live`,
`$fair`, `$check`
These public names allow downstream tools to refer to individual properties by
their hierarchical path rather than by anonymous internal identifiers.
The `write_aiger -ywmap` option generates a map file for conversion to and from
Yosys witness traces, and also allows for mapping AIGER bad-state properties and
invariant constraints back to individual formal properties by name. This enables
features like per-property pass/fail reporting (e.g. ``abc pdr`` with
``--keep-going`` mode).
The `write_smt2` backend similarly uses the public witness names when emitting
SMT2 comments. Cells whose ``hdlname`` attribute contains the ``_witness_``
marker are treated as having private names for comment purposes, keeping solver
output clean.

56
docs/source/yosys_internals/extending_yosys/test_suites.rst
View file

@ -8,7 +8,44 @@ Running the included test suite
The Yosys source comes with a test suite to avoid regressions and keep
everything working as expected. Tests can be run by calling ``make test`` from
the root Yosys directory.
the root Yosys directory. By default, this runs vanilla and unit tests.
Vanilla tests
~~~~~~~~~~~~~
These make up the majority of our testing coverage.
They can be run with ``make vanilla-test`` and are based on calls to
make subcommands (``make makefile-tests``) and shell scripts
(``make seed-tests`` and ``make abcopt-tests``). Both use ``run-test.sh``
files, but make-based tests only call ``tests/gen-tests-makefile.sh``
to generate a makefile appropriate for the given directory, so only
afterwards when make is invoked do the tests actually run.
Usually their structure looks something like this:
you write a .ys file that gets automatically run,
which runs a frontend like ``read_verilog`` or ``read_rtlil`` with
a relative path or a heredoc, then runs some commands including the command
under test, and then uses :doc:`/using_yosys/more_scripting/selections`
with ``-assert-count``. Usually it's unnecessary to "register" the test anywhere
as if it's being added to an existing directory, depending
on how the ``run-test.sh`` in that directory works.
Unit tests
~~~~~~~~~~
Running the unit tests requires the following additional packages:
.. tab:: Ubuntu
.. code:: console
sudo apt-get install libgtest-dev
.. tab:: macOS
No additional requirements.
Unit tests can be run with ``make unit-test``.
Functional tests
~~~~~~~~~~~~~~~~
@ -41,23 +78,6 @@ instructions <https://github.com/Z3Prover/z3>`_.
Then, set the :makevar:`ENABLE_FUNCTIONAL_TESTS` make variable when calling
``make test`` and the functional tests will be run as well.
Unit tests
~~~~~~~~~~
Running the unit tests requires the following additional packages:
.. tab:: Ubuntu
.. code:: console
sudo apt-get install libgtest-dev
.. tab:: macOS
No additional requirements.
Unit tests can be run with ``make unit-test``.
Docs tests
~~~~~~~~~~

20
frontends/aiger/aigerparse.cc
View file

@ -286,10 +286,15 @@ end_of_header:
RTLIL::IdString escaped_s = stringf("\\%s", s);
RTLIL::Wire* wire;
if (c == 'i') wire = inputs[l1];
else if (c == 'l') wire = latches[l1];
else if (c == 'o') {
if (c == 'i') {
log_assert(l1 < inputs.size());
wire = inputs[l1];
} else if (c == 'l') {
log_assert(l1 < latches.size());
wire = latches[l1];
} else if (c == 'o') {
wire = module->wire(escaped_s);
log_assert(l1 < outputs.size());
if (wire) {
// Could have been renamed by a latch
module->swap_names(wire, outputs[l1]);
@ -297,9 +302,9 @@ end_of_header:
goto next;
}
wire = outputs[l1];
}
else if (c == 'b') wire = bad_properties[l1];
else log_abort();
} else if (c == 'b') {
wire = bad_properties[l1];
} else log_abort();
module->rename(wire, escaped_s);
}
@ -652,6 +657,9 @@ void AigerReader::parse_aiger_binary()
unsigned l1, l2, l3;
std::string line;
if (M != I + L + A)
log_error("Binary AIGER input is malformed: maximum variable index M is %u, but number of inputs, latches and AND gates adds up to %u.\n", M, I + L + A);
// Parse inputs
int digits = decimal_digits(I);
for (unsigned i = 1; i <= I; ++i) {

12
frontends/ast/genrtlil.cc
View file

@ -403,6 +403,18 @@ struct AST_INTERNAL::ProcessGenerator
if (GetSize(syncrule->signal) != 1)
always->input_error("Found posedge/negedge event on a signal that is not 1 bit wide!\n");
addChunkActions(syncrule->actions, subst_lvalue_from, subst_lvalue_to, true);
// Automatic (nosync) variables must not become flip-flops: remove
// them from clocked sync rules so that proc_dff does not infer
// an unnecessary register for a purely combinational temporary.
syncrule->actions.erase(
std::remove_if(syncrule->actions.begin(), syncrule->actions.end(),
[](const RTLIL::SigSig &ss) {
for (auto &chunk : ss.first.chunks())
if (chunk.wire && chunk.wire->get_bool_attribute(ID::nosync))
return true;
return false;
}),
syncrule->actions.end());
proc->syncs.push_back(syncrule);
}
if (proc->syncs.empty()) {

1
frontends/blif/blifparse.cc
View file

@ -629,6 +629,7 @@ void parse_blif(RTLIL::Design *design, std::istream &f, IdString dff_name, bool
goto try_next_value;
}
}
log_assert(i < lutptr->size());
lutptr->set(i, !strcmp(output, "0") ? RTLIL::State::S0 : RTLIL::State::S1);
try_next_value:;
}

3
frontends/json/jsonparse.cc
View file

@ -302,6 +302,9 @@ void json_import(Design *design, string &modname, JsonNode *node)
if (node->data_dict.count("attributes"))
json_parse_attr_param(module->attributes, node->data_dict.at("attributes"));
if (node->data_dict.count("parameter_default_values"))
json_parse_attr_param(module->parameter_default_values, node->data_dict.at("parameter_default_values"));
dict<int, SigBit> signal_bits;
if (node->data_dict.count("ports"))

18
frontends/verilog/verilog_parser.y
View file

@ -84,7 +84,7 @@
int current_function_or_task_port_id;
std::vector<char> case_type_stack;
bool do_not_require_port_stubs;
bool current_wire_rand, current_wire_const;
bool current_wire_rand, current_wire_const, current_wire_automatic;
bool current_modport_input, current_modport_output;
bool default_nettype_wire = true;
std::istream* lexin;
@ -958,14 +958,18 @@ delay:
non_opt_delay | %empty;
io_wire_type:
{ extra->astbuf3 = std::make_unique<AstNode>(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; }
{ extra->astbuf3 = std::make_unique<AstNode>(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; extra->current_wire_automatic = false; }
wire_type_token_io wire_type_const_rand opt_wire_type_token wire_type_signedness
{ $$ = std::move(extra->astbuf3); SET_RULE_LOC(@$, @2, @$); };
non_io_wire_type:
{ extra->astbuf3 = std::make_unique<AstNode>(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; }
wire_type_const_rand wire_type_token wire_type_signedness
{ $$ = std::move(extra->astbuf3); SET_RULE_LOC(@$, @2, @$); };
{ extra->astbuf3 = std::make_unique<AstNode>(@$, AST_WIRE); extra->current_wire_rand = false; extra->current_wire_const = false; extra->current_wire_automatic = false; }
opt_lifetime wire_type_const_rand wire_type_token wire_type_signedness
{
if (extra->current_wire_automatic)
extra->astbuf3->set_attribute(ID::nosync, AstNode::mkconst_int(extra->astbuf3->location, 1, false));
$$ = std::move(extra->astbuf3); SET_RULE_LOC(@$, @2, @$);
};
wire_type:
io_wire_type { $$ = std::move($1); } |
@ -1253,6 +1257,10 @@ opt_automatic:
TOK_AUTOMATIC |
%empty;
opt_lifetime:
TOK_AUTOMATIC { extra->current_wire_automatic = true; } |
%empty;
task_func_args_opt:
TOK_LPAREN TOK_RPAREN | %empty | TOK_LPAREN {
extra->albuf = nullptr;

2
kernel/calc.cc
View file

@ -291,7 +291,7 @@ static RTLIL::Const const_shift_worker(const RTLIL::Const &arg1, const RTLIL::Co
if (pos < 0)
result.set(i, vacant_bits);
else if (pos >= BigInteger(GetSize(arg1)))
result.set(i, sign_ext ? arg1.back() : vacant_bits);
result.set(i, sign_ext && !arg1.empty() ? arg1.back() : vacant_bits);
else
result.set(i, arg1[pos.toInt()]);
}

144
kernel/celledges.cc
View file

@ -112,6 +112,41 @@ void reduce_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
db->add_edge(cell, ID::A, i, ID::Y, 0, -1);
}
void logic_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
{
int a_width = GetSize(cell->getPort(ID::A));
int b_width = GetSize(cell->getPort(ID::B));
for (int i = 0; i < a_width; i++)
db->add_edge(cell, ID::A, i, ID::Y, 0, -1);
for (int i = 0; i < b_width; i++)
db->add_edge(cell, ID::B, i, ID::Y, 0, -1);
}
void concat_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
{
int a_width = GetSize(cell->getPort(ID::A));
int b_width = GetSize(cell->getPort(ID::B));
for (int i = 0; i < a_width; i++)
db->add_edge(cell, ID::A, i, ID::Y, i, -1);
for (int i = 0; i < b_width; i++)
db->add_edge(cell, ID::B, i, ID::Y, a_width + i, -1);
}
void slice_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
{
int offset = cell->getParam(ID::OFFSET).as_int();
int a_width = GetSize(cell->getPort(ID::A));
int y_width = GetSize(cell->getPort(ID::Y));
for (int i = 0; i < y_width; i++) {
int a_bit = offset + i;
if (a_bit >= 0 && a_bit < a_width)
db->add_edge(cell, ID::A, a_bit, ID::Y, i, -1);
}
}
void compare_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
{
int a_width = GetSize(cell->getPort(ID::A));
@ -254,7 +289,7 @@ void shift_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
int skip = 1 << (k + 1);
int base = skip -1;
if (i % skip != base && i - a_width + 2 < 1 << b_width_capped)
db->add_edge(cell, ID::B, k, ID::Y, i, -1);
db->add_edge(cell, ID::B, k, ID::Y, i, -1);
} else if (is_signed) {
if (i - a_width + 2 < 1 << b_width_capped)
db->add_edge(cell, ID::B, k, ID::Y, i, -1);
@ -388,6 +423,64 @@ void ff_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
db->add_edge(cell, ID::ARST, 0, ID::Q, k, -1);
}
void full_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
{
std::vector<RTLIL::IdString> input_ports;
std::vector<RTLIL::IdString> output_ports;
for (auto &conn : cell->connections())
{
RTLIL::IdString port = conn.first;
RTLIL::PortDir dir = cell->port_dir(port);
if (cell->input(port) || dir == RTLIL::PortDir::PD_INOUT)
input_ports.push_back(port);
if (cell->output(port) || dir == RTLIL::PortDir::PD_INOUT)
output_ports.push_back(port);
}
for (auto out_port : output_ports)
{
int out_width = GetSize(cell->getPort(out_port));
for (int out_bit = 0; out_bit < out_width; out_bit++)
{
for (auto in_port : input_ports)
{
int in_width = GetSize(cell->getPort(in_port));
for (int in_bit = 0; in_bit < in_width; in_bit++)
db->add_edge(cell, in_port, in_bit, out_port, out_bit, -1);
}
}
}
}
void bweqx_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
{
int width = GetSize(cell->getPort(ID::Y));
int a_width = GetSize(cell->getPort(ID::A));
int b_width = GetSize(cell->getPort(ID::B));
int max_width = std::min(width, std::min(a_width, b_width));
for (int i = 0; i < max_width; i++) {
db->add_edge(cell, ID::A, i, ID::Y, i, -1);
db->add_edge(cell, ID::B, i, ID::Y, i, -1);
}
}
void bwmux_op(AbstractCellEdgesDatabase *db, RTLIL::Cell *cell)
{
int width = GetSize(cell->getPort(ID::Y));
int a_width = GetSize(cell->getPort(ID::A));
int b_width = GetSize(cell->getPort(ID::B));
int s_width = GetSize(cell->getPort(ID::S));
int max_width = std::min(width, std::min(a_width, std::min(b_width, s_width)));
for (int i = 0; i < max_width; i++) {
db->add_edge(cell, ID::A, i, ID::Y, i, -1);
db->add_edge(cell, ID::B, i, ID::Y, i, -1);
db->add_edge(cell, ID::S, i, ID::Y, i, -1);
}
}
PRIVATE_NAMESPACE_END
bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL::Cell *cell)
@ -417,6 +510,21 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL
return true;
}
if (cell->type.in(ID($logic_and), ID($logic_or))) {
logic_op(this, cell);
return true;
}
if (cell->type == ID($slice)) {
slice_op(this, cell);
return true;
}
if (cell->type == ID($concat)) {
concat_op(this, cell);
return true;
}
if (cell->type.in(ID($shl), ID($shr), ID($sshl), ID($sshr), ID($shift), ID($shiftx))) {
shift_op(this, cell);
return true;
@ -442,6 +550,16 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL
return true;
}
if (cell->type == ID($bweqx)) {
bweqx_op(this, cell);
return true;
}
if (cell->type == ID($bwmux)) {
bwmux_op(this, cell);
return true;
}
if (cell->type.in(ID($mem_v2), ID($memrd), ID($memrd_v2), ID($memwr), ID($memwr_v2), ID($meminit))) {
mem_op(this, cell);
return true;
@ -452,13 +570,24 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL
return true;
}
// FIXME: $mul $div $mod $divfloor $modfloor $slice $concat
// FIXME: $lut $sop $alu $lcu $macc $macc_v2 $fa
// FIXME: $mul $div $mod $divfloor $modfloor $pow $slice $concat $bweqx
// FIXME: $lut $sop $alu $lcu $macc $fa $logic_and $logic_or $bwmux
if (cell->type.in(ID($mul), ID($div), ID($mod), ID($divfloor), ID($modfloor), ID($pow))) {
full_op(this, cell);
return true;
}
// FIXME: $_BUF_ $_NOT_ $_AND_ $_NAND_ $_OR_ $_NOR_ $_XOR_ $_XNOR_ $_ANDNOT_ $_ORNOT_
// FIXME: $_MUX_ $_NMUX_ $_MUX4_ $_MUX8_ $_MUX16_ $_AOI3_ $_OAI3_ $_AOI4_ $_OAI4_
if (cell->type.in(ID($lut), ID($sop), ID($alu), ID($lcu), ID($macc), ID($macc_v2))) {
full_op(this, cell);
return true;
}
if (cell->type.in(
ID($_BUF_), ID($_NOT_), ID($_AND_), ID($_NAND_), ID($_OR_), ID($_NOR_),
ID($_XOR_), ID($_XNOR_), ID($_ANDNOT_), ID($_ORNOT_), ID($_MUX_), ID($_NMUX_),
ID($_MUX4_), ID($_MUX8_), ID($_MUX16_), ID($_AOI3_), ID($_OAI3_), ID($_AOI4_),
ID($_OAI4_), ID($_TBUF_))) {
full_op(this, cell);
return true;
}
// FIXME: $specify2 $specify3 $specrule ???
// FIXME: $equiv $set_tag $get_tag $overwrite_tag $original_tag
@ -468,4 +597,3 @@ bool YOSYS_NAMESPACE_PREFIX AbstractCellEdgesDatabase::add_edges_from_cell(RTLIL
return false;
}

35
kernel/modtools.h
View file

@ -28,6 +28,22 @@ YOSYS_NAMESPACE_BEGIN
struct ModIndex : public RTLIL::Monitor
{
struct PointerOrderedSigBit : public RTLIL::SigBit {
PointerOrderedSigBit(SigBit s) {
wire = s.wire;
if (wire)
offset = s.offset;
else
data = s.data;
}
inline bool operator<(const RTLIL::SigBit &other) const {
if (wire == other.wire)
return wire ? (offset < other.offset) : (data < other.data);
if (wire != nullptr && other.wire != nullptr)
return wire < other.wire; // look here
return (wire != nullptr) < (other.wire != nullptr);
}
};
struct PortInfo {
RTLIL::Cell* cell;
RTLIL::IdString port;
@ -77,7 +93,7 @@ struct ModIndex : public RTLIL::Monitor
SigMap sigmap;
RTLIL::Module *module;
std::map<RTLIL::SigBit, SigBitInfo> database;
std::map<PointerOrderedSigBit, SigBitInfo> database;
int auto_reload_counter;
bool auto_reload_module;
@ -94,8 +110,11 @@ struct ModIndex : public RTLIL::Monitor
{
for (int i = 0; i < GetSize(sig); i++) {
RTLIL::SigBit bit = sigmap(sig[i]);
if (bit.wire)
if (bit.wire) {
database[bit].ports.erase(PortInfo(cell, port, i));
if (!database[bit].is_input && !database[bit].is_output && database[bit].ports.empty())
database.erase(bit);
}
}
}
@ -132,11 +151,11 @@ struct ModIndex : public RTLIL::Monitor
}
}
void check()
bool ok()
{
#ifndef NDEBUG
if (auto_reload_module)
return;
return true;
for (auto it : database)
log_assert(it.first == sigmap(it.first));
@ -156,11 +175,17 @@ struct ModIndex : public RTLIL::Monitor
else if (!(it.second == database_bak.at(it.first)))
log("ModuleIndex::check(): Different content for database[%s].\n", log_signal(it.first));
log_assert(database == database_bak);
return false;
}
return true;
#endif
}
void check()
{
log_assert(ok());
}
void notify_connect(RTLIL::Cell *cell, RTLIL::IdString port, const RTLIL::SigSpec &old_sig, const RTLIL::SigSpec &sig) override
{
log_assert(module == cell->module);

22
kernel/satgen.cc
View file

@ -19,6 +19,7 @@
#include "kernel/satgen.h"
#include "kernel/ff.h"
#include "kernel/yosys_common.h"
USING_YOSYS_NAMESPACE
@ -1378,7 +1379,7 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
return true;
}
if (cell->type == ID($scopeinfo))
if (cell->type == ID($scopeinfo) || cell->type == ID($input_port))
{
return true;
}
@ -1387,3 +1388,22 @@ bool SatGen::importCell(RTLIL::Cell *cell, int timestep)
// .. and all sequential cells with asynchronous inputs
return false;
}
namespace Yosys {
void report_missing_model(bool warn_only, RTLIL::Cell* cell)
{
std::string s;
if (cell->is_builtin_ff())
s = stringf("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type));
else
s = stringf("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
if (warn_only) {
log_formatted_warning_noprefix(s);
} else {
log_formatted_error(s);
}
}
}

3
kernel/satgen.h
View file

@ -59,6 +59,7 @@ struct SatSolver
struct ezSatPtr : public std::unique_ptr<ezSAT> {
ezSatPtr() : unique_ptr<ezSAT>(yosys_satsolver->create()) { }
explicit ezSatPtr(SatSolver *solver) : unique_ptr<ezSAT>((solver ? solver : yosys_satsolver)->create()) { }
};
struct SatGen
@ -292,6 +293,8 @@ struct SatGen
bool importCell(RTLIL::Cell *cell, int timestep = -1);
};
void report_missing_model(bool warn_only, RTLIL::Cell* cell);
YOSYS_NAMESPACE_END
#endif

92
libs/ezsat/ezcmdline.cc Normal file
View file

@ -0,0 +1,92 @@
#include "ezcmdline.h"
#include "../../kernel/yosys.h"
ezCmdlineSAT::ezCmdlineSAT(const std::string &cmd) : command(cmd) {}
ezCmdlineSAT::~ezCmdlineSAT() {}
bool ezCmdlineSAT::solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions)
{
#if !defined(YOSYS_DISABLE_SPAWN)
const std::string tempdir_name = Yosys::make_temp_dir(Yosys::get_base_tmpdir() + "/yosys-sat-XXXXXX");
const std::string cnf_filename = Yosys::stringf("%s/problem.cnf", tempdir_name.c_str());
const std::string sat_command = Yosys::stringf("%s %s", command.c_str(), cnf_filename.c_str());
FILE *dimacs = fopen(cnf_filename.c_str(), "w");
if (dimacs == nullptr) {
Yosys::log_cmd_error("Failed to create CNF file `%s`.\n", cnf_filename.c_str());
}
std::vector<int> modelIdx;
for (auto id : modelExpressions)
modelIdx.push_back(bind(id));
std::vector<std::vector<int>> extraClauses;
for (auto id : assumptions)
extraClauses.push_back({bind(id)});
printDIMACS(dimacs, false, extraClauses);
fclose(dimacs);
bool status_sat = false;
bool status_unsat = false;
std::vector<bool> values;
auto line_callback = [&](const std::string &line) {
if (line.empty()) {
return;
}
if (line[0] == 's') {
if (line.substr(0, 5) == "s SAT") {
status_sat = true;
}
if (line.substr(0, 7) == "s UNSAT") {
status_unsat = true;
}
return;
}
if (line[0] == 'v') {
std::stringstream ss(line.substr(1));
int lit;
while (ss >> lit) {
if (lit == 0) {
return;
}
bool val = lit >= 0;
int ind = lit >= 0 ? lit - 1 : -lit - 1;
if (Yosys::GetSize(values) <= ind) {
values.resize(ind + 1);
}
values[ind] = val;
}
}
};
int return_code = Yosys::run_command(sat_command, line_callback);
if (return_code != 0 && return_code != 10 && return_code != 20) {
Yosys::log_cmd_error("Shell command failed!\n");
}
modelValues.clear();
modelValues.resize(modelIdx.size());
if (!status_sat && !status_unsat) {
solverTimeoutStatus = true;
}
if (!status_sat) {
return false;
}
for (size_t i = 0; i < modelIdx.size(); i++) {
int idx = modelIdx[i];
bool refvalue = true;
if (idx < 0)
idx = -idx, refvalue = false;
modelValues[i] = (values.at(idx - 1) == refvalue);
}
return true;
#else
Yosys::log_error("SAT solver command not available in this build!\n");
#endif
}

36
libs/ezsat/ezcmdline.h Normal file
View file

@ -0,0 +1,36 @@
/*
* ezSAT -- A simple and easy to use CNF generator for SAT solvers
*
* Copyright (C) 2013 Claire Xenia Wolf <claire@yosyshq.com>
*
* 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 EZSATCOMMAND_H
#define EZSATCOMMAND_H
#include "ezsat.h"
class ezCmdlineSAT : public ezSAT
{
private:
std::string command;
public:
ezCmdlineSAT(const std::string &cmd);
virtual ~ezCmdlineSAT();
bool solver(const std::vector<int> &modelExpressions, std::vector<bool> &modelValues, const std::vector<int> &assumptions) override;
};
#endif

4
libs/ezsat/ezminisat.cc
View file

@ -103,7 +103,7 @@ bool ezMiniSAT::solver(const std::vector<int> &modelExpressions, std::vector<boo
{
preSolverCallback();
solverTimoutStatus = false;
solverTimeoutStatus = false;
if (0) {
contradiction:
@ -206,7 +206,7 @@ contradiction:
#if defined(HAS_ALARM)
if (solverTimeout > 0) {
if (alarmHandlerTimeout == 0)
solverTimoutStatus = true;
solverTimeoutStatus = true;
alarm(0);
sigaction(SIGALRM, &old_sig_action, NULL);
alarm(old_alarm_timeout);

15
libs/ezsat/ezsat.cc
View file

@ -54,7 +54,7 @@ ezSAT::ezSAT()
cnfClausesCount = 0;
solverTimeout = 0;
solverTimoutStatus = false;
solverTimeoutStatus = false;
literal("CONST_TRUE");
literal("CONST_FALSE");
@ -1222,10 +1222,15 @@ ezSATvec ezSAT::vec(const std::vector<int> &vec)
return ezSATvec(*this, vec);
}
void ezSAT::printDIMACS(FILE *f, bool verbose) const
void ezSAT::printDIMACS(FILE *f, bool verbose, const std::vector<std::vector<int>> &extraClauses) const
{
if (f == nullptr) {
fprintf(stderr, "Usage error: printDIMACS() must not be called with a null FILE pointer\n");
abort();
}
if (cnfConsumed) {
fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!");
fprintf(stderr, "Usage error: printDIMACS() must not be called after cnfConsumed()!\n");
abort();
}
@ -1259,8 +1264,10 @@ void ezSAT::printDIMACS(FILE *f, bool verbose) const
std::vector<std::vector<int>> all_clauses;
getFullCnf(all_clauses);
assert(cnfClausesCount == int(all_clauses.size()));
for (auto c : extraClauses)
all_clauses.push_back(c);
fprintf(f, "p cnf %d %d\n", cnfVariableCount, cnfClausesCount);
fprintf(f, "p cnf %d %d\n", cnfVariableCount, (int) all_clauses.size());
int maxClauseLen = 0;
for (auto &clause : all_clauses)
maxClauseLen = std::max(int(clause.size()), maxClauseLen);

8
libs/ezsat/ezsat.h
View file

@ -78,7 +78,7 @@ protected:
public:
int solverTimeout;
bool solverTimoutStatus;
bool solverTimeoutStatus;
ezSAT();
virtual ~ezSAT();
@ -153,8 +153,8 @@ public:
solverTimeout = newTimeoutSeconds;
}
bool getSolverTimoutStatus() {
return solverTimoutStatus;
bool getSolverTimeoutStatus() {
return solverTimeoutStatus;
}
// manage CNF (usually only accessed by SAT solvers)
@ -295,7 +295,7 @@ public:
// printing CNF and internal state
void printDIMACS(FILE *f, bool verbose = false) const;
void printDIMACS(FILE *f, bool verbose = false, const std::vector<std::vector<int>> &extraClauses = std::vector<std::vector<int>>()) const;
void printInternalState(FILE *f) const;
// more sophisticated constraints (designed to be used directly with assume(..))

15
passes/cmds/rename.cc
View file

@ -254,18 +254,17 @@ struct RenamePass : public Pass {
log("\n");
log(" rename -enumerate [-pattern <pattern>] [selection]\n");
log("\n");
log("Assign short auto-generated names to all selected wires and cells with private\n");
log("names. The -pattern option can be used to set the pattern for the new names.\n");
log("The character %% in the pattern is replaced with a integer number. The default\n");
log("pattern is '_%%_'.\n");
log("Assigns auto-generated names to objects used in formal verification\n");
log("that do not have a public name. This applies to all formal property\n");
log("cells, $any*/$all* output wires, and their containing cells.\n");
log("\n");
log("\n");
log(" rename -witness\n");
log("\n");
log("Assigns auto-generated names to all $any*/$all* output wires and containing\n");
log("cells that do not have a public name. This ensures that, during formal\n");
log("verification, a solver-found trace can be fully specified using a public\n");
log("hierarchical names.\n");
log("Assigns auto-generated names to objects used in formal verification\n");
log("that do not have a public name. This applies to all formal property\n");
log("cells ($assert, $assume, $cover, $live, $fair, $check), $any*/$all*\n");
log("output wires, and their containing cells.\n");
log("\n");
log("\n");
log(" rename -hide [selection]\n");

2
passes/cmds/scratchpad.cc
View file

@ -37,7 +37,7 @@ struct ScratchpadPass : public Pass {
log("\n");
log(" scratchpad [options]\n");
log("\n");
log("This pass allows to read and modify values from the scratchpad of the current\n");
log("This pass allows reading and modifying values from the scratchpad of the current\n");
log("design. Options:\n");
log("\n");
log(" -get <identifier>\n");

67
passes/equiv/equiv.h Normal file
View file

@ -0,0 +1,67 @@
#ifndef EQUIV_H
#define EQUIV_H
#include "kernel/log.h"
#include "kernel/yosys_common.h"
#include "kernel/sigtools.h"
#include "kernel/satgen.h"
YOSYS_NAMESPACE_BEGIN
struct EquivBasicConfig {
bool model_undef = false;
int max_seq = 1;
bool set_assumes = false;
bool ignore_unknown_cells = false;
bool parse(const std::vector<std::string>& args, size_t& idx) {
if (args[idx] == "-undef") {
model_undef = true;
return true;
}
if (args[idx] == "-seq" && idx+1 < args.size()) {
max_seq = atoi(args[++idx].c_str());
return true;
}
if (args[idx] == "-set-assumes") {
set_assumes = true;
return true;
}
if (args[idx] == "-ignore-unknown-cells") {
ignore_unknown_cells = true;
return true;
}
return false;
}
static std::string help(const char* default_seq) {
return stringf(
" -undef\n"
" enable modelling of undef states\n"
"\n"
" -seq <N>\n"
" the max. number of time steps to be considered (default = %s)\n"
"\n"
" -set-assumes\n"
" set all assumptions provided via $assume cells\n"
"\n"
" -ignore-unknown-cells\n"
" ignore all cells that can not be matched to a SAT model\n"
, default_seq);
}
};
template<typename Config = EquivBasicConfig>
struct EquivWorker {
RTLIL::Module *module;
ezSatPtr ez;
SatGen satgen;
Config cfg;
EquivWorker(RTLIL::Module *module, const SigMap *sigmap, Config cfg) : module(module), satgen(ez.get(), sigmap), cfg(cfg) {
satgen.model_undef = cfg.model_undef;
}
};
YOSYS_NAMESPACE_END
#endif // EQUIV_H

66
passes/equiv/equiv_induct.cc
View file

@ -18,49 +18,34 @@
*/
#include "kernel/yosys.h"
#include "kernel/satgen.h"
#include "kernel/sigtools.h"
#include "passes/equiv/equiv.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
struct EquivInductWorker
struct EquivInductWorker : public EquivWorker<>
{
Module *module;
SigMap sigmap;
vector<Cell*> cells;
pool<Cell*> workset;
ezSatPtr ez;
SatGen satgen;
int max_seq;
int success_counter;
bool set_assumes;
dict<int, int> ez_step_is_consistent;
pool<Cell*> cell_warn_cache;
SigPool undriven_signals;
EquivInductWorker(Module *module, const pool<Cell*> &unproven_equiv_cells, bool model_undef, int max_seq, bool set_assumes) : module(module), sigmap(module),
EquivInductWorker(Module *module, const pool<Cell*> &unproven_equiv_cells, EquivBasicConfig cfg) : EquivWorker<>(module, &sigmap, cfg), sigmap(module),
cells(module->selected_cells()), workset(unproven_equiv_cells),
satgen(ez.get(), &sigmap), max_seq(max_seq), success_counter(0), set_assumes(set_assumes)
{
satgen.model_undef = model_undef;
}
success_counter(0) {}
void create_timestep(int step)
{
vector<int> ez_equal_terms;
for (auto cell : cells) {
if (!satgen.importCell(cell, step) && !cell_warn_cache.count(cell)) {
if (cell->is_builtin_ff())
log_warning("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type));
else
log_warning("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
cell_warn_cache.insert(cell);
if (!satgen.importCell(cell, step)) {
report_missing_model(cfg.ignore_unknown_cells, cell);
}
if (cell->type == ID($equiv)) {
SigBit bit_a = sigmap(cell->getPort(ID::A)).as_bit();
@ -78,7 +63,7 @@ struct EquivInductWorker
}
}
if (set_assumes) {
if (cfg.set_assumes) {
if (step == 1) {
RTLIL::SigSpec assumes_a, assumes_en;
satgen.getAssumes(assumes_a, assumes_en, step);
@ -123,7 +108,7 @@ struct EquivInductWorker
GetSize(satgen.initial_state), GetSize(undriven_signals));
}
for (int step = 1; step <= max_seq; step++)
for (int step = 1; step <= cfg.max_seq; step++)
{
ez->assume(ez_step_is_consistent[step]);
@ -146,7 +131,7 @@ struct EquivInductWorker
return;
}
log(" Proof for induction step failed. %s\n", step != max_seq ? "Extending to next time step." : "Trying to prove individual $equiv from workset.");
log(" Proof for induction step failed. %s\n", step != cfg.max_seq ? "Extending to next time step." : "Trying to prove individual $equiv from workset.");
}
workset.sort();
@ -158,12 +143,12 @@ struct EquivInductWorker
log(" Trying to prove $equiv for %s:", log_signal(sigmap(cell->getPort(ID::Y))));
int ez_a = satgen.importSigBit(bit_a, max_seq+1);
int ez_b = satgen.importSigBit(bit_b, max_seq+1);
int ez_a = satgen.importSigBit(bit_a, cfg.max_seq+1);
int ez_b = satgen.importSigBit(bit_b, cfg.max_seq+1);
int cond = ez->XOR(ez_a, ez_b);
if (satgen.model_undef)
cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_a, max_seq+1)));
cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_a, cfg.max_seq+1)));
if (!ez->solve(cond)) {
log(" success!\n");
@ -189,14 +174,7 @@ struct EquivInductPass : public Pass {
log("Only selected $equiv cells are proven and only selected cells are used to\n");
log("perform the proof.\n");
log("\n");
log(" -undef\n");
log(" enable modelling of undef states\n");
log("\n");
log(" -seq <N>\n");
log(" the max. number of time steps to be considered (default = 4)\n");
log("\n");
log(" -set-assumes\n");
log(" set all assumptions provided via $assume cells\n");
log("%s", EquivBasicConfig::help("4"));
log("\n");
log("This command is very effective in proving complex sequential circuits, when\n");
log("the internal state of the circuit quickly propagates to $equiv cells.\n");
@ -214,25 +192,15 @@ struct EquivInductPass : public Pass {
void execute(std::vector<std::string> args, Design *design) override
{
int success_counter = 0;
bool model_undef = false, set_assumes = false;
int max_seq = 4;
EquivBasicConfig cfg {};
cfg.max_seq = 4;
log_header(design, "Executing EQUIV_INDUCT pass.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
if (args[argidx] == "-undef") {
model_undef = true;
if (cfg.parse(args, argidx))
continue;
}
if (args[argidx] == "-seq" && argidx+1 < args.size()) {
max_seq = atoi(args[++argidx].c_str());
continue;
}
if (args[argidx] == "-set-assumes") {
set_assumes = true;
continue;
}
break;
}
extra_args(args, argidx, design);
@ -253,7 +221,7 @@ struct EquivInductPass : public Pass {
continue;
}
EquivInductWorker worker(module, unproven_equiv_cells, model_undef, max_seq, set_assumes);
EquivInductWorker worker(module, unproven_equiv_cells, cfg);
worker.run();
success_counter += worker.success_counter;
}

123
passes/equiv/equiv_simple.cc
View file

@ -17,15 +17,51 @@
*
*/
#include "kernel/log.h"
#include "kernel/yosys.h"
#include "kernel/satgen.h"
#include "passes/equiv/equiv.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
struct EquivSimpleWorker
struct EquivSimpleConfig : EquivBasicConfig {
bool verbose = false;
bool short_cones = false;
bool group = true;
bool parse(const std::vector<std::string>& args, size_t& idx) {
if (EquivBasicConfig::parse(args, idx))
return true;
if (args[idx] == "-v") {
verbose = true;
return true;
}
if (args[idx] == "-short") {
short_cones = true;
return true;
}
if (args[idx] == "-nogroup") {
group = false;
return true;
}
return false;
}
static std::string help(const char* default_seq) {
return EquivBasicConfig::help(default_seq) +
" -v\n"
" verbose output\n"
"\n"
" -short\n"
" create shorter input cones that stop at shared nodes. This yields\n"
" simpler SAT problems but sometimes fails to prove equivalence.\n"
"\n"
" -nogroup\n"
" disabling grouping of $equiv cells by output wire\n"
"\n";
}
};
struct EquivSimpleWorker : public EquivWorker<EquivSimpleConfig>
{
Module *module;
const vector<Cell*> &equiv_cells;
const vector<Cell*> &assume_cells;
struct Cone {
@ -43,27 +79,11 @@ struct EquivSimpleWorker
};
DesignModel model;
ezSatPtr ez;
SatGen satgen;
struct Config {
bool verbose = false;
bool short_cones = false;
bool model_undef = false;
bool nogroup = false;
bool set_assumes = false;
int max_seq = 1;
};
Config cfg;
pool<pair<Cell*, int>> imported_cells_cache;
EquivSimpleWorker(const vector<Cell*> &equiv_cells, const vector<Cell*> &assume_cells, DesignModel model, Config cfg) :
module(equiv_cells.front()->module), equiv_cells(equiv_cells), assume_cells(assume_cells),
model(model), satgen(ez.get(), &model.sigmap), cfg(cfg)
{
satgen.model_undef = cfg.model_undef;
}
EquivSimpleWorker(const vector<Cell*> &equiv_cells, const vector<Cell*> &assume_cells, DesignModel model, EquivSimpleConfig cfg) :
EquivWorker<EquivSimpleConfig>(equiv_cells.front()->module, &model.sigmap, cfg), equiv_cells(equiv_cells), assume_cells(assume_cells),
model(model) {}
struct ConeFinder {
DesignModel model;
@ -229,14 +249,6 @@ struct EquivSimpleWorker
return extra_problem_cells;
}
static void report_missing_model(Cell* cell)
{
if (cell->is_builtin_ff())
log_cmd_error("No SAT model available for async FF cell %s (%s). Consider running `async2sync` or `clk2fflogic` first.\n", log_id(cell), log_id(cell->type));
else
log_cmd_error("No SAT model available for cell %s (%s).\n", log_id(cell), log_id(cell->type));
}
void prepare_ezsat(int ez_context, SigBit bit_a, SigBit bit_b)
{
if (satgen.model_undef)
@ -257,7 +269,9 @@ struct EquivSimpleWorker
}
void construct_ezsat(const pool<SigBit>& input_bits, int step)
{
log("ezsat\n");
if (cfg.set_assumes) {
log("yep assume\n");
if (cfg.verbose && step == cfg.max_seq) {
RTLIL::SigSpec assumes_a, assumes_en;
satgen.getAssumes(assumes_a, assumes_en, step+1);
@ -323,7 +337,7 @@ struct EquivSimpleWorker
for (auto cell : problem_cells) {
auto key = pair<Cell*, int>(cell, step+1);
if (!imported_cells_cache.count(key) && !satgen.importCell(cell, step+1)) {
report_missing_model(cell);
report_missing_model(cfg.ignore_unknown_cells, cell);
}
imported_cells_cache.insert(key);
}
@ -414,59 +428,20 @@ struct EquivSimplePass : public Pass {
log("\n");
log("This command tries to prove $equiv cells using a simple direct SAT approach.\n");
log("\n");
log(" -v\n");
log(" verbose output\n");
log("\n");
log(" -undef\n");
log(" enable modelling of undef states\n");
log("\n");
log(" -short\n");
log(" create shorter input cones that stop at shared nodes. This yields\n");
log(" simpler SAT problems but sometimes fails to prove equivalence.\n");
log("\n");
log(" -nogroup\n");
log(" disabling grouping of $equiv cells by output wire\n");
log("\n");
log(" -seq <N>\n");
log(" the max. number of time steps to be considered (default = 1)\n");
log("\n");
log(" -set-assumes\n");
log(" set all assumptions provided via $assume cells\n");
log("%s", EquivSimpleConfig::help("1"));
log("\n");
}
void execute(std::vector<std::string> args, Design *design) override
{
EquivSimpleWorker::Config cfg = {};
EquivSimpleConfig cfg {};
int success_counter = 0;
log_header(design, "Executing EQUIV_SIMPLE pass.\n");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
if (args[argidx] == "-v") {
cfg.verbose = true;
if (cfg.parse(args, argidx))
continue;
}
if (args[argidx] == "-short") {
cfg.short_cones = true;
continue;
}
if (args[argidx] == "-undef") {
cfg.model_undef = true;
continue;
}
if (args[argidx] == "-nogroup") {
cfg.nogroup = true;
continue;
}
if (args[argidx] == "-seq" && argidx+1 < args.size()) {
cfg.max_seq = atoi(args[++argidx].c_str());
continue;
}
if (args[argidx] == "-set-assumes") {
cfg.set_assumes = true;
continue;
}
break;
}
extra_args(args, argidx, design);
@ -489,7 +464,7 @@ struct EquivSimplePass : public Pass {
if (cell->type == ID($equiv) && cell->getPort(ID::A) != cell->getPort(ID::B)) {
auto bit = sigmap(cell->getPort(ID::Y).as_bit());
auto bit_group = bit;
if (!cfg.nogroup && bit_group.wire)
if (cfg.group && bit_group.wire)
bit_group.offset = 0;
unproven_equiv_cells[bit_group][bit] = cell;
unproven_cells_counter++;

15
passes/memory/memory_libmap.cc
View file

@ -39,6 +39,7 @@ struct PassOptions {
bool no_auto_distributed;
bool no_auto_block;
bool no_auto_huge;
bool force_params;
double logic_cost_rom;
double logic_cost_ram;
};
@ -1859,7 +1860,7 @@ void MemMapping::emit_port(const MemConfig &cfg, std::vector<Cell*> &cells, cons
cell->setParam(stringf("\\PORT_%s_WR_BE_WIDTH", name), GetSize(hw_wren));
} else {
cell->setPort(stringf("\\PORT_%s_WR_EN", name), hw_wren);
if (cfg.def->byte != 0 && cfg.def->width_mode != WidthMode::Single)
if (cfg.def->byte != 0 && (cfg.def->width_mode != WidthMode::Single || opts.force_params))
cell->setParam(stringf("\\PORT_%s_WR_EN_WIDTH", name), GetSize(hw_wren));
}
}
@ -2068,8 +2069,10 @@ void MemMapping::emit(const MemConfig &cfg) {
std::vector<Cell *> cells;
for (int rd = 0; rd < cfg.repl_d; rd++) {
Cell *cell = mem.module->addCell(stringf("%s.%d.%d", mem.memid, rp, rd), cfg.def->id);
if (cfg.def->width_mode == WidthMode::Global)
if (cfg.def->width_mode == WidthMode::Global || opts.force_params)
cell->setParam(ID::WIDTH, cfg.def->dbits[cfg.base_width_log2]);
if (opts.force_params)
cell->setParam(ID::ABITS, cfg.def->abits);
if (cfg.def->widthscale) {
std::vector<State> val;
for (auto &bit: init_swz.bits[rd])
@ -2179,6 +2182,9 @@ struct MemoryLibMapPass : public Pass {
log(" Disables automatic mapping of given kind of RAMs. Manual mapping\n");
log(" (using ram_style or other attributes) is still supported.\n");
log("\n");
log(" -force-params\n");
log(" Always generate memories with WIDTH and ABITS parameters.\n");
log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
@ -2188,6 +2194,7 @@ struct MemoryLibMapPass : public Pass {
opts.no_auto_distributed = false;
opts.no_auto_block = false;
opts.no_auto_huge = false;
opts.force_params = false;
opts.logic_cost_ram = 1.0;
opts.logic_cost_rom = 1.0/16.0;
log_header(design, "Executing MEMORY_LIBMAP pass (mapping memories to cells).\n");
@ -2214,6 +2221,10 @@ struct MemoryLibMapPass : public Pass {
opts.no_auto_huge = true;
continue;
}
if (args[argidx] == "-force-params") {
opts.force_params = true;
continue;
}
if (args[argidx] == "-logic-cost-rom" && argidx+1 < args.size()) {
opts.logic_cost_rom = strtod(args[++argidx].c_str(), nullptr);
continue;

64
passes/sat/sat.cc
View file

@ -31,6 +31,22 @@
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
static SatSolver *find_satsolver(const std::string &name)
{
for (auto solver = yosys_satsolver_list; solver != nullptr; solver = solver->next)
if (solver->name == name)
return solver;
return nullptr;
}
static std::string list_satsolvers()
{
std::string result;
for (auto solver = yosys_satsolver_list; solver != nullptr; solver = solver->next)
result += result.empty() ? solver->name : ", " + solver->name;
return result;
}
struct SatHelper
{
RTLIL::Design *design;
@ -60,8 +76,8 @@ struct SatHelper
int max_timestep, timeout;
bool gotTimeout;
SatHelper(RTLIL::Design *design, RTLIL::Module *module, bool enable_undef, bool set_def_formal) :
design(design), module(module), sigmap(module), ct(design), satgen(ez.get(), &sigmap)
SatHelper(RTLIL::Design *design, RTLIL::Module *module, SatSolver *solver, bool enable_undef, bool set_def_formal) :
design(design), module(module), sigmap(module), ct(design), ez(solver), satgen(ez.get(), &sigmap)
{
this->enable_undef = enable_undef;
satgen.model_undef = enable_undef;
@ -227,16 +243,12 @@ struct SatHelper
int import_cell_counter = 0;
for (auto cell : module->cells())
if (design->selected(module, cell)) {
// log("Import cell: %s\n", RTLIL::id2cstr(cell->name));
if (satgen.importCell(cell, timestep)) {
for (auto &p : cell->connections())
if (ct.cell_output(cell->type, p.first))
show_drivers.insert(sigmap(p.second), cell);
import_cell_counter++;
} else if (ignore_unknown_cells)
log_warning("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
else
log_error("Failed to import cell %s (type %s) to SAT database.\n", RTLIL::id2cstr(cell->name), RTLIL::id2cstr(cell->type));
} else report_missing_model(ignore_unknown_cells, cell);
}
log("Imported %d cells to SAT database.\n", import_cell_counter);
@ -441,7 +453,7 @@ struct SatHelper
log_assert(gotTimeout == false);
ez->setSolverTimeout(timeout);
bool success = ez->solve(modelExpressions, modelValues, assumptions);
if (ez->getSolverTimoutStatus())
if (ez->getSolverTimeoutStatus())
gotTimeout = true;
return success;
}
@ -451,7 +463,7 @@ struct SatHelper
log_assert(gotTimeout == false);
ez->setSolverTimeout(timeout);
bool success = ez->solve(modelExpressions, modelValues, a, b, c, d, e, f);
if (ez->getSolverTimoutStatus())
if (ez->getSolverTimeoutStatus())
gotTimeout = true;
return success;
}
@ -961,10 +973,10 @@ struct SatPass : public Pass {
log(" -show-regs, -show-public, -show-all\n");
log(" show all registers, show signals with 'public' names, show all signals\n");
log("\n");
log(" -ignore_div_by_zero\n");
log(" -ignore-div-by-zero\n");
log(" ignore all solutions that involve a division by zero\n");
log("\n");
log(" -ignore_unknown_cells\n");
log(" -ignore-unknown-cells\n");
log(" ignore all cells that can not be matched to a SAT model\n");
log("\n");
log("The following options can be used to set up a sequential problem:\n");
@ -1066,6 +1078,10 @@ struct SatPass : public Pass {
log(" -timeout <N>\n");
log(" Maximum number of seconds a single SAT instance may take.\n");
log("\n");
log(" -select-solver <name>\n");
log(" Select SAT solver implementation for this invocation.\n");
log(" If not given, uses scratchpad key 'sat.solver' if set, otherwise default.\n");
log("\n");
log(" -verify\n");
log(" Return an error and stop the synthesis script if the proof fails.\n");
log("\n");
@ -1097,8 +1113,14 @@ struct SatPass : public Pass {
log_header(design, "Executing SAT pass (solving SAT problems in the circuit).\n");
std::string solver_name = design->scratchpad_get_string("sat.solver", "");
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++) {
if (args[argidx] == "-select-solver" && argidx+1 < args.size()) {
solver_name = args[++argidx];
continue;
}
if (args[argidx] == "-all") {
loopcount = -1;
continue;
@ -1141,7 +1163,7 @@ struct SatPass : public Pass {
stepsize = max(1, atoi(args[++argidx].c_str()));
continue;
}
if (args[argidx] == "-ignore_div_by_zero") {
if (args[argidx] == "-ignore-div-by-zero" || args[argidx] == "-ignore_div_by_zero") {
ignore_div_by_zero = true;
continue;
}
@ -1316,7 +1338,7 @@ struct SatPass : public Pass {
show_all = true;
continue;
}
if (args[argidx] == "-ignore_unknown_cells") {
if (args[argidx] == "-ignore-unknown-cells" || args[argidx] == "-ignore_unknown_cells") {
ignore_unknown_cells = true;
continue;
}
@ -1336,6 +1358,14 @@ struct SatPass : public Pass {
}
extra_args(args, argidx, design);
SatSolver *solver = yosys_satsolver;
if (!solver_name.empty()) {
solver = find_satsolver(solver_name);
if (solver == nullptr)
log_cmd_error("Unknown SAT solver '%s'. Available solvers: %s\n",
solver_name, list_satsolvers());
}
RTLIL::Module *module = NULL;
for (auto mod : design->selected_modules()) {
if (module)
@ -1398,13 +1428,15 @@ struct SatPass : public Pass {
shows.push_back(wire->name.str());
}
log("Using SAT solver `%s`.\n", solver->name.c_str());
if (tempinduct)
{
if (loopcount > 0 || max_undef)
log_cmd_error("The options -max, -all, and -max_undef are not supported for temporal induction proofs!\n");
SatHelper basecase(design, module, enable_undef, set_def_formal);
SatHelper inductstep(design, module, enable_undef, set_def_formal);
SatHelper basecase(design, module, solver, enable_undef, set_def_formal);
SatHelper inductstep(design, module, solver, enable_undef, set_def_formal);
basecase.sets = sets;
basecase.set_assumes = set_assumes;
@ -1593,7 +1625,7 @@ struct SatPass : public Pass {
if (maxsteps > 0)
log_cmd_error("The options -maxsteps is only supported for temporal induction proofs!\n");
SatHelper sathelper(design, module, enable_undef, set_def_formal);
SatHelper sathelper(design, module, solver, enable_undef, set_def_formal);
sathelper.sets = sets;
sathelper.set_assumes = set_assumes;

56
passes/techmap/abc.cc
View file

@ -285,7 +285,7 @@ using AbcSigMap = SigValMap<AbcSigVal>;
struct RunAbcState {
const AbcConfig &config;
std::string tempdir_name;
std::string per_run_tempdir_name;
std::vector<gate_t> signal_list;
bool did_run = false;
bool err = false;
@ -836,16 +836,23 @@ std::string fold_abc_cmd(std::string str)
return new_str;
}
std::string replace_tempdir(std::string text, std::string tempdir_name, bool show_tempdir)
std::string replace_tempdir(std::string text, std::string_view global_tempdir_name, std::string_view per_run_tempdir_name, bool show_tempdir)
{
if (show_tempdir)
return text;
while (1) {
size_t pos = text.find(tempdir_name);
size_t pos = text.find(global_tempdir_name);
if (pos == std::string::npos)
break;
text = text.substr(0, pos) + "<abc-temp-dir>" + text.substr(pos + GetSize(tempdir_name));
text = text.substr(0, pos) + "<abc-temp-dir>" + text.substr(pos + GetSize(global_tempdir_name));
}
while (1) {
size_t pos = text.find(per_run_tempdir_name);
if (pos == std::string::npos)
break;
text = text.substr(0, pos) + "<abc-temp-dir>" + text.substr(pos + GetSize(per_run_tempdir_name));
}
std::string selfdir_name = proc_self_dirname();
@ -867,11 +874,12 @@ struct abc_output_filter
bool got_cr;
int escape_seq_state;
std::string linebuf;
std::string tempdir_name;
std::string global_tempdir_name;
std::string per_run_tempdir_name;
bool show_tempdir;
abc_output_filter(RunAbcState& state, std::string tempdir_name, bool show_tempdir)
: state(state), tempdir_name(tempdir_name), show_tempdir(show_tempdir)
abc_output_filter(RunAbcState& state, std::string global_tempdir_name, std::string per_run_tempdir_name, bool show_tempdir)
: state(state), global_tempdir_name(global_tempdir_name), per_run_tempdir_name(per_run_tempdir_name), show_tempdir(show_tempdir)
{
got_cr = false;
escape_seq_state = 0;
@ -898,7 +906,7 @@ struct abc_output_filter
return;
}
if (ch == '\n') {
state.logs.log("ABC: %s\n", replace_tempdir(linebuf, tempdir_name, show_tempdir));
state.logs.log("ABC: %s\n", replace_tempdir(linebuf, global_tempdir_name, per_run_tempdir_name, show_tempdir));
got_cr = false, linebuf.clear();
return;
}
@ -999,15 +1007,15 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module
const AbcConfig &config = run_abc.config;
if (config.cleanup)
run_abc.tempdir_name = get_base_tmpdir() + "/";
run_abc.per_run_tempdir_name = get_base_tmpdir() + "/";
else
run_abc.tempdir_name = "_tmp_";
run_abc.tempdir_name += proc_program_prefix() + "yosys-abc-XXXXXX";
run_abc.tempdir_name = make_temp_dir(run_abc.tempdir_name);
run_abc.per_run_tempdir_name = "_tmp_";
run_abc.per_run_tempdir_name += proc_program_prefix() + "yosys-abc-XXXXXX";
run_abc.per_run_tempdir_name = make_temp_dir(run_abc.per_run_tempdir_name);
log_header(design, "Extracting gate netlist of module `%s' to `%s/input.blif'..\n",
module->name.c_str(), replace_tempdir(run_abc.tempdir_name, run_abc.tempdir_name, config.show_tempdir).c_str());
module->name.c_str(), replace_tempdir(run_abc.per_run_tempdir_name, config.global_tempdir_name, run_abc.per_run_tempdir_name, config.show_tempdir).c_str());
std::string abc_script = stringf("read_blif \"%s/input.blif\"; ", run_abc.tempdir_name);
std::string abc_script = stringf("read_blif \"%s/input.blif\"; ", run_abc.per_run_tempdir_name);
if (!config.liberty_files.empty() || !config.genlib_files.empty()) {
std::string dont_use_args;
@ -1073,8 +1081,8 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module
for (size_t pos = abc_script.find("{S}"); pos != std::string::npos; pos = abc_script.find("{S}", pos))
abc_script = abc_script.substr(0, pos) + config.lutin_shared + abc_script.substr(pos+3);
if (config.abc_dress)
abc_script += stringf("; dress \"%s/input.blif\"", run_abc.tempdir_name);
abc_script += stringf("; write_blif %s/output.blif", run_abc.tempdir_name);
abc_script += stringf("; dress \"%s/input.blif\"", run_abc.per_run_tempdir_name);
abc_script += stringf("; write_blif %s/output.blif", run_abc.per_run_tempdir_name);
abc_script = add_echos_to_abc_cmd(abc_script);
#if defined(REUSE_YOSYS_ABC_PROCESSES)
if (config.is_yosys_abc())
@ -1085,7 +1093,7 @@ void AbcModuleState::prepare_module(RTLIL::Design *design, RTLIL::Module *module
if (abc_script[i] == ';' && abc_script[i+1] == ' ')
abc_script[i+1] = '\n';
std::string buffer = stringf("%s/abc.script", run_abc.tempdir_name);
std::string buffer = stringf("%s/abc.script", run_abc.per_run_tempdir_name);
FILE *f = fopen(buffer.c_str(), "wt");
if (f == nullptr)
log_error("Opening %s for writing failed: %s\n", buffer, strerror(errno));
@ -1220,7 +1228,7 @@ void RunAbcState::run(ConcurrentStack<AbcProcess> &process_pool)
void RunAbcState::run(ConcurrentStack<AbcProcess> &)
#endif
{
std::string buffer = stringf("%s/input.blif", tempdir_name);
std::string buffer = stringf("%s/input.blif", per_run_tempdir_name);
FILE *f = fopen(buffer.c_str(), "wt");
if (f == nullptr) {
logs.log("Opening %s for writing failed: %s\n", buffer, strerror(errno));
@ -1348,14 +1356,14 @@ void RunAbcState::run(ConcurrentStack<AbcProcess> &)
return;
}
int ret;
std::string tmp_script_name = stringf("%s/abc.script", tempdir_name);
std::string tmp_script_name = stringf("%s/abc.script", per_run_tempdir_name);
do {
logs.log("Running ABC script: %s\n", replace_tempdir(tmp_script_name, tempdir_name, config.show_tempdir));
logs.log("Running ABC script: %s\n", replace_tempdir(tmp_script_name, config.global_tempdir_name, per_run_tempdir_name, config.show_tempdir));
errno = 0;
abc_output_filter filt(*this, tempdir_name, config.show_tempdir);
abc_output_filter filt(*this, config.global_tempdir_name, per_run_tempdir_name, config.show_tempdir);
#ifdef YOSYS_LINK_ABC
string temp_stdouterr_name = stringf("%s/stdouterr.txt", tempdir_name);
string temp_stdouterr_name = stringf("%s/stdouterr.txt", per_run_tempdir_name);
FILE *temp_stdouterr_w = fopen(temp_stdouterr_name.c_str(), "w");
if (temp_stdouterr_w == NULL)
log_error("ABC: cannot open a temporary file for output redirection");
@ -1502,7 +1510,7 @@ void AbcModuleState::extract(AbcSigMap &assign_map, RTLIL::Design *design, RTLIL
return;
}
std::string buffer = stringf("%s/%s", run_abc.tempdir_name, "output.blif");
std::string buffer = stringf("%s/%s", run_abc.per_run_tempdir_name, "output.blif");
std::ifstream ifs;
ifs.open(buffer);
if (ifs.fail())
@ -1789,7 +1797,7 @@ void AbcModuleState::finish()
if (run_abc.config.cleanup)
{
log("Removing temp directory.\n");
remove_directory(run_abc.tempdir_name);
remove_directory(run_abc.per_run_tempdir_name);
}
log_pop();
}

4
passes/techmap/abc9.cc
View file

@ -219,9 +219,7 @@ struct Abc9Pass : public ScriptPass
for (argidx = 1; argidx < args.size(); argidx++) {
std::string arg = args[argidx];
if ((arg == "-exe" || arg == "-script" || arg == "-D" ||
/*arg == "-S" ||*/ arg == "-lut" || arg == "-luts" ||
/*arg == "-box" ||*/ arg == "-W" || arg == "-genlib" ||
arg == "-constr" || arg == "-dont_use" || arg == "-liberty") &&
arg == "-lut" || arg == "-luts" || arg == "-W") &&
argidx+1 < args.size()) {
if (arg == "-lut" || arg == "-luts")
lut_mode = true;

2
passes/techmap/abc9_exe.cc
View file

@ -248,7 +248,7 @@ void abc9_module(RTLIL::Design *design, std::string script_file, std::string exe
}
abc9_script += stringf("; &ps -l; &write -n %s/output.aig", tempdir_name);
if (design->scratchpad_get_bool("abc9.verify")) {
if (design->scratchpad_get_bool("abc9.verify", true)) {
if (dff_mode)
abc9_script += "; &verify -s";
else

113
passes/techmap/abc9_ops.cc
View file

@ -23,6 +23,7 @@
#include "kernel/utils.h"
#include "kernel/celltypes.h"
#include "kernel/timinginfo.h"
#include <optional>
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
@ -587,6 +588,7 @@ void break_scc(RTLIL::Module *module)
auto id = it->second;
auto r = ids_seen.insert(id);
cell->attributes.erase(it);
// Cut exactly one representative cell per SCC id.
if (!r.second)
continue;
for (auto &c : cell->connections_) {
@ -710,8 +712,6 @@ void prep_xaiger(RTLIL::Module *module, bool dff)
SigMap sigmap(module);
dict<SigBit, pool<IdString>> bit_drivers, bit_users;
TopoSort<IdString, RTLIL::sort_by_id_str> toposort;
dict<IdString, std::vector<IdString>> box_ports;
for (auto cell : module->cells()) {
@ -750,39 +750,100 @@ void prep_xaiger(RTLIL::Module *module, bool dff)
}
}
}
else if (!yosys_celltypes.cell_known(cell->type))
continue;
// TODO: Speed up toposort -- we care about box ordering only
for (auto conn : cell->connections()) {
if (cell->input(conn.first))
for (auto bit : sigmap(conn.second))
bit_users[bit].insert(cell->name);
if (cell->output(conn.first) && !abc9_flop)
for (auto bit : sigmap(conn.second))
bit_drivers[bit].insert(cell->name);
}
toposort.node(cell->name);
}
if (box_ports.empty())
return;
for (auto &it : bit_users)
if (bit_drivers.count(it.first))
for (auto driver_cell : bit_drivers.at(it.first))
for (auto user_cell : it.second)
toposort.edge(driver_cell, user_cell);
// Build the same topo graph for the initial pass and the optional retry.
auto build_toposort = [&](TopoSort<IdString, RTLIL::sort_by_id_str> &toposort) {
dict<SigBit, pool<IdString>> bit_drivers, bit_users;
if (ys_debug(1))
toposort.analyze_loops = true;
for (auto cell : module->cells()) {
if (cell->type.in(ID($_DFF_N_), ID($_DFF_P_)))
continue;
if (cell->has_keep_attr())
continue;
bool no_loops = toposort.sort();
auto inst_module = design->module(cell->type);
bool abc9_flop = inst_module && inst_module->get_bool_attribute(ID::abc9_flop);
if (abc9_flop && !dff)
continue;
if (!(inst_module && inst_module->get_bool_attribute(ID::abc9_box)) && !yosys_celltypes.cell_known(cell->type))
continue;
// TODO: Speed up toposort -- we care about box ordering only
for (auto conn : cell->connections()) {
if (cell->input(conn.first))
for (auto bit : sigmap(conn.second))
bit_users[bit].insert(cell->name);
if (cell->output(conn.first) && !abc9_flop)
for (auto bit : sigmap(conn.second))
bit_drivers[bit].insert(cell->name);
}
toposort.node(cell->name);
}
// Build producer -> consumer edges on sigmapped nets.
for (auto &it : bit_users)
if (bit_drivers.count(it.first))
for (auto driver_cell : bit_drivers.at(it.first))
for (auto user_cell : it.second)
toposort.edge(driver_cell, user_cell);
if (ys_debug(1))
toposort.analyze_loops = true;
return toposort.sort();
};
// Build TopoSort in a container, as we may need to conditionally rebuild it on retry.
std::optional<TopoSort<IdString, RTLIL::sort_by_id_str>> toposort;
toposort.emplace();
bool no_loops = build_toposort(toposort.value());
// Fallback for residual loops after SCC cutting: insert additional
// breakers on non-box loop cells, then re-run toposort checks.
if (!no_loops) {
SigSpec I, O;
pool<IdString> broken_cells;
for (auto &loop : toposort.value().loops)
for (auto cell_name : loop) {
// Loop reports can overlap; cut each cell at most once.
if (!broken_cells.insert(cell_name).second)
continue;
auto cell = module->cell(cell_name);
log_assert(cell);
auto inst_module = design->module(cell->type);
if (inst_module && inst_module->get_bool_attribute(ID::abc9_box))
continue;
for (auto &c : cell->connections_) {
if (c.second.is_fully_const()) continue;
if (cell->output(c.first)) {
Wire *w = module->addWire(NEW_ID, GetSize(c.second));
I.append(w);
O.append(c.second);
c.second = w;
}
}
}
if (!I.empty()) {
auto cell = module->addCell(NEW_ID, ID($__ABC9_SCC_BREAKER));
log_assert(GetSize(I) == GetSize(O));
cell->setParam(ID::WIDTH, GetSize(I));
cell->setPort(ID::I, std::move(I));
cell->setPort(ID::O, std::move(O));
// Rebuild topo ordering after inserting the additional breakers.
toposort.emplace();
no_loops = build_toposort(toposort.value());
}
}
if (ys_debug(1)) {
unsigned i = 0;
for (auto &it : toposort.loops) {
for (auto &it : toposort.value().loops) {
log(" loop %d\n", i++);
for (auto cell_name : it) {
auto cell = module->cell(cell_name);
@ -806,7 +867,7 @@ void prep_xaiger(RTLIL::Module *module, bool dff)
TimingInfo timing;
int port_id = 1, box_count = 0;
for (auto cell_name : toposort.sorted) {
for (auto cell_name : toposort.value().sorted) {
RTLIL::Cell *cell = module->cell(cell_name);
log_assert(cell);

1
techlibs/gowin/Makefile.inc
View file

@ -12,3 +12,4 @@ $(eval $(call add_share_file,share/gowin,techlibs/gowin/brams_map_gw5a.v))
$(eval $(call add_share_file,share/gowin,techlibs/gowin/brams.txt))
$(eval $(call add_share_file,share/gowin,techlibs/gowin/lutrams_map.v))
$(eval $(call add_share_file,share/gowin,techlibs/gowin/lutrams.txt))
$(eval $(call add_share_file,share/gowin,techlibs/gowin/dsp_map.v))

2
techlibs/gowin/brams_map.v
View file

@ -205,7 +205,7 @@ 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 [13:0] ADA = `addrbe(PORT_A_WIDTH, PORT_A_ADDR, 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);
generate

2
techlibs/gowin/brams_map_gw5a.v
View file

@ -205,7 +205,7 @@ 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 [13:0] ADA = `addrbe(PORT_A_WIDTH, PORT_A_ADDR, 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);
generate

70
techlibs/gowin/dsp_map.v Normal file
View file

@ -0,0 +1,70 @@
module \$__MUL9X9 (input [8:0] A, input [8:0] B, output [17:0] Y);
parameter A_WIDTH = 9;
parameter B_WIDTH = 9;
parameter Y_WIDTH = 18;
parameter A_SIGNED = 0;
parameter B_SIGNED = 0;
MULT9X9 __TECHMAP_REPLACE__ (
.CLK(1'b0),
.CE(1'b0),
.RESET(1'b0),
.A(A),
.SIA({A_WIDTH{1'b0}}),
.ASEL(1'b0),
.ASIGN(A_SIGNED ? 1'b1 : 1'b0),
.B(B),
.SIB({B_WIDTH{1'b0}}),
.BSEL(1'b0),
.BSIGN(B_SIGNED ? 1'b1 : 1'b0),
.DOUT(Y)
);
endmodule
module \$__MUL18X18 (input [17:0] A, input [17:0] B, output [35:0] Y);
parameter A_WIDTH = 18;
parameter B_WIDTH = 18;
parameter Y_WIDTH = 36;
parameter A_SIGNED = 0;
parameter B_SIGNED = 0;
MULT18X18 __TECHMAP_REPLACE__ (
.CLK(1'b0),
.CE(1'b0),
.RESET(1'b0),
.A(A),
.SIA({A_WIDTH{1'b0}}),
.ASEL(1'b0),
.ASIGN(A_SIGNED ? 1'b1 : 1'b0),
.B(B),
.SIB({B_WIDTH{1'b0}}),
.BSEL(1'b0),
.BSIGN(B_SIGNED ? 1'b1 : 1'b0),
.DOUT(Y)
);
endmodule
module \$__MUL36X36 (input [35:0] A, input [35:0] B, output [71:0] Y);
parameter A_WIDTH = 36;
parameter B_WIDTH = 36;
parameter Y_WIDTH = 72;
parameter A_SIGNED = 0;
parameter B_SIGNED = 0;
MULT36X36 __TECHMAP_REPLACE__ (
.CLK(1'b0),
.RESET(1'b0),
.CE(1'b0),
.A(A),
.ASIGN(A_SIGNED ? 1'b1 : 1'b0),
.B(B),
.BSIGN(B_SIGNED ? 1'b1 : 1'b0),
.DOUT(Y)
);
endmodule

68
techlibs/gowin/synth_gowin.cc
View file

@ -29,6 +29,21 @@ struct SynthGowinPass : public ScriptPass
{
SynthGowinPass() : ScriptPass("synth_gowin", "synthesis for Gowin FPGAs") { }
struct DSPRule {
int a_maxwidth;
int b_maxwidth;
int a_minwidth;
int b_minwidth;
std::string prim;
};
const std::vector<DSPRule> dsp_rules = {
{36, 36, 22, 22, "$__MUL36X36"},
{18, 18, 10, 4, "$__MUL18X18"},
{18, 18, 4, 10, "$__MUL18X18"},
{9, 9, 4, 4, "$__MUL9X9"},
};
void help() override
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
@ -97,13 +112,16 @@ struct SynthGowinPass : public ScriptPass
log(" -setundef\n");
log(" set undriven wires and parameters to zero\n");
log("\n");
log(" -nodsp\n");
log(" do not infer DSP multipliers\n");
log("\n");
log("The following commands are executed by this synthesis command:\n");
help_script();
log("\n");
}
string top_opt, vout_file, json_file, family;
bool retime, nobram, nolutram, flatten, nodffe, strict_gw5a_dffs, nowidelut, abc9, noiopads, noalu, no_rw_check, setundef;
bool retime, nobram, nolutram, flatten, nodffe, strict_gw5a_dffs, nowidelut, abc9, noiopads, noalu, no_rw_check, setundef, nodsp;
void clear_flags() override
{
@ -123,6 +141,7 @@ struct SynthGowinPass : public ScriptPass
noalu = false;
no_rw_check = false;
setundef = false;
nodsp = false;
}
void execute(std::vector<std::string> args, RTLIL::Design *design) override
@ -209,6 +228,10 @@ struct SynthGowinPass : public ScriptPass
setundef = true;
continue;
}
if (args[argidx] == "-nodsp") {
nodsp = true;
continue;
}
break;
}
extra_args(args, argidx, design);
@ -239,17 +262,40 @@ struct SynthGowinPass : public ScriptPass
run(stringf("hierarchy -check %s", help_mode ? "-top <top>" : top_opt));
}
if (flatten && check_label("flatten", "(unless -noflatten)"))
{
run("proc");
run("flatten");
run("tribuf -logic");
run("deminout");
}
if (check_label("coarse"))
{
run("synth -run coarse" + no_rw_check_opt);
run("proc");
if (flatten || help_mode)
run("flatten", "(unless -noflatten)");
run("tribuf -logic");
run("deminout");
run("opt_expr");
run("opt_clean");
run("check");
run("opt -nodffe -nosdff");
run("fsm");
run("opt");
run("wreduce");
run("peepopt");
run("opt_clean");
run("share");
if (help_mode) {
run("techmap -map +/mul2dsp.v [...]", "(unless -nodsp and if -family gw1n or gw2a)");
run("techmap -map +/gowin/dsp_map.v", "(unless -nodsp and if -family gw1n or gw2a)");
} else if (!nodsp && (family == "gw1n" || family == "gw2a")) {
for (const auto &rule : dsp_rules) {
run(stringf("techmap -map +/mul2dsp.v -D DSP_A_MAXWIDTH=%d -D DSP_B_MAXWIDTH=%d -D DSP_A_MINWIDTH=%d -D DSP_B_MINWIDTH=%d -D DSP_NAME=%s",
rule.a_maxwidth, rule.b_maxwidth, rule.a_minwidth, rule.b_minwidth, rule.prim));
run("chtype -set $mul t:$__soft_mul");
}
run("techmap -map +/gowin/dsp_map.v");
}
run("alumacc");
run("opt");
run("memory -nomap" + no_rw_check_opt);
run("opt_clean");
}
if (check_label("map_ram"))
@ -263,7 +309,7 @@ struct SynthGowinPass : public ScriptPass
if (nolutram)
args += " -no-auto-distributed";
}
run(stringf("memory_libmap -lib +/gowin/lutrams.txt -lib +/gowin/brams.txt -D %s", family) + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)");
run(stringf("memory_libmap -lib +/gowin/lutrams.txt -lib +/gowin/brams.txt%s", family == "gw5a" ? " -D gw5a" : "") + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)");
run(stringf("techmap -map +/gowin/lutrams_map.v -map +/gowin/brams_map%s.v", family == "gw5a" ? "_gw5a" : ""));
}

20
techlibs/xilinx/xilinx_dsp.cc
View file

@ -263,6 +263,7 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm)
log("Analysing %s.%s for Xilinx DSP packing.\n", log_id(pm.module), log_id(st.dsp));
log_debug("preAdd: %s\n", log_id(st.preAdd, "--"));
log_debug("preSub: %s\n", log_id(st.preSub, "--"));
log_debug("ffAD: %s\n", log_id(st.ffAD, "--"));
log_debug("ffA2: %s\n", log_id(st.ffA2, "--"));
log_debug("ffA1: %s\n", log_id(st.ffA1, "--"));
@ -278,17 +279,22 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm)
Cell *cell = st.dsp;
if (st.preAdd) {
log(" preadder %s (%s)\n", log_id(st.preAdd), log_id(st.preAdd->type));
bool A_SIGNED = st.preAdd->getParam(ID::A_SIGNED).as_bool();
bool D_SIGNED = st.preAdd->getParam(ID::B_SIGNED).as_bool();
if (st.sigA == st.preAdd->getPort(ID::B))
if (st.preAdd || st.preSub) {
Cell* preAdder = st.preAdd ? st.preAdd : st.preSub;
log(" preadder %s (%s)\n", log_id(preAdder), log_id(preAdder->type));
bool A_SIGNED = preAdder->getParam(ID::A_SIGNED).as_bool();
bool D_SIGNED = preAdder->getParam(ID::B_SIGNED).as_bool();
if (st.sigA == preAdder->getPort(ID::B))
std::swap(A_SIGNED, D_SIGNED);
st.sigA.extend_u0(30, A_SIGNED);
st.sigD.extend_u0(25, D_SIGNED);
cell->setPort(ID::A, st.sigA);
cell->setPort(ID::D, st.sigD);
cell->setPort(ID(INMODE), Const::from_string("00100"));
if (preAdder->type == ID($add))
cell->setPort(ID(INMODE), Const::from_string("00100"));
else
cell->setPort(ID(INMODE), Const::from_string("01100"));
if (st.ffAD) {
if (st.ffAD->type.in(ID($dffe), ID($sdffe))) {
@ -303,7 +309,7 @@ void xilinx_dsp_pack(xilinx_dsp_pm &pm)
cell->setParam(ID(USE_DPORT), Const("TRUE"));
pm.autoremove(st.preAdd);
pm.autoremove(preAdder);
}
if (st.postAdd) {
log(" postadder %s (%s)\n", log_id(st.postAdd), log_id(st.postAdd->type));

32
techlibs/xilinx/xilinx_dsp.pmg
View file

@ -6,6 +6,8 @@
// If ADREG matched, treat 'A' input as input of ADREG
// ( 3) Match the driver of the 'A' and 'D' inputs for a possible $add cell
// (pre-adder)
// (3.1) Match the driver of the 'A' and 'D' inputs for a possible $sub cell
// (pre-adder)
// ( 4) If pre-adder was present, find match 'A' input for A2REG
// If pre-adder was not present, move ADREG to A2REG
// If A2REG, then match 'A' input for A1REG
@ -152,13 +154,41 @@ code sigA sigD
}
endcode
// (3.1) Match the driver of the 'A' and 'D' inputs for a possible $sub cell
// (pre-adder)
match preSub
if sigD.empty() || sigD.is_fully_zero()
// Ensure that preAdder not already used
if param(dsp, \USE_DPORT).decode_string() == "FALSE"
if port(dsp, \INMODE, Const(0, 5)).is_fully_zero()
select preSub->type.in($sub)
// Output has to be 25 bits or less
select GetSize(port(preSub, \Y)) <= 25
select nusers(port(preSub, \Y)) == 2
// D port has to be 25 bits or less
select GetSize(port(preSub, \A)) <= 25
// A port has to be 30 bits or less
select GetSize(port(preSub, \B)) <= 30
index <SigSpec> port(preSub, \Y) === sigA
optional
endmatch
code sigA sigD
if (preSub) {
sigD = port(preSub, \A);
sigA = port(preSub, \B);
}
endcode
// (4) If pre-adder was present, find match 'A' input for A2REG
// If pre-adder was not present, move ADREG to A2REG
// Then match 'A' input for A1REG
code argQ ffAD sigA clock ffA2 ffA1
// Only search for ffA2 if there was a pre-adder
// (otherwise ffA2 would have been matched as ffAD)
if (preAdd) {
if (preAdd || preSub) {
if (param(dsp, \AREG).as_int() == 0) {
argQ = sigA;
subpattern(in_dffe);

31
tests/arch/gowin/bug5688.ys Normal file
View file

@ -0,0 +1,31 @@
read_verilog << EOT
`default_nettype none
module top (
input wire clk,
input wire [9:0] rd_addr,
output reg [15:0] rd_data,
input wire [9:0] wr_addr,
input wire [15:0] wr_data,
input wire wr_en
);
(* ram_style = "block" *) reg [15:0] mem [0:1023];
// Read port — separate always block
always @(posedge clk) begin
rd_data <= mem[rd_addr];
end
// Write port — separate always block
always @(posedge clk) begin
if (wr_en)
mem[wr_addr] <= wr_data;
end
endmodule
EOT
synth_gowin -top top
splitnets
select -assert-any top/mem.0.0 %ci*:+DPX9B[ADA]:+DFF:+IBUF i:wr_en %i

53
tests/arch/gowin/mul_gw1n.ys Normal file
View file

@ -0,0 +1,53 @@
read_verilog ../common/mul.v
chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
hierarchy -top top
proc
# equivalence checking is somewhat slow (and missing simulation models)
synth_gowin -family gw1n
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:MULT9X9
# Make sure that DSPs are not inferred with -nodsp option
design -reset
read_verilog ../common/mul.v
chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
hierarchy -top top
proc
synth_gowin -family gw1n -nodsp
cd top # Constrain all select calls below inside the top module
select -assert-none t:MULT9X9
design -reset
read_verilog ../common/mul.v
chparam -set X_WIDTH 16 -set Y_WIDTH 16 -set A_WIDTH 32
hierarchy -top top
proc
synth_gowin -family gw1n
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:MULT18X18
design -reset
read_verilog ../common/mul.v
chparam -set X_WIDTH 32 -set Y_WIDTH 32 -set A_WIDTH 64
hierarchy -top top
proc
# equivalence checking is too slow here
synth_gowin
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:MULT36X36
# We end up with two 18x18 multipliers
# 36x36 min width is 22
design -reset
read_verilog ../common/mul.v
chparam -set X_WIDTH 32 -set Y_WIDTH 16 -set A_WIDTH 48
hierarchy -top top
proc
# equivalence checking is too slow here
synth_gowin
cd top # Constrain all select calls below inside the top module
select -assert-count 2 t:MULT18X18

53
tests/arch/gowin/mul_gw2a.ys Normal file
View file

@ -0,0 +1,53 @@
read_verilog ../common/mul.v
chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
hierarchy -top top
proc
# equivalence checking is somewhat slow (and missing simulation models)
synth_gowin -family gw2a
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:MULT9X9
# Make sure that DSPs are not inferred with -nodsp option
design -reset
read_verilog ../common/mul.v
chparam -set X_WIDTH 8 -set Y_WIDTH 8 -set A_WIDTH 16
hierarchy -top top
proc
synth_gowin -family gw2a -nodsp
cd top # Constrain all select calls below inside the top module
select -assert-none t:MULT9X9
design -reset
read_verilog ../common/mul.v
chparam -set X_WIDTH 16 -set Y_WIDTH 16 -set A_WIDTH 32
hierarchy -top top
proc
synth_gowin -family gw2a
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:MULT18X18
design -reset
read_verilog ../common/mul.v
chparam -set X_WIDTH 32 -set Y_WIDTH 32 -set A_WIDTH 64
hierarchy -top top
proc
# equivalence checking is too slow here
synth_gowin -family gw2a
cd top # Constrain all select calls below inside the top module
select -assert-count 1 t:MULT36X36
# We end up with two 18x18 multipliers
# 36x36 min width is 22
design -reset
read_verilog ../common/mul.v
chparam -set X_WIDTH 32 -set Y_WIDTH 16 -set A_WIDTH 48
hierarchy -top top
proc
# equivalence checking is too slow here
synth_gowin -family gw2a
cd top # Constrain all select calls below inside the top module
select -assert-count 2 t:MULT18X18

2
tests/arch/ice40/fsm.ys
View file

@ -12,5 +12,5 @@ cd fsm # Constrain all select calls below inside the top module
select -assert-count 4 t:SB_DFF
select -assert-count 2 t:SB_DFFESR
select -assert-max 15 t:SB_LUT4
select -assert-max 16 t:SB_LUT4
select -assert-none t:SB_DFFESR t:SB_DFF t:SB_LUT4 %% t:* %D

1
tests/arch/ice40/ice40_dsp_const.ys
View file

@ -74,6 +74,7 @@ EOT
techmap -wb -D EQUIV -autoproc -map +/ice40/cells_sim.v
async2sync
equiv_make top ref equiv
select -assert-any -module equiv t:$equiv
equiv_induct

29
tests/arch/xilinx/dsp_preadder_sub.ys Normal file
View file

@ -0,0 +1,29 @@
read_verilog <<EOT
module top(
input signed [7:0] A,
input signed [7:0] D,
input signed [7:0] B,
output signed [16:0] P
);
assign P = (A - D) * B;
endmodule
EOT
proc
design -save gold
synth_xilinx -noiopad
design -save gate
cd top
select -assert-count 1 t:DSP48E1
select -assert-count 1 t:DSP48E1 r:USE_DPORT=TRUE %i
select -assert-none t:DSP48E1 %% t:* %D
# Now prove functional equivalence of the mapped netlist against the original
# (saved as `gold` above).
design -reset
design -copy-from gold -as gold top
design -copy-from gate -as gate top
techmap -wb -D EQUIV -autoproc -map +/xilinx/cells_sim.v
equiv_make gold gate equiv
equiv_induct equiv
equiv_status -assert equiv

2
tests/opt/opt_hier.tcl
View file

@ -27,7 +27,7 @@ foreach fn [glob opt_hier_*.v] {
design -copy-from gate -as gate A:top
yosys rename -hide
equiv_make gold gate equiv
equiv_induct equiv
equiv_induct -ignore-unknown-cells equiv
equiv_status -assert equiv
log -pop

19
tests/techmap/abc9-nonbox-loop-with-box.ys Normal file
View file

@ -0,0 +1,19 @@
read_verilog -icells -specify <<EOT
(* abc9_box, blackbox *)
module box1(input i, output o);
specify
(i => o) = 1;
endspecify
endmodule
module top(input i, output o);
wire a, b, c, z;
$_AND_ a0(.A(b), .B(i), .Y(a));
$_AND_ b0(.A(a), .B(c), .Y(b));
$_AND_ c0(.A(b), .B(i), .Y(c));
box1 u_box(.i(i), .o(z));
assign o = c ^ z;
endmodule
EOT
abc9 -lut 4

13
tests/techmap/abc_temp_dir_sanitization.ys Normal file
View file

@ -0,0 +1,13 @@
read_verilog <<EOT
module simple(I1, I2, O);
input wire I1;
input wire I2;
output wire O;
assign O = I1 | I2;
endmodule
EOT
techmap
logger -warn " /tmp/" -werror " /tmp/"
abc -g all

9
tests/unit/Makefile
View file

@ -18,10 +18,11 @@ endif
EXTRAFLAGS := -lyosys -pthread
OBJTEST := objtest
BINTEST := bintest
MAKEFILE_DIR := $(dir $(abspath $(lastword $(MAKEFILE_LIST))))
OBJTEST := $(MAKEFILE_DIR)objtest
BINTEST := $(MAKEFILE_DIR)bintest
ALLTESTFILE := $(shell find . -name '*Test.cc' | sed 's|^\./||' | tr '\n' ' ')
ALLTESTFILE := $(shell cd $(MAKEFILE_DIR) && find . -name '*Test.cc' | sed 's|^\./||' | tr '\n' ' ')
TESTDIRS := $(sort $(dir $(ALLTESTFILE)))
TESTS := $(addprefix $(BINTEST)/, $(basename $(ALLTESTFILE:%Test.cc=%Test.o)))
@ -34,7 +35,7 @@ $(BINTEST)/%: $(OBJTEST)/%.o | prepare
$(CXX) -L$(ROOTPATH) $(RPATH) $(LINKFLAGS) -o $@ $^ $(LIBS) \
$(GTEST_LDFLAGS) $(EXTRAFLAGS)
$(OBJTEST)/%.o: $(basename $(subst $(OBJTEST),.,%)).cc | prepare
$(OBJTEST)/%.o: $(MAKEFILE_DIR)/%.cc | prepare
$(CXX) -o $@ -c -I$(ROOTPATH) $(CPPFLAGS) $(CXXFLAGS) $(GTEST_CXXFLAGS) $^
.PHONY: prepare run-tests clean

47
tests/unit/kernel/modindexTest.cc Normal file
View file

@ -0,0 +1,47 @@
#include <gtest/gtest.h>
#include "kernel/modtools.h"
#include "kernel/rtlil.h"
YOSYS_NAMESPACE_BEGIN
TEST(ModIndexSwapTest, has)
{
Design* d = new Design;
Module* m = d->addModule("$m");
Wire* o = m->addWire("$o", 2);
o->port_input = true;
Wire* i = m->addWire("$i", 2);
i->port_input = true;
m->fixup_ports();
m->addNot("$not", i, o);
auto mi = ModIndex(m);
mi.reload_module();
for (auto [sb, info] : mi.database) {
EXPECT_TRUE(mi.database.find(sb) != mi.database.end());
}
m->swap_names(i, o);
for (auto [sb, info] : mi.database) {
EXPECT_TRUE(mi.database.find(sb) != mi.database.end());
}
}
TEST(ModIndexDeleteTest, has)
{
if (log_files.empty()) log_files.emplace_back(stdout);
Design* d = new Design;
Module* m = d->addModule("$m");
Wire* w = m->addWire("$w");
Wire* o = m->addWire("$o");
o->port_output = true;
m->fixup_ports();
Cell* not_ = m->addNotGate("$not", w, o);
auto mi = ModIndex(m);
mi.reload_module();
mi.dump_db();
Wire* a = m->addWire("\\a");
not_->setPort(ID::A, a);
EXPECT_TRUE(mi.ok());
}
YOSYS_NAMESPACE_END

2
tests/various/.gitignore vendored
View file

@ -4,6 +4,8 @@
/plugin.so
/plugin_search
/plugin.so.dSYM
/ezcmdline_plugin.so
/ezcmdline_plugin.so.dSYM
/temp
/smtlib2_module.smt2
/smtlib2_module-filtered.smt2

49
tests/various/const_shift_empty_arg.ys Normal file
View file

@ -0,0 +1,49 @@
# Regression test for #5684: const_shift_worker must not crash when arg1 is
# empty.
read_json << EOF
{
"modules": {
"sshl": {
"cells": {
"sshlCell": {
"connections": {
"A": [],
"B": [3],
"Y": [1]
},
"parameters": {
"A_SIGNED": "1",
"A_WIDTH": "0",
"B_SIGNED": "0",
"B_WIDTH": "1",
"Y_WIDTH": "1"
},
"port_directions": {
"A": "input",
"B": "input",
"Y": "output"
},
"type": "$sshl"
}
},
"ports": {
"A": {
"bits": [],
"direction": "input"
},
"B": {
"bits": [3],
"direction": "input"
},
"Y": {
"bits": [1],
"direction": "output"
}
}
}
}
}
EOF
eval -set B 0 -show Y sshl

61
tests/various/ezcmdline_dummy_solver Executable file
View file

@ -0,0 +1,61 @@
#!/bin/sh
# Dummy SAT solver for ezCmdlineSAT tests.
# Accepts exactly two CNF shapes:
# - SAT: p cnf 1 1; clause: "1 0" -> exits 10 with v 1
# - UNSAT: p cnf 1 2; clauses: "1 0" and "-1 0" -> exits 20
set -e
if [ "$#" -ne 1 ]; then
echo "usage: $0 <cnf>" >&2
exit 1
fi
awk '
BEGIN {
vars = 0;
clauses = 0;
clause_count = 0;
clause_data = "";
current = "";
}
$1 == "c" {
next;
}
$1 == "p" && $2 == "cnf" {
vars = $3;
clauses = $4;
next;
}
{
for (i = 1; i <= NF; i++) {
lit = $i;
if (lit == 0) {
clause_count++;
if (clause_data != "")
clause_data = clause_data ";" current;
else
clause_data = current;
current = "";
} else {
if (current == "")
current = lit;
else
current = current "," lit;
}
}
}
END {
if (vars == 1 && clause_count == 1 && clause_data == "1") {
print "s SATISFIABLE";
print "v 1 0";
exit 10;
}
if (vars == 1 && clause_count == 2 && clause_data == "1;-1") {
print "s UNSATISFIABLE";
exit 20;
}
print "c unexpected CNF for dummy solver";
print "c vars=" vars " header_clauses=" clauses " parsed_clauses=" clause_count " data=" clause_data;
exit 1;
}
' "$1"

53
tests/various/ezcmdline_plugin.cc Normal file
View file

@ -0,0 +1,53 @@
#include "kernel/yosys.h"
#include "libs/ezsat/ezcmdline.h"
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
struct EzCmdlineTestPass : public Pass {
EzCmdlineTestPass() : Pass("ezcmdline_test", "smoke-test ezCmdlineSAT") { }
void execute(std::vector<std::string> args, RTLIL::Design *design) override
{
std::string cmd;
size_t argidx = 1;
while (argidx < args.size()) {
if (args[argidx] == "-cmd" && argidx + 1 < args.size()) {
cmd = args[argidx + 1];
argidx += 2;
continue;
}
break;
}
extra_args(args, argidx, design);
if (cmd.empty())
log_error("Missing -cmd <solver> argument.\n");
ezCmdlineSAT sat(cmd);
sat.non_incremental();
// assume("A") adds a permanent CNF clause "A".
sat.assume(sat.VAR("A"));
std::vector<int> model_expressions;
std::vector<bool> model_values;
model_expressions.push_back(sat.VAR("A"));
// Expect SAT with A=true.
if (!sat.solve(model_expressions, model_values))
log_error("ezCmdlineSAT SAT case failed.\n");
if (model_values.size() != 1 || !model_values[0])
log_error("ezCmdlineSAT SAT model mismatch.\n");
// Passing NOT("A") here adds a temporary unit clause for this solve call,
// so the solver sees A && !A and must return UNSAT.
if (sat.solve(model_expressions, model_values, sat.NOT("A")))
log_error("ezCmdlineSAT UNSAT case failed.\n");
log("ezcmdline_test passed!\n");
}
} EzCmdlineTestPass;
PRIVATE_NAMESPACE_END

12
tests/various/ezcmdline_plugin.sh Normal file
View file

@ -0,0 +1,12 @@
set -e
DIR=$(cd "$(dirname "$0")" && pwd)
BASEDIR=$(cd "$DIR/../.." && pwd)
rm -f "$DIR/ezcmdline_plugin.so"
chmod +x "$DIR/ezcmdline_dummy_solver"
CXXFLAGS=$("$BASEDIR/yosys-config" --cxxflags)
DATDIR=$("$BASEDIR/yosys-config" --datdir)
DATDIR=${DATDIR//\//\\\/}
CXXFLAGS=${CXXFLAGS//$DATDIR/..\/..\/share}
"$BASEDIR/yosys-config" --exec --cxx ${CXXFLAGS} -I"$BASEDIR" --ldflags -shared -o "$DIR/ezcmdline_plugin.so" "$DIR/ezcmdline_plugin.cc"
"$BASEDIR/yosys" -m "$DIR/ezcmdline_plugin.so" -p "ezcmdline_test -cmd $DIR/ezcmdline_dummy_solver" | grep -q "ezcmdline_test passed!"

10
tests/various/json_param_defaults.v Normal file
View file

@ -0,0 +1,10 @@
module json_param_defaults #(
parameter WIDTH = 8,
parameter SIGNED = 1
) (
input [WIDTH-1:0] a,
output [WIDTH-1:0] y
);
wire [WIDTH-1:0] y_int = a << SIGNED;
assign y = y_int;
endmodule

8
tests/various/json_param_defaults.ys Normal file
View file

@ -0,0 +1,8 @@
! mkdir -p temp
read_verilog -sv json_param_defaults.v
write_json temp/json_param_defaults.json
design -reset
read_json temp/json_param_defaults.json
write_verilog -noattr -defaultparams temp/json_param_defaults.v
! grep -qF "parameter WIDTH = 32'd8" temp/json_param_defaults.v
! grep -qF "parameter SIGNED = 32'd1" temp/json_param_defaults.v

4
tests/various/specify.ys
View file

@ -43,7 +43,7 @@ select n:C_* -assert-count 2
equiv_make gold gate equiv
hierarchy -top equiv
equiv_struct
equiv_induct -seq 5
equiv_induct -ignore-unknown-cells -seq 5
equiv_status -assert
design -reset
@ -57,7 +57,7 @@ select n:B_* -assert-count 2
equiv_make gold gate equiv
hierarchy -top equiv
equiv_struct
equiv_induct -seq 5
equiv_induct -ignore-unknown-cells -seq 5
equiv_status -assert
design -reset

104
tests/verilog/automatic_lifetime.ys Normal file
View file

@ -0,0 +1,104 @@
# Automatic reg as intermediate value in always @(*)
# The result must be provably equivalent to the direct expression.
# No latch or DFF must be created for tmp.
design -reset
read_verilog -sv <<EOF
module t1(input a, b, c, output reg y);
always @(*) begin : blk
automatic reg tmp;
tmp = a ^ b;
if (c) tmp = tmp & a;
y = tmp;
end
// equivalent to: y = c ? ((a^b)&a) : (a^b)
assert property (y === (c ? ((a ^ b) & a) : (a ^ b)));
endmodule
EOF
proc
async2sync
# no state elements for tmp
select -assert-none t:$dff t:$dlatch %%
sat -verify -prove-asserts -show-all
# automatic logic in always_comb with chained computation
# Two automatic intermediates used in sequence; result must match
# the direct expression. No latch/DFF.
design -reset
read_verilog -sv <<EOF
module t2(input [3:0] a, b, input sel, output reg [3:0] y, output reg co);
always_comb begin : blk
automatic reg [4:0] sum;
automatic reg [3:0] pick;
sum = {1'b0, a} + {1'b0, b};
pick = sel ? sum[3:0] : (a & b);
y = pick;
co = sum[4];
end
assert property (y === (sel ? ((a + b) & 4'hf) : (a & b)));
assert property (co === (((5'(a) + 5'(b)) >> 4) & 1'b1));
endmodule
EOF
proc
async2sync
select -assert-none t:$dff t:$dlatch %%
sat -verify -prove-asserts -show-all
# automatic in a clocked block — only the explicitly registered
# output (result) must get a DFF; the automatic temp must not.
design -reset
read_verilog -sv <<EOF
module t3(input clk, rst, input [7:0] data, output reg [7:0] result);
always @(posedge clk) begin : compute
automatic reg [7:0] tmp;
tmp = data ^ 8'hA5;
if (rst)
result <= 8'h00;
else
result <= tmp;
end
endmodule
EOF
proc
# Exactly one DFF (for result), zero latches, no DFF for tmp
select -assert-count 1 t:$dff %%
select -assert-none t:$dlatch %%
# automatic integer in named block — ensure integer-width
# automatic variables work and produce no state elements.
design -reset
read_verilog -sv <<EOF
module t4(input [7:0] a, b, input sub, output reg [7:0] y);
always @(*) begin : arith
automatic integer acc;
if (sub)
acc = $signed(a) - $signed(b);
else
acc = $signed(a) + $signed(b);
y = acc[7:0];
end
assert property (y === (sub ? (a - b) : (a + b)));
endmodule
EOF
proc
async2sync
select -assert-none t:$dff t:$dlatch %%
sat -verify -prove-asserts -show-all
# automatic variable not assigned on all paths (X semantics)
# With 'automatic', tmp holds no previous state; the undriven path
# produces X, not the old register value. After proc, no latch may be
# inferred for tmp.
design -reset
read_verilog -sv <<EOF
module t5(input en, d, output reg q);
always @(*) begin : blk
automatic reg tmp;
if (en) tmp = d;
// tmp is X when en==0: automatic means no state retention
q = tmp;
end
endmodule
EOF
proc
# No latch for tmp — X propagates instead of old value
select -assert-none t:$dff t:$dlatch %%