diff --git a/.github/PULL_REQUEST_TEMPLATE.md b/.github/PULL_REQUEST_TEMPLATE.md new file mode 100644 index 00000000000..82daf609d36 --- /dev/null +++ b/.github/PULL_REQUEST_TEMPLATE.md @@ -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._ diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml index 4a77d223429..24ae7c89883 100644 --- a/.github/workflows/codeql.yml +++ b/.github/workflows/codeql.yml @@ -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: diff --git a/.github/workflows/emcc.yml b/.github/workflows/emcc.yml index 7c6409c1be2..b883cfa0a8a 100644 --- a/.github/workflows/emcc.yml +++ b/.github/workflows/emcc.yml @@ -8,6 +8,8 @@ jobs: steps: - uses: mymindstorm/setup-emsdk@v14 - uses: actions/checkout@v4 + with: + submodules: true - name: Build run: | make config-emcc diff --git a/.github/workflows/test-build.yml b/.github/workflows/test-build.yml index 91ceb89d8fd..dc7124bb5f8 100644 --- a/.github/workflows/test-build.yml +++ b/.github/workflows/test-build.yml @@ -15,6 +15,8 @@ jobs: steps: - name: Checkout Yosys uses: actions/checkout@v4 + with: + submodules: true - name: Setup environment uses: ./.github/actions/setup-build-env diff --git a/.github/workflows/test-compile.yml b/.github/workflows/test-compile.yml index f3d4333514c..326b3afd677 100644 --- a/.github/workflows/test-compile.yml +++ b/.github/workflows/test-compile.yml @@ -30,6 +30,8 @@ jobs: steps: - name: Checkout Yosys uses: actions/checkout@v4 + with: + submodules: true - name: Setup environment uses: ./.github/actions/setup-build-env diff --git a/.github/workflows/test-verific.yml b/.github/workflows/test-verific.yml index b4383eba462..ef7fa3829d8 100644 --- a/.github/workflows/test-verific.yml +++ b/.github/workflows/test-verific.yml @@ -10,7 +10,7 @@ jobs: uses: actions/checkout@v4 with: persist-credentials: false - + submodules: true - name: Runtime environment run: | echo "procs=$(nproc)" >> $GITHUB_ENV diff --git a/.github/workflows/version.yml b/.github/workflows/version.yml index 47a7fe1a39f..f73c68bdf12 100644 --- a/.github/workflows/version.yml +++ b/.github/workflows/version.yml @@ -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 diff --git a/.github/workflows/vs.yml b/.github/workflows/vs.yml index d456336474f..f145de2d7e0 100644 --- a/.github/workflows/vs.yml +++ b/.github/workflows/vs.yml @@ -7,17 +7,19 @@ jobs: runs-on: ubuntu-latest 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 - + build: runs-on: windows-2019 needs: yosys-vcxsrc - steps: + steps: - uses: actions/download-artifact@v4 with: name: vcxsrc diff --git a/.github/workflows/wasi.yml b/.github/workflows/wasi.yml index d6d200d92c2..d65a9622799 100644 --- a/.github/workflows/wasi.yml +++ b/.github/workflows/wasi.yml @@ -7,6 +7,8 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 + with: + submodules: true - name: Build run: | WASI_SDK=wasi-sdk-19.0 diff --git a/.gitignore b/.gitignore index 6e4ffea4203..b4797d63884 100644 --- a/.gitignore +++ b/.gitignore @@ -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 diff --git a/.gitmodules b/.gitmodules new file mode 100644 index 00000000000..d88d4b1e5e9 --- /dev/null +++ b/.gitmodules @@ -0,0 +1,3 @@ +[submodule "abc"] + path = abc + url = https://github.com/YosysHQ/abc diff --git a/CHANGELOG b/CHANGELOG index f42eaca27e1..7c3ad481e9e 100644 --- a/CHANGELOG +++ b/CHANGELOG @@ -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 diff --git a/Makefile b/Makefile index c217dcb222b..e36d85848df 100644 --- a/Makefile +++ b/Makefile @@ -142,7 +142,7 @@ LIBS += -lrt endif endif -YOSYS_VER := 0.40+25 +YOSYS_VER := 0.41+0 # 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 - -# 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 + sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline c1ad377.. | wc -l`/;" Makefile + ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) # set ABCEXTERNAL = to use an external ABC instance @@ -795,41 +786,40 @@ $(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: - $(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); \ +.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 "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 "'abc' comes from a tarball. Continuing."; \ + exit 0; \ 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) -ifeq ($(ABCREV),default) -.PHONY: abc/abc-$(ABCREV)$(EXE) -.PHONY: abc/libabc-$(ABCREV).a -endif +ABC_SOURCES := $(wildcard $(YOSYS_SRC)/abc/*) -$(PROGRAM_PREFIX)yosys-abc$(EXE): abc/abc-$(ABCREV)$(EXE) - $(P) cp abc/abc-$(ABCREV)$(EXE) $(PROGRAM_PREFIX)yosys-abc$(EXE) +abc/abc$(EXE) abc/libabc.a: $(ABC_SOURCES) check-git-abc + $(P) + $(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) -$(PROGRAM_PREFIX)yosys-libabc.a: abc/libabc-$(ABCREV).a - $(P) cp abc/libabc-$(ABCREV).a $(PROGRAM_PREFIX)yosys-libabc.a +$(PROGRAM_PREFIX)yosys-abc$(EXE): abc/abc$(EXE) + $(P) cp $< $(PROGRAM_PREFIX)yosys-abc$(EXE) + +$(PROGRAM_PREFIX)yosys-libabc.a: abc/libabc.a + $(P) cp $< $(PROGRAM_PREFIX)yosys-libabc.a ifneq ($(SEED),) SEEDOPT="-S $(SEED)" @@ -1148,9 +1138,6 @@ echo-yosys-ver: echo-git-rev: @echo "$(GIT_REV)" -echo-abc-rev: - @echo "$(ABCREV)" - echo-cxx: @echo "$(CXX)" diff --git a/abc b/abc new file mode 160000 index 00000000000..237d81397fc --- /dev/null +++ b/abc @@ -0,0 +1 @@ +Subproject commit 237d81397fcc85dd3894bf1a449d2955cd3df02d diff --git a/backends/cxxrtl/cxxrtl_backend.cc b/backends/cxxrtl/cxxrtl_backend.cc index 877a829d37a..703494682a8 100644 --- a/backends/cxxrtl/cxxrtl_backend.cc +++ b/backends/cxxrtl/cxxrtl_backend.cc @@ -606,22 +606,30 @@ std::vector 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 &metadata_map) - { + void dump_serialized_metadata(const dict &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; + } + }; + 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_metadata_map(const dict &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) << ")"; + } 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"; } - f << " },\n"; - } - dec_indent(); - f << indent << "})"; + dec_indent(); + f << indent << "})"; + } } - void dump_debug_attrs(const RTLIL::AttrObject *object) + void dump_debug_attrs(const RTLIL::AttrObject *object, bool serialize = true) { dict 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 << 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 << "debug_item::" << flag; } - f << "), "; - dump_debug_attrs(wire); 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"; } } diff --git a/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h b/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h index 8546a841189..057d34cf906 100644 --- a/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h +++ b/backends/cxxrtl/runtime/cxxrtl/cxxrtl.h @@ -941,6 +941,55 @@ struct metadata { assert(value_type == DOUBLE); return double_value; } + + // Internal CXXRTL use only. + static std::map deserialize(const char *ptr) { + std::map result; + std::string name; + // Grammar: + // string ::= [^\0]+ \0 + // metadata ::= [uid] .{8} | s + // map ::= ( )* \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 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 + 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(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(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); } diff --git a/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h b/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h index b8233b007c6..9aa3e105d2c 100644 --- a/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h +++ b/backends/cxxrtl/runtime/cxxrtl/cxxrtl_replay.h @@ -512,9 +512,10 @@ class spool { 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); } diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py index e6b4088dbd7..995a714c926 100644 --- a/backends/smt2/smtbmc.py +++ b/backends/smt2/smtbmc.py @@ -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 @@ def print_msg(msg): 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 = {} - - 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) + if ywfile_hierwitness_cache is None: + ywfile_hierwitness = 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,91 +685,147 @@ 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 - max_t = -1 + return ywfile_hierwitness_cache - for t, step in inyw.steps(): - present_signals, missing = step.present_signals(inyw.sigmap) - for sig in present_signals: - bits = step[sig] - if skip_x: - bits = bits.replace('x', '?') - if not bits_re.match(bits): - raise ValueError("unsupported bit value in Yosys witness file") +def_bits_re = re.compile(r'([01]+)') - 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"] +def smt_extract_mask(smt_expr, mask): + chunks = [] + def_bits = '' - smt_bool = smt.net_width(topmod, wire["smtpath"]) == 1 + mask_index_order = mask[::-1] - offset = max(offset, 0) + for matched in def_bits_re.finditer(mask_index_order): + chunks.append(matched.span()) + def_bits += matched[0] - end = width + offset - common_offset = max(sig.offset, offset) - common_end = min(sig_end, end) - if common_end <= common_offset: - continue + if not chunks: + return - smt_expr = smt.witness_net_expr(topmod, f"s{map_steps.get(t, t)}", wire) + 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) + )) - 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) + return combined_chunks, ''.join(mask_index_order[start:end] for start, end in chunks)[::-1] - bit_slice = bits[len(bits) - (common_end - sig.offset):len(bits) - (common_offset - sig.offset)] +def smt_concat(exprs): + if not exprs: + return "" + if len(exprs) == 1: + return exprs[1] + return "(concat %s)" % ' '.join(exprs) - if bit_slice.count("?") == len(bit_slice): - continue +def ywfile_signal(sig, step, mask=None): + assert sig.width > 0 - 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) + inits, seqs, clocks, mems, smt_wires, smt_mems = ywfile_hierwitness() + sig_end = sig.offset + sig.width - smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) + output = [] - constr_assumes[t].append((inywfile, smt_constr)) + if sig.path in smt_wires: + for wire in smt_wires[sig.path]: + width, offset = wire["width"], wire["offset"] - 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_bool = smt.net_width(topmod, wire["smtpath"]) == 1 - smt_expr = smt.net_expr(topmod, f"s{map_steps.get(t, t)}", mem["smtpath"]) + offset = max(offset, 0) - 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) + end = width + offset + common_offset = max(sig.offset, offset) + common_end = min(sig_end, end) + if common_end <= common_offset: + continue - if len(bits) < width: - slice_high = sig.offset + len(bits) - 1 - smt_expr = "((_ extract %d %d) %s)" % (slice_high, sig.offset, smt_expr) + smt_expr = smt.witness_net_expr(topmod, f"s{step}", wire) - bit_slice = bits + 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 - 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) + output.append(((common_offset - sig.offset), (common_end - sig.offset), smt_expr)) - smt_constr = "(= %s #b%s)" % (smt_expr, bit_slice) - constr_assumes[t].append((inywfile, smt_constr)) - max_t = t + 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(): + present_signals, missing = step.present_signals(inyw.sigmap) + for sig in present_signals: + bits = step[sig] + if skip_x: + bits = bits.replace('x', '?') + if not bits_re.match(bits): + raise ValueError("unsupported bit value in Yosys witness file") + + smt_expr = ywfile_signal(sig, map_steps.get(t, t)) + + smt_expr, bits = smt_extract_mask(smt_expr, bits) + + smt_constr = "(= %s #b%s)" % (smt_expr, bits) + 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 diff --git a/backends/smt2/smtbmc_incremental.py b/backends/smt2/smtbmc_incremental.py index f43e878f31c..0bd280b4a48 100644 --- a/backends/smt2/smtbmc_incremental.py +++ b/backends/smt2/smtbmc_incremental.py @@ -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 @@ def __init__(self): self._witness_index = None self._yw_constraints = {} + self._define_sorts = {} def setup(self): generic_assert_map = smtbmc.get_assert_map( @@ -175,11 +176,7 @@ def expr_andor(self, expr, smt_out): 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 @@ def expr_andor(self, expr, smt_out): 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 @@ def expr_yw(self, expr, smt_out): 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 @@ def expr_smtlib(self, expr, smt_out): 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 @@ def expr_label(self, expr, smt_out): 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 @@ def expr_label(self, expr, smt_out): "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 @@ def expr(self, expr, smt_out, required_sort=None): 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 @@ def cmd_update_assumptions(self, cmd): expr = cmd.get("expr") key = cmd.get("key") - key = mkkey(key) result = smtbmc.smt.smt2_assumptions.pop(key, None) @@ -348,7 +445,7 @@ def cmd_update_assumptions(self, cmd): 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 @@ def cmd_smtlib(self, cmd): 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 @@ def cmd_ping(self, cmd): "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, diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index e32f43c60a0..5fc3ab5a424 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -160,6 +160,7 @@ def __init__(self, opts=None): 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 @@ def bv2int(self, v): 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 @@ def get_raw_unsat_assumptions(self): 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 @@ def get_unsat_assumptions(self, minimize=False): 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 @@ def wait(self): 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 @@ def __init__(self): 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 @@ def handle(self, o, a): 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