mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2026-06-27 02:58:48 +00:00
Code Activity

Merge pull request #20 from YosysHQ/main

Browse source 
bump fork for version 0.41
This commit is contained in:
Eder Monteiro 2024-05-09 13:05:58 +00:00 • committed by GitHub
commit a883985812
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
49 changed files with 1348 additions and 345 deletions
Download patch file Download diff file Expand all files Collapse all files

5
.github/PULL_REQUEST_TEMPLATE.md vendored Normal file
View file

@ -0,0 +1,5 @@
_What are the reasons/motivation for this change?_
_Explain how this is achieved._
_If applicable, please suggest to reviewers how they can test the change._

3
.github/workflows/codeql.yml vendored
View file

@ -15,7 +15,8 @@ jobs:
- name: Checkout repository
uses: actions/checkout@v4
with:
submodules: true
- name: Initialize CodeQL
uses: github/codeql-action/init@v3
with:

18
.github/workflows/emcc.yml vendored
View file

@ -1,18 +0,0 @@
name: Emscripten Build
on: [push, pull_request]
jobs:
emcc:
runs-on: ubuntu-latest
steps:
- uses: mymindstorm/setup-emsdk@v14
- uses: actions/checkout@v4
- name: Build
run: |
make config-emcc
make YOSYS_VER=latest
- uses: actions/upload-artifact@v4
with:
name: yosysjs
path: yosysjs-latest.zip

83
.github/workflows/extra-builds.yml vendored Normal file
View file

@ -0,0 +1,83 @@
name: Test extra build flows
on: [push, pull_request]
jobs:
pre_job:
runs-on: ubuntu-latest
outputs:
should_skip: ${{ steps.skip_check.outputs.should_skip }}
steps:
- id: skip_check
uses: fkirc/skip-duplicate-actions@v5
with:
paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]'
# cancel previous builds if a new commit is pushed
cancel_others: 'true'
# only run on push *or* pull_request, not both
concurrent_skipping: 'same_content_newer'
vs-prep:
name: Prepare Visual Studio build
runs-on: ubuntu-latest
needs: [pre_job]
if: needs.pre_job.outputs.should_skip != 'true'
steps:
- uses: actions/checkout@v4
with:
submodules: true
- name: Build
run: make vcxsrc YOSYS_VER=latest
- uses: actions/upload-artifact@v4
with:
name: vcxsrc
path: yosys-win32-vcxsrc-latest.zip
vs-build:
name: Visual Studio build
runs-on: windows-2019
needs: [vs-prep, pre_job]
if: needs.pre_job.outputs.should_skip != 'true'
steps:
- uses: actions/download-artifact@v4
with:
name: vcxsrc
path: .
- name: unzip
run: unzip yosys-win32-vcxsrc-latest.zip
- name: setup-msbuild
uses: microsoft/setup-msbuild@v2
- name: MSBuild
working-directory: yosys-win32-vcxsrc-latest
run: msbuild YosysVS.sln /p:PlatformToolset=v142 /p:Configuration=Release /p:WindowsTargetPlatformVersion=10.0.17763.0
wasi-build:
name: WASI build
needs: pre_job
if: needs.pre_job.outputs.should_skip != 'true'
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
with:
submodules: true
- name: Build
run: |
WASI_SDK=wasi-sdk-19.0
WASI_SDK_URL=https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-19/wasi-sdk-19.0-linux.tar.gz
if ! [ -d ${WASI_SDK} ]; then curl -L ${WASI_SDK_URL} | tar xzf -; fi
mkdir -p build
cat > build/Makefile.conf <<END
export PATH := $(pwd)/${WASI_SDK}/bin:${PATH}
WASI_SYSROOT := $(pwd)/${WASI_SDK}/share/wasi-sysroot
CONFIG := wasi
PREFIX := /
ENABLE_TCL := 0
ENABLE_READLINE := 0
ENABLE_PLUGINS := 0
ENABLE_ZLIB := 0
END
make -C build -f ../Makefile CXX=clang -j$(nproc)

20
.github/workflows/test-docs.yml vendored
View file

@ -6,7 +6,22 @@ on:
- main
jobs:
pre_job:
runs-on: ubuntu-latest
outputs:
should_skip: ${{ steps.skip_check.outputs.should_skip }}
steps:
- id: skip_check
uses: fkirc/skip-duplicate-actions@v5
with:
# cancel previous builds if a new commit is pushed
cancel_others: 'true'
# only run on push *or* pull_request, not both
concurrent_skipping: 'same_content_newer'
test-docs:
needs: pre_job
if: needs.pre_job.outputs.should_skip != 'true'
runs-on: ubuntu-latest
steps:
- name: Install Dependencies
@ -28,8 +43,9 @@ jobs:
echo "procs=$(nproc)" >> $GITHUB_ENV
- name: Checkout Yosys
uses: actions/checkout@v3
uses: actions/checkout@v4
with:
submodules: true
- name: Build yosys
shell: bash
run: |

19
.github/workflows/test-linux.yml vendored
View file

@ -3,7 +3,23 @@ name: Build and run tests (Linux)
on: [push, pull_request]
jobs:
pre_job:
runs-on: ubuntu-latest
outputs:
should_skip: ${{ steps.skip_check.outputs.should_skip }}
steps:
- id: skip_check
uses: fkirc/skip-duplicate-actions@v5
with:
paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]'
# cancel previous builds if a new commit is pushed
cancel_others: 'true'
# only run on push *or* pull_request, not both
concurrent_skipping: 'same_content_newer'
test-linux:
needs: pre_job
if: needs.pre_job.outputs.should_skip != 'true'
runs-on: ${{ matrix.os.id }}
strategy:
matrix:
@ -80,7 +96,8 @@ jobs:
- name: Checkout Yosys
uses: actions/checkout@v4
with:
submodules: true
- name: Get iverilog
shell: bash
run: |

19
.github/workflows/test-macos.yml vendored
View file

@ -3,7 +3,23 @@ name: Build and run tests (macOS)
on: [push, pull_request]
jobs:
pre_job:
runs-on: ubuntu-latest
outputs:
should_skip: ${{ steps.skip_check.outputs.should_skip }}
steps:
- id: skip_check
uses: fkirc/skip-duplicate-actions@v5
with:
paths_ignore: '["**/README.md", "docs/**", "guidelines/**"]'
# cancel previous builds if a new commit is pushed
cancel_others: 'true'
# only run on push *or* pull_request, not both
concurrent_skipping: 'same_content_newer'
test-macos:
needs: pre_job
if: needs.pre_job.outputs.should_skip != 'true'
runs-on: ${{ matrix.os.id }}
strategy:
matrix:
@ -36,7 +52,8 @@ jobs:
- name: Checkout Yosys
uses: actions/checkout@v4
with:
submodules: true
- name: Get iverilog
shell: bash
run: |

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

@ -0,0 +1,95 @@
name: Build and run tests with Verific (Linux)
on: [push, pull_request]
jobs:
pre_job:
runs-on: ubuntu-latest
outputs:
should_skip: ${{ steps.skip_check.outputs.should_skip }}
steps:
- id: skip_check
uses: fkirc/skip-duplicate-actions@v5
with:
paths_ignore: '["**/README.md"]'
# don't cancel previous builds
cancel_others: 'true'
# only run on push *or* pull_request, not both
concurrent_skipping: 'same_content_newer'
# we have special actions when running on main, so this should be off
skip_after_successful_duplicate: 'false'
test-verific:
needs: pre_job
if: needs.pre_job.outputs.should_skip != 'true'
runs-on: [self-hosted, linux, x64]
steps:
- name: Checkout Yosys
uses: actions/checkout@v4
with:
persist-credentials: false
submodules: true
- name: Runtime environment
run: |
echo "procs=$(nproc)" >> $GITHUB_ENV
- name: Build Yosys
run: |
make config-clang
echo "ENABLE_VERIFIC := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_EDIF := 1" >> Makefile.conf
echo "ENABLE_VERIFIC_LIBERTY := 1" >> Makefile.conf
echo "ENABLE_CCACHE := 1" >> Makefile.conf
make -j${{ env.procs }}
- name: Install Yosys
run: |
make install DESTDIR=${GITHUB_WORKSPACE}/.local PREFIX=
- name: Checkout Documentation
if: ${{ github.ref == 'refs/heads/main' }}
uses: actions/checkout@v4
with:
path: 'yosys-cmd-ref'
repository: 'YosysHQ-Docs/yosys-cmd-ref'
fetch-depth: 0
token: ${{ secrets.CI_DOCS_UPDATE_PAT }}
persist-credentials: true
- name: Update documentation
if: ${{ github.ref == 'refs/heads/main' }}
run: |
make docs
rm -rf docs/build
cd yosys-cmd-ref
rm -rf *
git checkout README.md
cp -R ../docs/* .
rm -rf util/__pycache__
git add -A .
git diff-index --quiet HEAD || git commit -m "Update"
git push
- name: Checkout SBY
uses: actions/checkout@v4
with:
repository: 'YosysHQ/sby'
path: 'sby'
- name: Build SBY
run: |
make -C sby install DESTDIR=${GITHUB_WORKSPACE}/.local PREFIX=
- name: Run Yosys tests
run: |
make -j${{ env.procs }} test
- name: Run Verific specific Yosys tests
run: |
make -C tests/sva
cd tests/svtypes && bash run-test.sh
- name: Run SBY tests
if: ${{ github.ref == 'refs/heads/main' }}
run: |
make -C sby run_ci

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

@ -13,6 +13,7 @@ jobs:
uses: actions/checkout@v4
with:
fetch-depth: 0
submodules: true
- name: Take last commit
id: log
run: echo "message=$(git log --no-merges -1 --oneline)" >> $GITHUB_OUTPUT

31
.github/workflows/vs.yml vendored
View file

@ -1,31 +0,0 @@
name: Visual Studio Build
on: [push, pull_request]
jobs:
yosys-vcxsrc:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Build
run: make vcxsrc YOSYS_VER=latest
- uses: actions/upload-artifact@v4
with:
name: vcxsrc
path: yosys-win32-vcxsrc-latest.zip
build:
runs-on: windows-2019
needs: yosys-vcxsrc
steps:
- uses: actions/download-artifact@v4
with:
name: vcxsrc
path: .
- name: unzip
run: unzip yosys-win32-vcxsrc-latest.zip
- name: setup-msbuild
uses: microsoft/setup-msbuild@v1
- name: MSBuild
working-directory: yosys-win32-vcxsrc-latest
run: msbuild YosysVS.sln /p:PlatformToolset=v142 /p:Configuration=Release /p:WindowsTargetPlatformVersion=10.0.17763.0

30
.github/workflows/wasi.yml vendored
View file

@ -1,30 +0,0 @@
name: WASI Build
on: [push, pull_request]
jobs:
wasi:
runs-on: ubuntu-latest
steps:
- uses: actions/checkout@v4
- name: Build
run: |
WASI_SDK=wasi-sdk-19.0
WASI_SDK_URL=https://github.com/WebAssembly/wasi-sdk/releases/download/wasi-sdk-19/wasi-sdk-19.0-linux.tar.gz
if ! [ -d ${WASI_SDK} ]; then curl -L ${WASI_SDK_URL} | tar xzf -; fi
mkdir -p build
cat > build/Makefile.conf <<END
export PATH := $(pwd)/${WASI_SDK}/bin:${PATH}
WASI_SYSROOT := $(pwd)/${WASI_SDK}/share/wasi-sysroot
CONFIG := wasi
PREFIX := /
ENABLE_TCL := 0
ENABLE_READLINE := 0
ENABLE_PLUGINS := 0
ENABLE_ZLIB := 0
END
make -C build -f ../Makefile CXX=clang -j$(nproc)

2
.gitignore vendored
View file

@ -18,7 +18,6 @@ __pycache__
/coverage.info
/coverage_html
/Makefile.conf
/abc
/viz.js
/yosys
/yosys.exe
@ -46,3 +45,4 @@ __pycache__
/tests/unit/bintest/
/tests/unit/objtest/
/tests/ystests
/build

3
.gitmodules vendored Normal file
View file

@ -0,0 +1,3 @@
[submodule "abc"]
path = abc
url = https://github.com/YosysHQ/abc

16
CHANGELOG
View file

@ -2,9 +2,23 @@
List of major changes and improvements between releases
=======================================================
Yosys 0.40 .. Yosys 0.41-dev
Yosys 0.41 .. Yosys 0.42-dev
--------------------------
Yosys 0.40 .. Yosys 0.41
--------------------------
* New commands and options
- Added "cellmatch" pass for picking out standard cells automatically.
* Various
- Extended the experimental incremental JSON API to allow arbitrary
smtlib subexpressions.
- Added support for using ABCs library merging when providing multiple
liberty files.
* Verific support
- Expose library name as module attribute.
Yosys 0.39 .. Yosys 0.40
--------------------------
* New commands and options

82
Makefile
View file

@ -142,7 +142,7 @@ LIBS += -lrt
endif
endif
YOSYS_VER := 0.40+7
YOSYS_VER := 0.41+8
# Note: We arrange for .gitcommit to contain the (short) commit hash in
# tarballs generated with git-archive(1) using .gitattributes. The git repo
@ -158,17 +158,8 @@ endif
OBJS = kernel/version_$(GIT_REV).o
bumpversion:
sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline a1bb025.. | wc -l`/;" Makefile
sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline c1ad377.. | wc -l`/;" Makefile
# set 'ABCREV = default' to use abc/ as it is
#
# Note: If you do ABC development, make sure that 'abc' in this directory
# is just a symlink to your actual ABC working directory, as 'make mrproper'
# will remove the 'abc' directory and you do not want to accidentally
# delete your work on ABC..
ABCREV = 0cd90d0
ABCPULL = 1
ABCURL ?= https://github.com/YosysHQ/abc
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
@ -789,41 +780,43 @@ $(PROGRAM_PREFIX)yosys-config: misc/yosys-config.in
-e 's#@BINDIR@#$(strip $(BINDIR))#;' -e 's#@DATDIR@#$(strip $(DATDIR))#;' < $< > $(PROGRAM_PREFIX)yosys-config
$(Q) chmod +x $(PROGRAM_PREFIX)yosys-config
abc/abc-$(ABCREV)$(EXE) abc/libabc-$(ABCREV).a:
.PHONY: check-git-abc
check-git-abc:
@if [ ! -d "$(YOSYS_SRC)/abc" ]; then \
echo "Error: The 'abc' directory does not exist."; \
echo "Initialize the submodule: Run 'git submodule update --init' to set up 'abc' as a submodule."; \
exit 1; \
elif git -C "$(YOSYS_SRC)" submodule status abc 2>/dev/null | grep -q '^ '; then \
echo "'abc' is a git submodule. Continuing."; \
exit 0; \
elif [ -f "$(YOSYS_SRC)/abc/.gitcommit" ] && ! grep -q '\$$Format:%h\$$' "$(YOSYS_SRC)/abc/.gitcommit"; then \
echo "'abc' comes from a tarball. Continuing."; \
exit 0; \
elif [ -f "$(YOSYS_SRC)/abc/.gitcommit" ] && grep -q '\$$Format:%h\$$' "$(YOSYS_SRC)/abc/.gitcommit"; then \
echo "Error: 'abc' is not configured as a git submodule."; \
echo "To resolve this:"; \
echo "1. Back up your changes: Save any modifications from the 'abc' directory to another location."; \
echo "2. Remove the existing 'abc' directory: Delete the 'abc' directory and all its contents."; \
echo "3. Initialize the submodule: Run 'git submodule update --init' to set up 'abc' as a submodule."; \
echo "4. Reapply your changes: Move your saved changes back to the 'abc' directory, if necessary."; \
exit 1; \
else \
echo "Initialize the submodule: Run 'git submodule update --init' to set up 'abc' as a submodule."; \
exit 1; \
fi
ABC_SOURCES := $(wildcard $(YOSYS_SRC)/abc/*)
abc/abc$(EXE) abc/libabc.a: $(ABC_SOURCES) check-git-abc
$(P)
ifneq ($(ABCREV),default)
$(Q) if test -d abc/.hg; then \
echo 'REEBE: NOP qverpgbel vf n ut jbexvat pbcl! Erzbir nop/ naq er-eha "znxr".' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; false; \
fi
$(Q) if test -d abc && test -d abc/.git && ! git -C abc diff-index --quiet HEAD; then \
echo 'REEBE: NOP pbagnvaf ybpny zbqvsvpngvbaf! Frg NOPERI=qrsnhyg va Lbflf Znxrsvyr!' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; false; \
fi
$(Q) if test -d abc && ! test -d abc/.git && ! test "`cat abc/.gitcommit | cut -c1-7`" = "$(ABCREV)"; then \
echo 'REEBE: Qbjaybnqrq NOP irefvbaf qbrf abg zngpu! Qbjaybnq sebz:' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; echo $(ABCURL)/archive/$(ABCREV).tar.gz; false; \
fi
# set a variable so the test fails if git fails to run - when comparing outputs directly, empty string would match empty string
$(Q) if test -d abc && ! test -d abc/.git && test "`cat abc/.gitcommit | cut -c1-7`" = "$(ABCREV)"; then \
echo "Compiling local copy of ABC"; \
elif ! (cd abc 2> /dev/null && rev="`git rev-parse $(ABCREV)`" && test "`git rev-parse HEAD`" = "$$rev"); then \
test $(ABCPULL) -ne 0 || { echo 'REEBE: NOP abg hc gb qngr naq NOPCHYY frg gb 0 va Znxrsvyr!' | tr 'A-Za-z' 'N-ZA-Mn-za-m'; exit 1; }; \
echo "Pulling ABC from $(ABCURL):"; set -x; \
test -d abc || git clone $(ABCURL) abc; \
cd abc && $(MAKE) DEP= clean && git fetch $(ABCURL) && git checkout $(ABCREV); \
fi
endif
$(Q) rm -f abc/abc-[0-9a-f]*
$(Q) $(MAKE) -C abc $(S) $(ABCMKARGS) $(if $(filter %.a,$@),PROG="abc-$(ABCREV)",PROG="abc-$(ABCREV)$(EXE)") MSG_PREFIX="$(eval P_OFFSET = 5)$(call P_SHOW)$(eval P_OFFSET = 10) ABC: " $(if $(filter %.a,$@),libabc-$(ABCREV).a)
$(Q) mkdir -p abc && $(MAKE) -C $(PROGRAM_PREFIX)abc -f "$(realpath $(YOSYS_SRC)/abc/Makefile)" ABCSRC="$(realpath $(YOSYS_SRC)/abc/)" $(S) $(ABCMKARGS) $(if $(filter %.a,$@),PROG="abc",PROG="abc$(EXE)") MSG_PREFIX="$(eval P_OFFSET = 5)$(call P_SHOW)$(eval P_OFFSET = 10) ABC: " $(if $(filter %.a,$@),libabc.a)
ifeq ($(ABCREV),default)
.PHONY: abc/abc-$(ABCREV)$(EXE)
.PHONY: abc/libabc-$(ABCREV).a
endif
$(PROGRAM_PREFIX)yosys-abc$(EXE): abc/abc$(EXE)
$(P) cp $< $(PROGRAM_PREFIX)yosys-abc$(EXE)
$(PROGRAM_PREFIX)yosys-abc$(EXE): abc/abc-$(ABCREV)$(EXE)
$(P) cp abc/abc-$(ABCREV)$(EXE) $(PROGRAM_PREFIX)yosys-abc$(EXE)
$(PROGRAM_PREFIX)yosys-libabc.a: abc/libabc-$(ABCREV).a
$(P) cp abc/libabc-$(ABCREV).a $(PROGRAM_PREFIX)yosys-libabc.a
$(PROGRAM_PREFIX)yosys-libabc.a: abc/libabc.a
$(P) cp $< $(PROGRAM_PREFIX)yosys-libabc.a
ifneq ($(SEED),)
SEEDOPT="-S $(SEED)"
@ -1141,9 +1134,6 @@ echo-yosys-ver:
echo-git-rev:
@echo "$(GIT_REV)"
echo-abc-rev:
@echo "$(ABCREV)"
echo-cxx:
@echo "$(CXX)"

1
abc Submodule

@ -0,0 +1 @@
Subproject commit 237d81397fcc85dd3894bf1a449d2955cd3df02d

195
backends/cxxrtl/cxxrtl_backend.cc
View file

@ -606,22 +606,30 @@ std::vector<std::string> split_by(const std::string &str, const std::string &sep
return result;
}
std::string escape_cxx_string(const std::string &input)
std::string escape_c_string(const std::string &input)
{
std::string output = "\"";
std::string output;
output.push_back('"');
for (auto c : input) {
if (::isprint(c)) {
if (c == '\\')
output.push_back('\\');
output.push_back(c);
} else {
char l = c & 0xf, h = (c >> 4) & 0xf;
output.append("\\x");
output.push_back((h < 10 ? '0' + h : 'a' + h - 10));
output.push_back((l < 10 ? '0' + l : 'a' + l - 10));
char l = c & 0x3, m = (c >> 3) & 0x3, h = (c >> 6) & 0x3;
output.append("\\");
output.push_back('0' + h);
output.push_back('0' + m);
output.push_back('0' + l);
}
}
output.push_back('"');
return output;
}
std::string escape_cxx_string(const std::string &input)
{
std::string output = escape_c_string(input);
if (output.find('\0') != std::string::npos) {
output.insert(0, "std::string {");
output.append(stringf(", %zu}", input.size()));
@ -2275,46 +2283,92 @@ struct CxxrtlWorker {
dec_indent();
}
void dump_metadata_map(const dict<RTLIL::IdString, RTLIL::Const> &metadata_map)
{
if (metadata_map.empty()) {
f << "metadata_map()";
return;
}
f << "metadata_map({\n";
inc_indent();
for (auto metadata_item : metadata_map) {
if (!metadata_item.first.isPublic())
continue;
if (metadata_item.second.size() > 64 && (metadata_item.second.flags & RTLIL::CONST_FLAG_STRING) == 0) {
f << indent << "/* attribute " << metadata_item.first.str().substr(1) << " is over 64 bits wide */\n";
continue;
}
f << indent << "{ " << escape_cxx_string(metadata_item.first.str().substr(1)) << ", ";
// In Yosys, a real is a type of string.
if (metadata_item.second.flags & RTLIL::CONST_FLAG_REAL) {
f << std::showpoint << std::stod(metadata_item.second.decode_string()) << std::noshowpoint;
} else if (metadata_item.second.flags & RTLIL::CONST_FLAG_STRING) {
f << escape_cxx_string(metadata_item.second.decode_string());
} else if (metadata_item.second.flags & RTLIL::CONST_FLAG_SIGNED) {
f << "INT64_C(" << metadata_item.second.as_int(/*is_signed=*/true) << ")";
} else {
f << "UINT64_C(" << metadata_item.second.as_int(/*is_signed=*/false) << ")";
}
f << " },\n";
void dump_serialized_metadata(const dict<RTLIL::IdString, RTLIL::Const> &metadata_map) {
// Creating thousands metadata_map objects using initializer lists in a single function results in one of:
// 1. Megabytes of stack usage (with __attribute__((optnone))).
// 2. Minutes of compile time (without __attribute__((optnone))).
// So, don't create them.
std::string data;
auto put_u64 = [&](uint64_t value) {
for (size_t count = 0; count < 8; count++) {
data += (char)(value >> 56);
value <<= 8;
}
dec_indent();
f << indent << "})";
};
for (auto metadata_item : metadata_map) {
if (!metadata_item.first.isPublic())
continue;
if (metadata_item.second.size() > 64 && (metadata_item.second.flags & RTLIL::CONST_FLAG_STRING) == 0) {
f << indent << "/* attribute " << metadata_item.first.str().substr(1) << " is over 64 bits wide */\n";
continue;
}
data += metadata_item.first.str().substr(1) + '\0';
// In Yosys, a real is a type of string.
if (metadata_item.second.flags & RTLIL::CONST_FLAG_REAL) {
double dvalue = std::stod(metadata_item.second.decode_string());
uint64_t uvalue;
static_assert(sizeof(dvalue) == sizeof(uvalue), "double must be 64 bits in size");
memcpy(&uvalue, &dvalue, sizeof(uvalue));
data += 'd';
put_u64(uvalue);
} else if (metadata_item.second.flags & RTLIL::CONST_FLAG_STRING) {
data += 's';
data += metadata_item.second.decode_string();
data += '\0';
} else if (metadata_item.second.flags & RTLIL::CONST_FLAG_SIGNED) {
data += 'i';
put_u64((uint64_t)metadata_item.second.as_int(/*is_signed=*/true));
} else {
data += 'u';
put_u64(metadata_item.second.as_int(/*is_signed=*/false));
}
}
f << escape_c_string(data);
}
void dump_debug_attrs(const RTLIL::AttrObject *object)
void dump_metadata_map(const dict<RTLIL::IdString, RTLIL::Const> &metadata_map) {
if (metadata_map.empty()) {
f << "metadata_map()";
} else {
f << "metadata_map({\n";
inc_indent();
for (auto metadata_item : metadata_map) {
if (!metadata_item.first.isPublic())
continue;
if (metadata_item.second.size() > 64 && (metadata_item.second.flags & RTLIL::CONST_FLAG_STRING) == 0) {
f << indent << "/* attribute " << metadata_item.first.str().substr(1) << " is over 64 bits wide */\n";
continue;
}
f << indent << "{ " << escape_cxx_string(metadata_item.first.str().substr(1)) << ", ";
// In Yosys, a real is a type of string.
if (metadata_item.second.flags & RTLIL::CONST_FLAG_REAL) {
f << std::showpoint << std::stod(metadata_item.second.decode_string()) << std::noshowpoint;
} else if (metadata_item.second.flags & RTLIL::CONST_FLAG_STRING) {
f << escape_cxx_string(metadata_item.second.decode_string());
} else if (metadata_item.second.flags & RTLIL::CONST_FLAG_SIGNED) {
f << "INT64_C(" << metadata_item.second.as_int(/*is_signed=*/true) << ")";
} else {
f << "UINT64_C(" << metadata_item.second.as_int(/*is_signed=*/false) << ")";
}
f << " },\n";
}
dec_indent();
f << indent << "})";
}
}
void dump_debug_attrs(const RTLIL::AttrObject *object, bool serialize = true)
{
dict<RTLIL::IdString, RTLIL::Const> attributes = object->attributes;
// Inherently necessary to get access to the object, so a waste of space to emit.
attributes.erase(ID::hdlname);
// Internal Yosys attribute that should be removed but isn't.
attributes.erase(ID::module_not_derived);
dump_metadata_map(attributes);
if (serialize) {
dump_serialized_metadata(attributes);
} else {
dump_metadata_map(attributes);
}
}
void dump_debug_info_method(RTLIL::Module *module)
@ -2337,7 +2391,7 @@ struct CxxrtlWorker {
// The module is responsible for adding its own scope.
f << indent << "scopes->add(path.empty() ? path : path.substr(0, path.size() - 1), ";
f << escape_cxx_string(get_hdl_name(module)) << ", ";
dump_debug_attrs(module);
dump_debug_attrs(module, /*serialize=*/false);
f << ", std::move(cell_attrs));\n";
count_scopes++;
// If there were any submodules that were flattened, the module is also responsible for adding them.
@ -2347,11 +2401,11 @@ struct CxxrtlWorker {
auto module_attrs = scopeinfo_attributes(cell, ScopeinfoAttrs::Module);
auto cell_attrs = scopeinfo_attributes(cell, ScopeinfoAttrs::Cell);
cell_attrs.erase(ID::module_not_derived);
f << indent << "scopes->add(path + " << escape_cxx_string(get_hdl_name(cell)) << ", ";
f << indent << "scopes->add(path, " << escape_cxx_string(get_hdl_name(cell)) << ", ";
f << escape_cxx_string(cell->get_string_attribute(ID(module))) << ", ";
dump_metadata_map(module_attrs);
dump_serialized_metadata(module_attrs);
f << ", ";
dump_metadata_map(cell_attrs);
dump_serialized_metadata(cell_attrs);
f << ");\n";
} else log_assert(false && "Unknown $scopeinfo type");
count_scopes++;
@ -2419,20 +2473,22 @@ struct CxxrtlWorker {
if (has_driven_sync + has_driven_comb + has_undriven > 1)
count_mixed_driver++;
f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire));
f << ", debug_item(" << mangle(wire) << ", " << wire->start_offset;
bool first = true;
for (auto flag : flags) {
if (first) {
first = false;
f << ", ";
} else {
f << "|";
}
f << "debug_item::" << flag;
}
f << "), ";
f << indent << "items->add(path, " << escape_cxx_string(get_hdl_name(wire)) << ", ";
dump_debug_attrs(wire);
f << ", " << mangle(wire);
if (wire->start_offset != 0 || !flags.empty()) {
f << ", " << wire->start_offset;
bool first = true;
for (auto flag : flags) {
if (first) {
first = false;
f << ", ";
} else {
f << "|";
}
f << "debug_item::" << flag;
}
}
f << ");\n";
count_member_wires++;
break;
@ -2440,16 +2496,18 @@ struct CxxrtlWorker {
case WireType::ALIAS: {
// Alias of a member wire
const RTLIL::Wire *aliasee = debug_wire_type.sig_subst.as_wire();
f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire));
f << ", debug_item(";
f << indent << "items->add(path, " << escape_cxx_string(get_hdl_name(wire)) << ", ";
dump_debug_attrs(aliasee);
f << ", ";
// If the aliasee is an outline, then the alias must be an outline, too; otherwise downstream
// tooling has no way to find out about the outline.
if (debug_wire_types[aliasee].is_outline())
f << "debug_eval_outline";
else
f << "debug_alias()";
f << ", " << mangle(aliasee) << ", " << wire->start_offset << "), ";
dump_debug_attrs(aliasee);
f << ", " << mangle(aliasee);
if (wire->start_offset != 0)
f << ", " << wire->start_offset;
f << ");\n";
count_alias_wires++;
break;
@ -2459,18 +2517,22 @@ struct CxxrtlWorker {
f << indent << "static const value<" << wire->width << "> const_" << mangle(wire) << " = ";
dump_const(debug_wire_type.sig_subst.as_const());
f << ";\n";
f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire));
f << ", debug_item(const_" << mangle(wire) << ", " << wire->start_offset << "), ";
f << indent << "items->add(path, " << escape_cxx_string(get_hdl_name(wire)) << ", ";
dump_debug_attrs(wire);
f << ", const_" << mangle(wire);
if (wire->start_offset != 0)
f << ", " << wire->start_offset;
f << ");\n";
count_const_wires++;
break;
}
case WireType::OUTLINE: {
// Localized or inlined, but rematerializable wire
f << indent << "items->add(path + " << escape_cxx_string(get_hdl_name(wire));
f << ", debug_item(debug_eval_outline, " << mangle(wire) << ", " << wire->start_offset << "), ";
f << indent << "items->add(path, " << escape_cxx_string(get_hdl_name(wire)) << ", ";
dump_debug_attrs(wire);
f << ", debug_eval_outline, " << mangle(wire);
if (wire->start_offset != 0)
f << ", " << wire->start_offset;
f << ");\n";
count_inline_wires++;
break;
@ -2486,15 +2548,14 @@ struct CxxrtlWorker {
for (auto &mem : mod_memories[module]) {
if (!mem.memid.isPublic())
continue;
f << indent << "items->add(path + " << escape_cxx_string(mem.packed ? get_hdl_name(mem.cell) : get_hdl_name(mem.mem));
f << ", debug_item(" << mangle(&mem) << ", ";
f << mem.start_offset << "), ";
f << indent << "items->add(path, " << escape_cxx_string(mem.packed ? get_hdl_name(mem.cell) : get_hdl_name(mem.mem)) << ", ";
if (mem.packed) {
dump_debug_attrs(mem.cell);
} else {
dump_debug_attrs(mem.mem);
}
f << ");\n";
f << ", " << mangle(&mem) << ", ";
f << mem.start_offset << ");\n";
}
}
dec_indent();
@ -2506,7 +2567,7 @@ struct CxxrtlWorker {
const char *access = is_cxxrtl_blackbox_cell(cell) ? "->" : ".";
f << indent << mangle(cell) << access;
f << "debug_info(items, scopes, path + " << escape_cxx_string(get_hdl_name(cell) + ' ') << ", ";
dump_debug_attrs(cell);
dump_debug_attrs(cell, /*serialize=*/false);
f << ");\n";
}
}

60
backends/cxxrtl/runtime/cxxrtl/cxxrtl.h
View file

@ -941,6 +941,55 @@ struct metadata {
assert(value_type == DOUBLE);
return double_value;
}
// Internal CXXRTL use only.
static std::map<std::string, metadata> deserialize(const char *ptr) {
std::map<std::string, metadata> result;
std::string name;
// Grammar:
// string ::= [^\0]+ \0
// metadata ::= [uid] .{8} | s <string>
// map ::= ( <string> <metadata> )* \0
for (;;) {
if (*ptr) {
name += *ptr++;
} else if (!name.empty()) {
ptr++;
auto get_u64 = [&]() {
uint64_t result = 0;
for (size_t count = 0; count < 8; count++)
result = (result << 8) | *ptr++;
return result;
};
char type = *ptr++;
if (type == 'u') {
uint64_t value = get_u64();
result.emplace(name, value);
} else if (type == 'i') {
int64_t value = (int64_t)get_u64();
result.emplace(name, value);
} else if (type == 'd') {
double dvalue;
uint64_t uvalue = get_u64();
static_assert(sizeof(dvalue) == sizeof(uvalue), "double must be 64 bits in size");
memcpy(&dvalue, &uvalue, sizeof(dvalue));
result.emplace(name, dvalue);
} else if (type == 's') {
std::string value;
while (*ptr)
value += *ptr++;
ptr++;
result.emplace(name, value);
} else {
assert(false && "Unknown type specifier");
return result;
}
name.clear();
} else {
return result;
}
}
}
};
typedef std::map<std::string, metadata> metadata_map;
@ -1417,6 +1466,12 @@ struct debug_items {
});
}
// This overload exists to reduce excessive stack slot allocation in `CXXRTL_EXTREMELY_COLD void debug_info()`.
template<class... T>
void add(const std::string &base_path, const char *path, const char *serialized_item_attrs, T&&... args) {
add(base_path + path, debug_item(std::forward<T>(args)...), metadata::deserialize(serialized_item_attrs));
}
size_t count(const std::string &path) const {
if (table.count(path) == 0)
return 0;
@ -1463,6 +1518,11 @@ struct debug_scopes {
scope.cell_attrs = std::unique_ptr<debug_attrs>(new debug_attrs { cell_attrs });
}
// This overload exists to reduce excessive stack slot allocation in `CXXRTL_EXTREMELY_COLD void debug_info()`.
void add(const std::string &base_path, const char *path, const char *module_name, const char *serialized_module_attrs, const char *serialized_cell_attrs) {
add(base_path + path, module_name, metadata::deserialize(serialized_module_attrs), metadata::deserialize(serialized_cell_attrs));
}
size_t contains(const std::string &path) const {
return table.count(path);
}

5
backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h
View file

@ -512,9 +512,10 @@ public:
spool &operator=(const spool &) = delete;
~spool() {
if (int fd = writefd.exchange(-1))
int fd;
if ((fd = writefd.exchange(-1)) != -1)
close(fd);
if (int fd = readfd.exchange(-1))
if ((fd = readfd.exchange(-1)) != -1)
close(fd);
}

213
backends/smt2/smtbmc.py
View file

@ -199,7 +199,6 @@ def help():
--minimize-assumes
when using --track-assumes, solve for a minimal set of sufficient assumptions.
""" + so.helpmsg())
def usage():
@ -670,18 +669,12 @@ if aimfile is not None:
ywfile_hierwitness_cache = None
def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False):
def ywfile_hierwitness():
global ywfile_hierwitness_cache
if map_steps is None:
map_steps = {}
if ywfile_hierwitness_cache is None:
ywfile_hierwitness = smt.hierwitness(topmod, allregs=True, blackbox=True)
with open(inywfile, "r") as f:
inyw = ReadWitness(f)
if ywfile_hierwitness_cache is None:
ywfile_hierwitness_cache = smt.hierwitness(topmod, allregs=True, blackbox=True)
inits, seqs, clocks, mems = ywfile_hierwitness_cache
inits, seqs, clocks, mems = ywfile_hierwitness
smt_wires = defaultdict(list)
smt_mems = defaultdict(list)
@ -692,9 +685,128 @@ def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False):
for mem in mems:
smt_mems[mem["path"]].append(mem)
addr_re = re.compile(r'\\\[[0-9]+\]$')
bits_re = re.compile(r'[01?]*$')
ywfile_hierwitness_cache = inits, seqs, clocks, mems, smt_wires, smt_mems
return ywfile_hierwitness_cache
def_bits_re = re.compile(r'([01]+)')
def smt_extract_mask(smt_expr, mask):
chunks = []
def_bits = ''
mask_index_order = mask[::-1]
for matched in def_bits_re.finditer(mask_index_order):
chunks.append(matched.span())
def_bits += matched[0]
if not chunks:
return
if len(chunks) == 1:
start, end = chunks[0]
if start == 0 and end == len(mask_index_order):
combined_chunks = smt_expr
else:
combined_chunks = '((_ extract %d %d) %s)' % (end - 1, start, smt_expr)
else:
combined_chunks = '(let ((x %s)) (concat %s))' % (smt_expr, ' '.join(
'((_ extract %d %d) x)' % (end - 1, start)
for start, end in reversed(chunks)
))
return combined_chunks, ''.join(mask_index_order[start:end] for start, end in chunks)[::-1]
def smt_concat(exprs):
if not exprs:
return ""
if len(exprs) == 1:
return exprs[1]
return "(concat %s)" % ' '.join(exprs)
def ywfile_signal(sig, step, mask=None):
assert sig.width > 0
inits, seqs, clocks, mems, smt_wires, smt_mems = ywfile_hierwitness()
sig_end = sig.offset + sig.width
output = []
if sig.path in smt_wires:
for wire in smt_wires[sig.path]:
width, offset = wire["width"], wire["offset"]
smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1
offset = max(offset, 0)
end = width + offset
common_offset = max(sig.offset, offset)
common_end = min(sig_end, end)
if common_end <= common_offset:
continue
smt_expr = smt.witness_net_expr(topmod, f"s{step}", wire)
if not smt_bool:
slice_high = common_end - offset - 1
slice_low = common_offset - offset
smt_expr = "((_ extract %d %d) %s)" % (slice_high, slice_low, smt_expr)
else:
smt_expr = "(ite %s #b1 #b0)" % smt_expr
output.append(((common_offset - sig.offset), (common_end - sig.offset), smt_expr))
if sig.memory_path:
if sig.memory_path in smt_mems:
for mem in smt_mems[sig.memory_path]:
width, size, bv = mem["width"], mem["size"], mem["statebv"]
smt_expr = smt.net_expr(topmod, f"s{step}", mem["smtpath"])
if bv:
word_low = sig.memory_addr * width
word_high = word_low + width - 1
smt_expr = "((_ extract %d %d) %s)" % (word_high, word_low, smt_expr)
else:
addr_width = (size - 1).bit_length()
addr_bits = f"{sig.memory_addr:0{addr_width}b}"
smt_expr = "(select %s #b%s )" % (smt_expr, addr_bits)
if sig.width < width:
slice_high = sig.offset + sig.width - 1
smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr)
output.append((0, sig.width, smt_expr))
output.sort()
output = [chunk for chunk in output if chunk[0] != chunk[1]]
pos = 0
for start, end, smt_expr in output:
assert start == pos
pos = end
assert pos == sig.width
if len(output) == 1:
return output[0][-1]
return smt_concat(smt_expr for start, end, smt_expr in reversed(output))
def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False):
global ywfile_hierwitness_cache
if map_steps is None:
map_steps = {}
with open(inywfile, "r") as f:
inyw = ReadWitness(f)
inits, seqs, clocks, mems, smt_wires, smt_mems = ywfile_hierwitness()
bits_re = re.compile(r'[01?]*$')
max_t = -1
for t, step in inyw.steps():
@ -706,77 +818,14 @@ def ywfile_constraints(inywfile, constr_assumes, map_steps=None, skip_x=False):
if not bits_re.match(bits):
raise ValueError("unsupported bit value in Yosys witness file")
sig_end = sig.offset + len(bits)
if sig.path in smt_wires:
for wire in smt_wires[sig.path]:
width, offset = wire["width"], wire["offset"]
smt_expr = ywfile_signal(sig, map_steps.get(t, t))
smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1
smt_expr, bits = smt_extract_mask(smt_expr, bits)
offset = max(offset, 0)
smt_constr = "(= %s #b%s)" % (smt_expr, bits)
constr_assumes[t].append((inywfile, smt_constr))
end = width + offset
common_offset = max(sig.offset, offset)
common_end = min(sig_end, end)
if common_end <= common_offset:
continue
smt_expr = smt.witness_net_expr(topmod, f"s{map_steps.get(t, t)}", wire)
if not smt_bool:
slice_high = common_end - offset - 1
slice_low = common_offset - offset
smt_expr = "((_ extract %d %d) %s)" % (slice_high, slice_low, smt_expr)
bit_slice = bits[len(bits) - (common_end - sig.offset):len(bits) - (common_offset - sig.offset)]
if bit_slice.count("?") == len(bit_slice):
continue
if smt_bool:
assert width == 1
smt_constr = "(= %s %s)" % (smt_expr, "true" if bit_slice == "1" else "false")
else:
if "?" in bit_slice:
mask = bit_slice.replace("0", "1").replace("?", "0")
bit_slice = bit_slice.replace("?", "0")
smt_expr = "(bvand %s #b%s)" % (smt_expr, mask)
smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice)
constr_assumes[t].append((inywfile, smt_constr))
if sig.memory_path:
if sig.memory_path in smt_mems:
for mem in smt_mems[sig.memory_path]:
width, size, bv = mem["width"], mem["size"], mem["statebv"]
smt_expr = smt.net_expr(topmod, f"s{map_steps.get(t, t)}", mem["smtpath"])
if bv:
word_low = sig.memory_addr * width
word_high = word_low + width - 1
smt_expr = "((_ extract %d %d) %s)" % (word_high, word_low, smt_expr)
else:
addr_width = (size - 1).bit_length()
addr_bits = f"{sig.memory_addr:0{addr_width}b}"
smt_expr = "(select %s #b%s )" % (smt_expr, addr_bits)
if len(bits) < width:
slice_high = sig.offset + len(bits) - 1
smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr)
bit_slice = bits
if "?" in bit_slice:
mask = bit_slice.replace("0", "1").replace("?", "0")
bit_slice = bit_slice.replace("?", "0")
smt_expr = "(bvand %s #b%s)" % (smt_expr, mask)
smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice)
constr_assumes[t].append((inywfile, smt_constr))
max_t = t
return max_t
if inywfile is not None:
@ -1367,11 +1416,11 @@ def write_yw_trace(steps, index, allregs=False, filename=None):
exprs.extend(smt.witness_net_expr(topmod, f"s{k}", sig) for sig in sigs)
all_sigs.append(sigs)
all_sigs.append((step_values, sigs))
bvs = iter(smt.get_list(exprs))
for sigs in all_sigs:
for (step_values, sigs) in all_sigs:
for sig in sigs:
value = smt.bv2bin(next(bvs))
step_values[sig["sig"]] = value

147
backends/smt2/smtbmc_incremental.py
View file

@ -1,7 +1,7 @@
from collections import defaultdict
import json
import typing
from functools import partial
import ywio
if typing.TYPE_CHECKING:
import smtbmc
@ -34,6 +34,7 @@ class Incremental:
self._witness_index = None
self._yw_constraints = {}
self._define_sorts = {}
def setup(self):
generic_assert_map = smtbmc.get_assert_map(
@ -175,11 +176,7 @@ class Incremental:
if len(expr) == 1:
smt_out.push({"and": "true", "or": "false"}[expr[0]])
elif len(expr) == 2:
arg_sort = self.expr(expr[1], smt_out)
if arg_sort != "Bool":
raise InteractiveError(
f"arguments of {json.dumps(expr[0])} must have sort Bool"
)
self.expr(expr[1], smt_out, required_sort="Bool")
else:
sep = f"({expr[0]} "
for arg in expr[1:]:
@ -189,7 +186,51 @@ class Incremental:
smt_out.append(")")
return "Bool"
def expr_bv_binop(self, expr, smt_out):
self.expr_arg_len(expr, 2)
smt_out.append(f"({expr[0]} ")
arg_sort = self.expr(expr[1], smt_out, required_sort=("BitVec", None))
smt_out.append(" ")
self.expr(expr[2], smt_out, required_sort=arg_sort)
smt_out.append(")")
return arg_sort
def expr_extract(self, expr, smt_out):
self.expr_arg_len(expr, 3)
hi = expr[1]
lo = expr[2]
smt_out.append(f"((_ extract {hi} {lo}) ")
arg_sort = self.expr(expr[3], smt_out, required_sort=("BitVec", None))
smt_out.append(")")
if not (isinstance(hi, int) and 0 <= hi < arg_sort[1]):
raise InteractiveError(
f"high bit index must be 0 <= index < {arg_sort[1]}, is {hi!r}"
)
if not (isinstance(lo, int) and 0 <= lo <= hi):
raise InteractiveError(
f"low bit index must be 0 <= index < {hi}, is {lo!r}"
)
return "BitVec", hi - lo + 1
def expr_bv(self, expr, smt_out):
self.expr_arg_len(expr, 1)
arg = expr[1]
if not isinstance(arg, str) or arg.count("0") + arg.count("1") != len(arg):
raise InteractiveError("bv argument must contain only 0 or 1 bits")
smt_out.append("#b" + arg)
return "BitVec", len(arg)
def expr_yw(self, expr, smt_out):
self.expr_arg_len(expr, 1, 2)
if len(expr) == 2:
name = None
step = expr[1]
@ -219,6 +260,40 @@ class Incremental:
return "Bool"
def expr_yw_sig(self, expr, smt_out):
self.expr_arg_len(expr, 3, 4)
step = expr[1]
path = expr[2]
offset = expr[3]
width = expr[4] if len(expr) == 5 else 1
if not isinstance(offset, int) or offset < 0:
raise InteractiveError(
f"offset must be a non-negative integer, got {json.dumps(offset)}"
)
if not isinstance(width, int) or width <= 0:
raise InteractiveError(
f"width must be a positive integer, got {json.dumps(width)}"
)
if not isinstance(path, list) or not all(isinstance(s, str) for s in path):
raise InteractiveError(
f"path must be a string list, got {json.dumps(path)}"
)
if step not in self.state_set:
raise InteractiveError(f"step {step} not declared")
smt_expr = smtbmc.ywfile_signal(
ywio.WitnessSig(path=path, offset=offset, width=width), step
)
smt_out.append(smt_expr)
return "BitVec", width
def expr_smtlib(self, expr, smt_out):
self.expr_arg_len(expr, 2)
@ -231,10 +306,15 @@ class Incremental:
f"got {json.dumps(smtlib_expr)}"
)
if not isinstance(sort, str):
raise InteractiveError(
f"raw SMT-LIB sort has to be a string, got {json.dumps(sort)}"
)
if (
isinstance(sort, list)
and len(sort) == 2
and sort[0] == "BitVec"
and (sort[1] is None or isinstance(sort[1], int))
):
sort = tuple(sort)
elif not isinstance(sort, str):
raise InteractiveError(f"unsupported raw SMT-LIB sort {json.dumps(sort)}")
smt_out.append(smtlib_expr)
return sort
@ -258,6 +338,14 @@ class Incremental:
return sort
def expr_def(self, expr, smt_out):
self.expr_arg_len(expr, 1)
sort = self._define_sorts.get(expr[1])
if sort is None:
raise InteractiveError(f"unknown definition {json.dumps(expr)}")
smt_out.append(expr[1])
return sort
expr_handlers = {
"step": expr_step,
"cell": expr_cell,
@ -270,8 +358,15 @@ class Incremental:
"not": expr_not,
"and": expr_andor,
"or": expr_andor,
"bv": expr_bv,
"bvand": expr_bv_binop,
"bvor": expr_bv_binop,
"bvxor": expr_bv_binop,
"extract": expr_extract,
"def": expr_def,
"=": expr_eq,
"yw": expr_yw,
"yw_sig": expr_yw_sig,
"smtlib": expr_smtlib,
"!": expr_label,
}
@ -305,10 +400,13 @@ class Incremental:
raise InteractiveError(f"unknown expression {json.dumps(expr[0])}")
def expr_smt(self, expr, required_sort):
return self.expr_smt_and_sort(expr, required_sort)[0]
def expr_smt_and_sort(self, expr, required_sort=None):
smt_out = []
self.expr(expr, smt_out, required_sort=required_sort)
output_sort = self.expr(expr, smt_out, required_sort=required_sort)
out = "".join(smt_out)
return out
return out, output_sort
def cmd_new_step(self, cmd):
step = self.arg_step(cmd, declare=True)
@ -338,7 +436,6 @@ class Incremental:
expr = cmd.get("expr")
key = cmd.get("key")
key = mkkey(key)
result = smtbmc.smt.smt2_assumptions.pop(key, None)
@ -348,7 +445,7 @@ class Incremental:
return result
def cmd_get_unsat_assumptions(self, cmd):
return smtbmc.smt.get_unsat_assumptions(minimize=bool(cmd.get('minimize')))
return smtbmc.smt.get_unsat_assumptions(minimize=bool(cmd.get("minimize")))
def cmd_push(self, cmd):
smtbmc.smt_push()
@ -370,6 +467,27 @@ class Incremental:
if response:
return smtbmc.smt.read()
def cmd_define(self, cmd):
expr = cmd.get("expr")
if expr is None:
raise InteractiveError("'define' copmmand requires 'expr' parameter")
expr, sort = self.expr_smt_and_sort(expr)
if isinstance(sort, tuple) and sort[0] == "module":
raise InteractiveError("'define' does not support module sorts")
define_name = f"|inc def {len(self._define_sorts)}|"
self._define_sorts[define_name] = sort
if isinstance(sort, tuple):
sort = f"(_ {' '.join(map(str, sort))})"
smtbmc.smt.write(f"(define-const {define_name} {sort} {expr})")
return {"name": define_name}
def cmd_design_hierwitness(self, cmd=None):
allregs = (cmd is None) or bool(cmd.get("allreges", False))
if self._cached_hierwitness[allregs] is not None:
@ -451,6 +569,7 @@ class Incremental:
"pop": cmd_pop,
"check": cmd_check,
"smtlib": cmd_smtlib,
"define": cmd_define,
"design_hierwitness": cmd_design_hierwitness,
"write_yw_trace": cmd_write_yw_trace,
"read_yw_trace": cmd_read_yw_trace,

21
backends/smt2/smtio.py
View file

@ -160,6 +160,7 @@ class SmtIo:
self.noincr = opts.noincr
self.info_stmts = opts.info_stmts
self.nocomments = opts.nocomments
self.smt2_options.update(opts.smt2_options)
else:
self.solver = "yices"
@ -959,6 +960,8 @@ class SmtIo:
return int(self.bv2bin(v), 2)
def get_raw_unsat_assumptions(self):
if not self.smt2_assumptions:
return []
self.write("(get-unsat-assumptions)")
exprs = set(self.unparse(part) for part in self.parse(self.read()))
unsat_assumptions = []
@ -973,6 +976,10 @@ class SmtIo:
def get_unsat_assumptions(self, minimize=False):
if not minimize:
return self.get_raw_unsat_assumptions()
orig_assumptions = self.smt2_assumptions
self.smt2_assumptions = dict(orig_assumptions)
required_assumptions = {}
while True:
@ -998,6 +1005,7 @@ class SmtIo:
required_assumptions[candidate_key] = candidate_assume
if candidate_assumptions is not None:
self.smt2_assumptions = orig_assumptions
return list(required_assumptions)
def get(self, expr):
@ -1146,7 +1154,7 @@ class SmtIo:
class SmtOpts:
def __init__(self):
self.shortopts = "s:S:v"
self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments"]
self.longopts = ["unroll", "noincr", "noprogress", "timeout=", "dump-smt2=", "logic=", "dummy=", "info=", "nocomments", "smt2-option="]
self.solver = "yices"
self.solver_opts = list()
self.debug_print = False
@ -1159,6 +1167,7 @@ class SmtOpts:
self.logic = None
self.info_stmts = list()
self.nocomments = False
self.smt2_options = {}
def handle(self, o, a):
if o == "-s":
@ -1185,6 +1194,13 @@ class SmtOpts:
self.info_stmts.append(a)
elif o == "--nocomments":
self.nocomments = True
elif o == "--smt2-option":
args = a.split('=', 1)
if len(args) != 2:
print("--smt2-option expects an <option>=<value> argument")
sys.exit(1)
option, value = args
self.smt2_options[option] = value
else:
return False
return True
@ -1208,6 +1224,9 @@ class SmtOpts:
if solver is "dummy", read solver output from that file
otherwise: write solver output to that file
--smt2-option <option>=<value>
enable an SMT-LIBv2 option.
-v
enable debug output

11
docs/source/conf.py
View file

@ -4,7 +4,8 @@ import os
project = 'YosysHQ Yosys'
author = 'YosysHQ GmbH'
copyright ='2022 YosysHQ GmbH'
copyright ='2024 YosysHQ GmbH'
yosys_ver = "0.41"
# select HTML theme
html_theme = 'furo'
@ -46,12 +47,18 @@ extensions = ['sphinx.ext.autosectionlabel', 'sphinxcontrib.bibtex']
autosectionlabel_prefix_document = True
autosectionlabel_maxdepth = 1
# set version
if os.getenv("READTHEDOCS") and os.getenv("READTHEDOCS_VERSION") == "latest":
release = yosys_ver + "-dev"
else:
release = yosys_ver
# assign figure numbers
numfig = True
bibtex_bibfiles = ['literature.bib']
latex_elements = {
'releasename': 'Version',
'preamble': r'''
\usepackage{lmodern}
\usepackage{comment}

12
frontends/aiger/aigerparse.cc
View file

@ -590,6 +590,7 @@ void AigerReader::parse_aiger_ascii()
for (unsigned i = 0; i < O; ++i, ++line_count) {
if (!(f >> l1))
log_error("Line %u cannot be interpreted as an output!\n", line_count);
std::getline(f, line); // Ignore up to start of next line
log_debug2("%d is an output\n", l1);
RTLIL::Wire *wire = module->addWire(stringf("$o%0*d", digits, i));
@ -597,20 +598,18 @@ void AigerReader::parse_aiger_ascii()
module->connect(wire, createWireIfNotExists(module, l1));
outputs.push_back(wire);
}
//std::getline(f, line); // Ignore up to start of next line
// Parse bad properties
for (unsigned i = 0; i < B; ++i, ++line_count) {
if (!(f >> l1))
log_error("Line %u cannot be interpreted as a bad state property!\n", line_count);
std::getline(f, line); // Ignore up to start of next line
log_debug2("%d is a bad state property\n", l1);
RTLIL::Wire *wire = createWireIfNotExists(module, l1);
wire->port_output = true;
bad_properties.push_back(wire);
}
//if (B > 0)
// std::getline(f, line); // Ignore up to start of next line
// TODO: Parse invariant constraints
for (unsigned i = 0; i < C; ++i, ++line_count)
@ -628,6 +627,7 @@ void AigerReader::parse_aiger_ascii()
for (unsigned i = 0; i < A; ++i) {
if (!(f >> l1 >> l2 >> l3))
log_error("Line %u cannot be interpreted as an AND!\n", line_count);
std::getline(f, line); // Ignore up to start of next line
log_debug2("%d %d %d is an AND\n", l1, l2, l3);
log_assert(!(l1 & 1));
@ -636,7 +636,6 @@ void AigerReader::parse_aiger_ascii()
RTLIL::Wire *i2_wire = createWireIfNotExists(module, l3);
module->addAndGate("$and" + o_wire->name.str(), i1_wire, i2_wire, o_wire);
}
std::getline(f, line); // Ignore up to start of next line
}
static unsigned parse_next_delta_literal(std::istream &f, unsigned ref)
@ -715,6 +714,7 @@ void AigerReader::parse_aiger_binary()
for (unsigned i = 0; i < O; ++i, ++line_count) {
if (!(f >> l1))
log_error("Line %u cannot be interpreted as an output!\n", line_count);
std::getline(f, line); // Ignore up to start of next line
log_debug2("%d is an output\n", l1);
RTLIL::Wire *wire = module->addWire(stringf("$o%0*d", digits, i));
@ -722,20 +722,18 @@ void AigerReader::parse_aiger_binary()
module->connect(wire, createWireIfNotExists(module, l1));
outputs.push_back(wire);
}
std::getline(f, line); // Ignore up to start of next line
// Parse bad properties
for (unsigned i = 0; i < B; ++i, ++line_count) {
if (!(f >> l1))
log_error("Line %u cannot be interpreted as a bad state property!\n", line_count);
std::getline(f, line); // Ignore up to start of next line
log_debug2("%d is a bad state property\n", l1);
RTLIL::Wire *wire = createWireIfNotExists(module, l1);
wire->port_output = true;
bad_properties.push_back(wire);
}
if (B > 0)
std::getline(f, line); // Ignore up to start of next line
// TODO: Parse invariant constraints
for (unsigned i = 0; i < C; ++i, ++line_count)

2
frontends/ast/genrtlil.cc
View file

@ -2224,7 +2224,7 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint)
else
input_error("FATAL.\n");
} else {
input_error("Unknown elabortoon system task '%s'.\n", str.c_str());
input_error("Unknown elaboration system task '%s'.\n", str.c_str());
}
} break;

12
frontends/verific/verific.cc
View file

@ -2156,8 +2156,16 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma
int port_offset = 0;
if (pr->GetPort()->Bus()) {
port_name = pr->GetPort()->Bus()->Name();
port_offset = pr->GetPort()->Bus()->IndexOf(pr->GetPort()) -
min(pr->GetPort()->Bus()->LeftIndex(), pr->GetPort()->Bus()->RightIndex());
int msb_index = pr->GetPort()->Bus()->LeftIndex();
int lsb_index = pr->GetPort()->Bus()->RightIndex();
int index_of_port = pr->GetPort()->Bus()->IndexOf(pr->GetPort());
port_offset = index_of_port - min(msb_index, lsb_index);
// In cases where the msb order is flipped we need to make sure
// that the indicies match LSB = 0 order to match the std::vector
// to SigSpec LSB = 0 precondition.
if (lsb_index > msb_index) {
port_offset = abs(port_offset - (lsb_index - min(msb_index, lsb_index)));
}
}
IdString port_name_id = RTLIL::escape_id(port_name);
auto &sigvec = cell_port_conns[port_name_id];

3
frontends/verilog/verilog_frontend.cc
View file

@ -270,8 +270,11 @@ struct VerilogFrontend : public Frontend {
frontend_verilog_yydebug = false;
sv_mode = false;
formal_mode = false;
noassert_mode = false;
noassume_mode = false;
norestrict_mode = false;
assume_asserts_mode = false;
assert_assumes_mode = false;
lib_mode = false;
specify_mode = false;
default_nettype_wire = true;

2
kernel/constids.inc
View file

@ -222,6 +222,8 @@ X(_TECHMAP_REPLACE_)
X(techmap_simplemap)
X(_techmap_special_)
X(techmap_wrap)
X(_TECHMAP_PLACEHOLDER_)
X(techmap_chtype)
X(T_FALL_MAX)
X(T_FALL_MIN)
X(T_FALL_TYP)

2
kernel/driver.cc
View file

@ -356,7 +356,7 @@ int main(int argc, char **argv)
printf(" -V\n");
printf(" print version information and exit\n");
printf("\n");
printf("The option -S is an shortcut for calling the \"synth\" command, a default\n");
printf("The option -S is a shortcut for calling the \"synth\" command, a default\n");
printf("script for transforming the Verilog input to a gate-level netlist. For example:\n");
printf("\n");
printf(" yosys -o output.blif -S input.v\n");

31
kernel/rtlil.cc
View file

@ -4435,9 +4435,36 @@ RTLIL::SigSpec RTLIL::SigSpec::extract(int offset, int length) const
log_assert(offset >= 0);
log_assert(length >= 0);
log_assert(offset + length <= width_);
unpack();
cover("kernel.rtlil.sigspec.extract_pos");
return std::vector<RTLIL::SigBit>(bits_.begin() + offset, bits_.begin() + offset + length);
if (packed()) {
SigSpec extracted;
extracted.width_ = length;
auto it = chunks_.begin();
for (; offset; offset -= it->width, it++) {
if (offset < it->width) {
int chunk_length = min(it->width - offset, length);
extracted.chunks_.emplace_back(it->extract(offset, chunk_length));
length -= chunk_length;
it++;
break;
}
}
for (; length; length -= it->width, it++) {
if (length >= it->width) {
extracted.chunks_.emplace_back(*it);
} else {
extracted.chunks_.emplace_back(it->extract(0, length));
break;
}
}
return extracted;
} else {
return std::vector<RTLIL::SigBit>(bits_.begin() + offset, bits_.begin() + offset + length);
}
}
void RTLIL::SigSpec::append(const RTLIL::SigSpec &signal)

2
passes/hierarchy/hierarchy.cc
View file

@ -47,7 +47,7 @@ void generate(RTLIL::Design *design, const std::vector<std::string> &celltypes,
{
if (design->module(cell->type) != nullptr)
continue;
if (cell->type.begins_with("$__"))
if (cell->type.begins_with("$") && !cell->type.begins_with("$__"))
continue;
for (auto &pattern : celltypes)
if (patmatch(pattern.c_str(), RTLIL::unescape_id(cell->type).c_str()))

2
passes/pmgen/ice40_dsp.cc
View file

@ -289,7 +289,7 @@ struct Ice40DspPass : public Pass {
log("\n");
log("Pack input registers (A, B, {C,D}; with optional hold), pipeline registers\n");
log("({F,J,K,G}, H), output registers (O -- full 32-bits or lower 16-bits only; with\n");
log("optional hold), and post-adder into into the SB_MAC16 resource.\n");
log("optional hold), and post-adder into the SB_MAC16 resource.\n");
log("\n");
log("Multiply-accumulate operations using the post-adder with feedback on the {C,D}\n");
log("input will be folded into the DSP. In this scenario only, resetting the\n");

1
passes/techmap/Makefile.inc
View file

@ -48,6 +48,7 @@ OBJS += passes/techmap/dfflegalize.o
OBJS += passes/techmap/dffunmap.o
OBJS += passes/techmap/flowmap.o
OBJS += passes/techmap/extractinv.o
OBJS += passes/techmap/cellmatch.o
endif
ifeq ($(DISABLE_SPAWN),0)

4
passes/techmap/abc.cc
View file

@ -804,8 +804,10 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
for (std::string dont_use_cell : dont_use_cells) {
dont_use_args += stringf("-X \"%s\" ", dont_use_cell.c_str());
}
bool first_lib = true;
for (std::string liberty_file : liberty_files) {
abc_script += stringf("read_lib %s -w \"%s\" ; ", dont_use_args.c_str(), liberty_file.c_str());
abc_script += stringf("read_lib %s %s -w \"%s\" ; ", dont_use_args.c_str(), first_lib ? "" : "-m", liberty_file.c_str());
first_lib = false;
}
for (std::string liberty_file : genlib_files)
abc_script += stringf("read_library \"%s\"; ", liberty_file.c_str());

312
passes/techmap/cellmatch.cc Normal file
View file

@ -0,0 +1,312 @@
#include "kernel/celltypes.h"
#include "kernel/register.h"
#include "kernel/rtlil.h"
#include "kernel/sigtools.h"
#include "kernel/consteval.h"
#include "kernel/utils.h"
#include <algorithm>
USING_YOSYS_NAMESPACE
YOSYS_NAMESPACE_BEGIN
// return module's inputs in canonical order
SigSpec module_inputs(Module *m)
{
SigSpec ret;
for (auto port : m->ports) {
Wire *w = m->wire(port);
if (!w->port_input)
continue;
if (w->width != 1)
log_error("Unsupported wide port (%s) of non-unit width found in module %s.\n",
log_id(w), log_id(m));
ret.append(w);
}
return ret;
}
// return module's outputs in canonical order
SigSpec module_outputs(Module *m)
{
SigSpec ret;
for (auto port : m->ports) {
Wire *w = m->wire(port);
if (!w->port_output)
continue;
if (w->width != 1)
log_error("Unsupported wide port (%s) of non-unit width found in module %s.\n",
log_id(w), log_id(m));
ret.append(w);
}
return ret;
}
// Permute the inputs of a single-output k-LUT according to varmap
uint64_t permute_lut(uint64_t lut, const std::vector<int> &varmap)
{
int k = varmap.size();
uint64_t ret = 0;
// Index j iterates over all bits in lut.
// When (j & 1 << n) is true,
// (lut & 1 << j) represents an output value where input var n is set.
// We use this fact to permute the LUT such that
// every variable n is remapped to varmap[n].
for (int j = 0; j < 1 << k; j++) {
int m = 0;
for (int l = 0; l < k; l++)
if (j & 1 << l)
m |= 1 << varmap[l];
if (lut & 1 << m)
ret |= 1 << j;
}
return ret;
}
// Find the LUT with the minimum integer representation
// such that it is a permutation of the given lut.
// The resulting LUT becomes the "fingerprint" of the "permutation class".
// This function checks all possible input permutations.
uint64_t p_class(int k, uint64_t lut)
{
std::vector<int> map;
for (int j = 0; j < k; j++)
map.push_back(j);
uint64_t repr = ~(uint64_t) 0;
std::vector<int> repr_vars;
while (true) {
uint64_t perm = permute_lut(lut, map);
if (perm <= repr) {
repr = perm;
repr_vars = map;
}
if (!std::next_permutation(map.begin(), map.end()))
break;
}
return repr;
}
// Represent module m as N single-output k-LUTs
// where k is the number of module inputs,
// and N is the number of module outputs.
bool derive_module_luts(Module *m, std::vector<uint64_t> &luts)
{
CellTypes ff_types;
ff_types.setup_stdcells_mem();
for (auto cell : m->cells()) {
if (ff_types.cell_known(cell->type)) {
log("Ignoring module '%s' which isn't purely combinational.\n", log_id(m));
return false;
}
}
SigSpec inputs = module_inputs(m);
SigSpec outputs = module_outputs(m);
int ninputs = inputs.size(), noutputs = outputs.size();
if (ninputs > 6) {
log_warning("Skipping module %s with more than 6 inputs bits.\n", log_id(m));
return false;
}
luts.clear();
luts.resize(noutputs);
ConstEval ceval(m);
for (int i = 0; i < 1 << ninputs; i++) {
ceval.clear();
for (int j = 0; j < ninputs; j++)
ceval.set(inputs[j], (i & (1 << j)) ? State::S1 : State::S0);
for (int j = 0; j < noutputs; j++) {
SigSpec bit = outputs[j];
if (!ceval.eval(bit)) {
log("Failed to evaluate output '%s' in module '%s'.\n",
log_signal(outputs[j]), log_id(m));
return false;
}
log_assert(ceval.eval(bit));
if (bit[0] == State::S1)
luts[j] |= 1 << i;
}
}
return true;
}
struct CellmatchPass : Pass {
CellmatchPass() : Pass("cellmatch", "match cells to their targets in cell library") {}
void help() override
{
// |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
log("\n");
log(" cellmatch -lib <design> [module selection]\n");
log("\n");
log("This pass identifies functionally equivalent counterparts between each of the\n");
log("selected modules and a module from the secondary design <design>. For every such\n");
log("correspondence found, a techmap rule is generated for mapping instances of the\n");
log("former to instances of the latter. This techmap rule is saved in yet another\n");
log("design called '$cellmatch', which is created if non-existent.\n");
log("\n");
log("This pass restricts itself to combinational modules. Modules are functionally\n");
log("equivalent as long as their truth tables are identical upto a permutation of\n");
log("inputs and outputs. The supported number of inputs is limited to 6.\n");
log("\n");
}
void execute(std::vector<std::string> args, RTLIL::Design *d) override
{
log_header(d, "Executing CELLMATCH pass. (match cells)\n");
size_t argidx;
bool lut_attrs = false;
Design *lib = NULL;
for (argidx = 1; argidx < args.size(); argidx++) {
if (args[argidx] == "-lut_attrs") {
// an undocumented debugging option
lut_attrs = true;
} else if (args[argidx] == "-lib" && argidx + 1 < args.size()) {
if (!saved_designs.count(args[++argidx]))
log_cmd_error("No design '%s' found!\n", args[argidx].c_str());
lib = saved_designs.at(args[argidx]);
} else {
break;
}
}
extra_args(args, argidx, d);
if (!lib && !lut_attrs)
log_cmd_error("Missing required -lib option.\n");
struct Target {
Module *module;
std::vector<uint64_t> luts;
};
dict<pool<uint64_t>, std::vector<Target>> targets;
if (lib)
for (auto m : lib->modules()) {
pool<uint64_t> p_classes;
// produce a fingerprint in p_classes
int ninputs = module_inputs(m).size();
std::vector<uint64_t> luts;
if (!derive_module_luts(m, luts))
continue;
for (auto lut : luts)
p_classes.insert(p_class(ninputs, lut));
log_debug("Registered %s\n", log_id(m));
// save as a viable target
targets[p_classes].push_back(Target{m, luts});
}
auto r = saved_designs.emplace("$cellmatch", nullptr);
if (r.second)
r.first->second = new Design;
Design *map_design = r.first->second;
for (auto m : d->selected_whole_modules_warn()) {
std::vector<uint64_t> luts;
if (!derive_module_luts(m, luts))
continue;
SigSpec inputs = module_inputs(m);
SigSpec outputs = module_outputs(m);
if (lut_attrs) {
int no = 0;
for (auto bit : outputs) {
log_assert(bit.is_wire());
bit.wire->attributes[ID(p_class)] = p_class(inputs.size(), luts[no]);
bit.wire->attributes[ID(lut)] = luts[no++];
}
}
// fingerprint
pool<uint64_t> p_classes;
for (auto lut : luts)
p_classes.insert(p_class(inputs.size(), lut));
for (auto target : targets[p_classes]) {
log_debug("Candidate %s for matching to %s\n", log_id(target.module), log_id(m));
SigSpec target_inputs = module_inputs(target.module);
SigSpec target_outputs = module_outputs(target.module);
if (target_inputs.size() != inputs.size())
continue;
if (target_outputs.size() != outputs.size())
continue;
std::vector<int> input_map;
for (int i = 0; i < inputs.size(); i++)
input_map.push_back(i);
bool found_match = false;
// For each input_map
while (!found_match) {
std::vector<int> output_map;
for (int i = 0; i < outputs.size(); i++)
output_map.push_back(i);
// For each output_map
while (!found_match) {
int out_no = 0;
bool match = true;
for (auto lut : luts) {
if (permute_lut(target.luts[output_map[out_no++]], input_map) != lut) {
match = false;
break;
}
}
if (match) {
log("Module %s matches %s\n", log_id(m), log_id(target.module));
// Add target.module to map_design ("$cellmatch")
// as a techmap rule to match m and replace it with target.module
Module *map = map_design->addModule(stringf("\\_60_%s_%s", log_id(m), log_id(target.module)));
Cell *cell = map->addCell(ID::_TECHMAP_REPLACE_, target.module->name);
map->attributes[ID(techmap_celltype)] = m->name.str();
for (int i = 0; i < outputs.size(); i++) {
log_assert(outputs[i].is_wire());
Wire *w = map->addWire(outputs[i].wire->name, 1);
w->port_id = outputs[i].wire->port_id;
w->port_output = true;
log_assert(target_outputs[output_map[i]].is_wire());
cell->setPort(target_outputs[output_map[i]].wire->name, w);
}
for (int i = 0; i < inputs.size(); i++) {
log_assert(inputs[i].is_wire());
Wire *w = map->addWire(inputs[i].wire->name, 1);
w->port_id = inputs[i].wire->port_id;
w->port_input = true;
log_assert(target_inputs[input_map[i]].is_wire());
cell->setPort(target_inputs[input_map[i]].wire->name, w);
}
map->fixup_ports();
found_match = true;
}
if (!std::next_permutation(output_map.begin(), output_map.end()))
break;
}
if (!std::next_permutation(input_map.begin(), input_map.end()))
break;
}
}
}
}
} CellmatchPass;
YOSYS_NAMESPACE_END

9
passes/techmap/techmap.cc
View file

@ -336,6 +336,11 @@ struct TechmapWorker
if (c->type.begins_with("\\$"))
c->type = c->type.substr(1);
if (c->type == ID::_TECHMAP_PLACEHOLDER_ && tpl_cell->has_attribute(ID::techmap_chtype)) {
c->type = RTLIL::escape_id(tpl_cell->get_string_attribute(ID::techmap_chtype));
c->attributes.erase(ID::techmap_chtype);
}
vector<IdString> autopurge_ports;
@ -1135,6 +1140,10 @@ struct TechmapPass : public Pass {
log("new wire alias to be created and named as above but with the `_TECHMAP_REPLACE_'\n");
log("prefix also substituted.\n");
log("\n");
log("A cell with the type _TECHMAP_PLACEHOLDER_ in the map file will have its type\n");
log("changed to the content of the techmap_chtype attribute. This allows for choosing\n");
log("the cell type dynamically.\n");
log("\n");
log("See 'help extract' for a pass that does the opposite thing.\n");
log("\n");
log("See 'help flatten' for a pass that does flatten the design (which is\n");

10
techlibs/anlogic/synth_anlogic.cc
View file

@ -169,12 +169,14 @@ struct SynthAnlogicPass : public ScriptPass
if (check_label("map_ram"))
{
std::string args = "";
if (nobram)
args += " -no-auto-block";
if (nolutram)
args += " -no-auto-distributed";
if (help_mode)
args += " [-no-auto-block] [-no-auto-distributed]";
else {
if (nobram)
args += " -no-auto-block";
if (nolutram)
args += " -no-auto-distributed";
}
run("memory_libmap -lib +/anlogic/lutrams.txt -lib +/anlogic/brams.txt" + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)");
run("techmap -map +/anlogic/lutrams_map.v -map +/anlogic/brams_map.v");
}

10
techlibs/ecp5/synth_ecp5.cc
View file

@ -308,12 +308,14 @@ struct SynthEcp5Pass : public ScriptPass
if (check_label("map_ram"))
{
std::string args = "";
if (nobram)
args += " -no-auto-block";
if (nolutram)
args += " -no-auto-distributed";
if (help_mode)
args += " [-no-auto-block] [-no-auto-distributed]";
else {
if (nobram)
args += " -no-auto-block";
if (nolutram)
args += " -no-auto-distributed";
}
run("memory_libmap -lib +/ecp5/lutrams.txt -lib +/ecp5/brams.txt" + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)");
run("techmap -map +/ecp5/lutrams_map.v -map +/ecp5/brams_map.v");
}

10
techlibs/efinix/synth_efinix.cc
View file

@ -161,9 +161,13 @@ struct SynthEfinixPass : public ScriptPass
if (check_label("map_ram"))
{
std::string args = "";
if (nobram)
args += " -no-auto-block";
run("memory_libmap -lib +/efinix/brams.txt" + args);
if (help_mode)
args += " [-no-auto-block]";
else {
if (nobram)
args += " -no-auto-block";
}
run("memory_libmap -lib +/efinix/brams.txt" + args, "(-no-auto-block if -nobram)");
run("techmap -map +/efinix/brams_map.v");
}

4
techlibs/fabulous/synth_fabulous.cc
View file

@ -320,7 +320,7 @@ struct SynthPass : public ScriptPass
run("opt_clean");
}
if (check_label("map_ram")) {
if (check_label("map_ram", "(unless -noregfile)")) {
// RegFile extraction
if (!noregfile) {
run("memory_libmap -lib +/fabulous/ram_regfile.txt");
@ -342,7 +342,7 @@ struct SynthPass : public ScriptPass
}
if (check_label("map_iopad", "(if -iopad)")) {
if (iopad) {
if (iopad || help_mode) {
run("opt -full");
run("iopadmap -bits -outpad $__FABULOUS_OBUF I:PAD -inpad $__FABULOUS_IBUF O:PAD "
"-toutpad IO_1_bidirectional_frame_config_pass ~T:I:PAD "

10
techlibs/gowin/synth_gowin.cc
View file

@ -230,12 +230,14 @@ struct SynthGowinPass : public ScriptPass
if (check_label("map_ram"))
{
std::string args = "";
if (nobram)
args += " -no-auto-block";
if (nolutram)
args += " -no-auto-distributed";
if (help_mode)
args += " [-no-auto-block] [-no-auto-distributed]";
else {
if (nobram)
args += " -no-auto-block";
if (nolutram)
args += " -no-auto-distributed";
}
run("memory_libmap -lib +/gowin/lutrams.txt -lib +/gowin/brams.txt" + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)");
run("techmap -map +/gowin/lutrams_map.v -map +/gowin/brams_map.v");
}

10
techlibs/ice40/synth_ice40.cc
View file

@ -353,12 +353,14 @@ struct SynthIce40Pass : public ScriptPass
if (check_label("map_ram"))
{
std::string args = "";
if (!spram)
args += " -no-auto-huge";
if (nobram)
args += " -no-auto-block";
if (help_mode)
args += " [-no-auto-huge] [-no-auto-block]";
else {
if (!spram)
args += " -no-auto-huge";
if (nobram)
args += " -no-auto-block";
}
run("memory_libmap -lib +/ice40/brams.txt -lib +/ice40/spram.txt" + args, "(-no-auto-huge unless -spram, -no-auto-block if -nobram)");
run("techmap -map +/ice40/brams_map.v -map +/ice40/spram_map.v");
run("ice40_braminit");

10
techlibs/lattice/synth_lattice.cc
View file

@ -373,12 +373,14 @@ struct SynthLatticePass : public ScriptPass
if (check_label("map_ram"))
{
std::string args = "";
if (nobram)
args += " -no-auto-block";
if (nolutram)
args += " -no-auto-distributed";
if (help_mode)
args += " [-no-auto-block] [-no-auto-distributed]";
else {
if (nobram)
args += " -no-auto-block";
if (nolutram)
args += " -no-auto-distributed";
}
run("memory_libmap -lib +/lattice/lutrams.txt -lib +/lattice/brams" + brams_map + ".txt" + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)");
run("techmap -map +/lattice/lutrams_map.v -map +/lattice/brams_map" + brams_map + ".v");
}

10
techlibs/nexus/synth_nexus.cc
View file

@ -300,12 +300,14 @@ struct SynthNexusPass : public ScriptPass
{
std::string args = "";
args += " -no-auto-huge";
if (nobram)
args += " -no-auto-block";
if (nolutram)
args += " -no-auto-distributed";
if (help_mode)
args += " [-no-auto-block] [-no-auto-distributed]";
else {
if (nobram)
args += " -no-auto-block";
if (nolutram)
args += " -no-auto-distributed";
}
run("memory_libmap -lib +/nexus/lutrams.txt -lib +/nexus/brams.txt -lib +/nexus/lrams.txt" + args, "(-no-auto-block if -nobram, -no-auto-distributed if -nolutram)");
run("techmap -map +/nexus/lutrams_map.v -map +/nexus/brams_map.v -map +/nexus/lrams_map.v");
}

8
tests/aiger/and_to_bad_out.aag Normal file
View file

@ -0,0 +1,8 @@
aag 3 2 0 0 1 1 0 0 0
2
4
6
6 2 4
i0 pi0
i1 pi1
b0 b0

5
tests/aiger/and_to_bad_out.aig Normal file
View file

@ -0,0 +1,5 @@
aig 3 2 0 0 1 1
6
i0 pi0
i1 pi1
b0 b0

79
tests/techmap/cellmatch.ys Normal file
View file

@ -0,0 +1,79 @@
read_verilog <<EOF
module bufgate(A, Y);
input wire A;
output wire Y = A;
endmodule
module reducegate(A, B, C, X, Y);
input wire A;
input wire B;
input wire C;
output wire X = &{A, B, C};
output wire Y = |{A, B, C};
endmodule
module fagate(A, B, C, X, Y);
input wire A;
input wire B;
input wire C;
wire t1 = A ^ B;
wire t2 = A & B;
wire t3 = C & t1;
output wire X = t1 ^ C;
output wire Y = t2 | t3;
endmodule
EOF
design -stash gatelib
read_verilog <<EOF
module ripple_carry(A, B, Y);
parameter WIDTH = 4;
input wire [WIDTH-1:0] A;
input wire [WIDTH-1:0] B;
output wire [WIDTH-1:0] Y;
wire [WIDTH:0] carry;
assign carry[0] = 0;
generate
genvar i;
for (i = 0; i < WIDTH; i = i + 1) begin
FA fa(
.A(A[i]),
.B(B[i]), .Y(Y[i]),
.CI(carry[i]), .CO(carry[i + 1]),
);
end
endgenerate
endmodule
(* gate *)
module FA(A, B, CI, CO, Y);
input wire A, B, CI;
output wire CO, Y;
assign {CO, Y} = A + B + CI;
endmodule
EOF
prep
cellmatch -lib gatelib FA A:gate
design -save gold
techmap -map %$cellmatch
design -save gate
select -assert-none ripple_carry/t:FA
design -reset
design -copy-from gold -as gold ripple_carry
design -copy-from gate -as gate ripple_carry
opt_clean
equiv_make gold gate equiv
hierarchy -top equiv
flatten
opt_clean
equiv_induct equiv
equiv_status -assert

33
tests/techmap/techmap_chtype.ys Normal file
View file

@ -0,0 +1,33 @@
read_verilog <<EOT
(* techmap_celltype="foo" *)
module _80_lcu_primitive(P, G, CI, CO);
parameter WIDTH = 10;
(* force_downto *)
input wire [WIDTH-1:0] P;
(* force_downto *)
input wire [WIDTH-1:0] G;
input wire CI;
(* force_downto *)
output wire [WIDTH-1:0] CO;
(* techmap_chtype=$sformatf("LCU_%0d", WIDTH) *)
_TECHMAP_PLACEHOLDER_ #(.WIDTH(WIDTH)) _TECHMAP_REPLACE_(.P(P), .G(G), .CI(CI), .CO(CO));
endmodule
EOT
design -stash techmap
read_verilog <<EOT
module top(input [3:0] pi, input [3:0] gi, input ci, output [3:0] co);
foo #(.WIDTH(8)) suuuub(pi, gi, ci, co);
endmodule
EOT
hierarchy -auto-top
proc
opt
techmap -map %techmap
select -assert-count 1 t:LCU_8

20
tests/various/hierarchy_generate.ys Normal file
View file

@ -0,0 +1,20 @@
read_verilog -icells <<EOF
module top(input [2:0] a, input [2:0] b, output [2:0] y);
sub sub_i (.a(a[0]), .b(b[0]), .y(y[0]));
unknown_sub sub_ii (.a(a[1]), .b(b[1]), .y(y[1]));
$__dunder_sub sub_iii (.a(a[2]), .b(b[2]), .y(y[2]));
endmodule
module sub(input a, input b, output y);
assign y = a ^ b;
endmodule
EOF
hierarchy -generate unknown_sub i:a i:b o:y
hierarchy -generate $__dunder_sub i:a i:b o:y
hierarchy -generate $xor i:A i:B o:Y # this one is ignored
hierarchy -top top -check
check -assert