diff options
62 files changed, 1305 insertions, 508 deletions
diff --git a/.github/ISSUE_TEMPLATE/bug_report.yml b/.github/ISSUE_TEMPLATE/bug_report.yml new file mode 100644 index 000000000..ca9cb4811 --- /dev/null +++ b/.github/ISSUE_TEMPLATE/bug_report.yml @@ -0,0 +1,63 @@ +name: Bug Report +description: Report an issue or regression with Yosys +labels: ["pending-verification"] +body: + - type: markdown + attributes: + value: > + + If you have a general question, please ask it in the [Discussions](https://github.com/YosysHQ/yosys/discussions) area + or join our [IRC Channel](https://web.libera.chat/#yosys) or [Community Slack](https://join.slack.com/t/yosyshq/shared_invite/zt-1aopkns2q-EiQ97BeQDt_pwvE41sGSuA). + + + If you have a feature request, please fill out the appropriate issue form, this form is for bugs and/or regressions. + + + Please contact [YosysHQ GmbH](https://www.yosyshq.com/) if you need + commercial support for Yosys. + + - type: input + id: yosys_version + attributes: + label: Version + description: "The version of yosys this bug was encountered on." + placeholder: "The output of `yosys --version`" + validations: + required: true + + - type: markdown + attributes: + value: > + When providing steps to reproduce the issue, please ensure that the issue + is reproducible in the current git master of Yosys. Also ensure to + provide all necessary source files needed. + + + Please see [https://stackoverflow.com/help/mcve](https://stackoverflow.com/help/mcve) + for information on how to create a Minimal, Complete, and Verifiable Example + (MCVE). + + - type: textarea + id: reproduction_steps + attributes: + label: Reproduction Steps + description: "Please provide clear and concise steps to reproduce the issue." + validations: + required: true + + - type: textarea + id: expected_behavior + attributes: + label: Expected Behavior + description: "Please describe the behavior you would have expected from the tool." + validations: + required: true + + - type: textarea + id: actual_behavior + attributes: + label: Actual Behavior + description: "Please describe how the behavior you see differs from the expected behavior." + validations: + required: true + diff --git a/.github/ISSUE_TEMPLATE/config.yml b/.github/ISSUE_TEMPLATE/config.yml new file mode 100644 index 000000000..bef410a3c --- /dev/null +++ b/.github/ISSUE_TEMPLATE/config.yml @@ -0,0 +1,11 @@ +contact_links: + - name: Discussions + url: https://github.com/YosysHQ/yosys/discussions + about: "Have a question? Ask it on our discussions page!" + - name: Community Slack + url: https://join.slack.com/t/yosyshq/shared_invite/zt-1aopkns2q-EiQ97BeQDt_pwvE41sGSuA + about: "Yosys Community Slack" + - name: IRC Channel + url: https://web.libera.chat/#yosys + about: "#yosys on irc.libera.chat" + diff --git a/.github/ISSUE_TEMPLATE/feature_request.yml b/.github/ISSUE_TEMPLATE/feature_request.yml new file mode 100644 index 000000000..c521b5296 --- /dev/null +++ b/.github/ISSUE_TEMPLATE/feature_request.yml @@ -0,0 +1,26 @@ +name: Feature Request +description: "Submit a feature request for Yosys" +labels: ["feature-request"] +body: + - type: markdown + attributes: + value: > + + If you have a general question, please ask it in the [Discussions](https://github.com/YosysHQ/yosys/discussions) area + or join our [IRC Channel](https://web.libera.chat/#yosys) or [Community Slack](https://join.slack.com/t/yosyshq/shared_invite/zt-1aopkns2q-EiQ97BeQDt_pwvE41sGSuA). + + + If you have a bug report, please fill out the appropriate issue form, this form is for feature requests. + + + Please contact [YosysHQ GmbH](https://www.yosyshq.com/) if you need + commercial support or work done for Yosys. + + - type: textarea + id: feature_description + attributes: + label: Feature Description + description: "A clear and detailed description of the feature." + validations: + required: true + diff --git a/.github/issue_template.md b/.github/issue_template.md deleted file mode 100644 index c72daae3e..000000000 --- a/.github/issue_template.md +++ /dev/null @@ -1,24 +0,0 @@ -## Steps to reproduce the issue - -*Provide instructions for reproducing the issue. Make sure to include -all necessary source files. (You can simply drag&drop a .zip file into -the issue editor.)* - -Also, make sure that the issue is actually reproducable in current git -master of Yosys. - -See https://stackoverflow.com/help/mcve for some information on how to -create a Minimal, Complete, and Verifiable example (MCVE). - -Please do not waste our time with issues that lack sufficient information -to reproduce the issue easily. We will simply close those issues. - -Contact https://www.yosyshq.com/ if you need commercial support for Yosys. - -## Expected behavior - -*Please describe the behavior you would have expected from the tool.* - -## Actual behavior - -*Please describe how the behavior you see differs from the expected behavior.* diff --git a/.github/workflows/codeql.yml b/.github/workflows/codeql.yml new file mode 100644 index 000000000..57cbe5010 --- /dev/null +++ b/.github/workflows/codeql.yml @@ -0,0 +1,29 @@ +name: "CodeQL" + +on: + workflow_dispatch: + schedule: + - cron: '0 3 * * *' + +jobs: + analyze: + name: Analyze + runs-on: ubuntu-latest + steps: + - name: Install deps + run: sudo apt-get install bison flex libreadline-dev tcl-dev libffi-dev + + - name: Checkout repository + uses: actions/checkout@v3.0.0 + + - name: Initialize CodeQL + uses: github/codeql-action/init@v2 + with: + languages: cpp + queries: security-extended,security-and-quality + + - name: Build + run: make yosys -j6 + + - name: Perform CodeQL Analysis + uses: github/codeql-action/analyze@v2 @@ -2,7 +2,25 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.20 .. Yosys 0.20-dev +Yosys 0.22 .. Yosys 0.22-dev +-------------------------- + * Various + - Added YOSYS_ABORT_ON_LOG_ERROR environment variable for debugging. + Setting it to 1 causes abort() to be called when Yosys terminates with an + error message. + +Yosys 0.21 .. Yosys 0.22 +-------------------------- + * Verific support + - Added support for here-document for "verific" command (for reading + source files). + - Added support for reading EDIF files using Verific library. + (Optinally enabled with ENABLE_VERIFIC_EDIF) + + * Various + - Added tech specific utilization to "stat" json. + +Yosys 0.20 .. Yosys 0.21 -------------------------- * New commands and options - Added "formalff" pass - transforms FFs for formal verification @@ -11,6 +29,7 @@ Yosys 0.20 .. Yosys 0.20-dev present in yosys witness traces - Added option "-hdlname" to "sim" pass - preserves hiearachy when writing simulation output for a flattened design + - Addded option "-scramble-name" to "rename" pass * Formal Verification - Added $anyinit cell to directly represent FFs with an unconstrained @@ -23,6 +42,18 @@ Yosys 0.20 .. Yosys 0.20-dev conversion. - yosys-witness: Conversion from and to AIGER witness traces. + * Verific support + - Filename re-writing support for "verific" pass. + + * Various + - ABC performance improvements + - Filename re-writing added for "show -lib". + + * SmartFusion2 support + - Added $alu support + - Added SYSRESET and XTLOSC cells + - Compatible now with LiberoSoc flow + Yosys 0.19 .. Yosys 0.20 -------------------------- * New commands and options @@ -18,6 +18,7 @@ ENABLE_READLINE := 1 ENABLE_EDITLINE := 0 ENABLE_GHDL := 0 ENABLE_VERIFIC := 0 +ENABLE_VERIFIC_EDIF := 0 DISABLE_VERIFIC_EXTENSIONS := 0 DISABLE_VERIFIC_VHDL := 0 ENABLE_COVER := 1 @@ -131,7 +132,7 @@ LDLIBS += -lrt endif endif -YOSYS_VER := 0.20+45 +YOSYS_VER := 0.22+4 # Note: We arrange for .gitcommit to contain the (short) commit hash in # tarballs generated with git-archive(1) using .gitattributes. The git repo @@ -147,7 +148,7 @@ endif OBJS = kernel/version_$(GIT_REV).o bumpversion: - sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline 4fcb95e.. | wc -l`/;" Makefile + sed -i "/^YOSYS_VER := / s/+[0-9][0-9]*$$/+`git log --oneline f109fa3.. | wc -l`/;" Makefile # set 'ABCREV = default' to use abc/ as it is # @@ -155,7 +156,7 @@ bumpversion: # 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 = 20f970f +ABCREV = ab5b16e ABCPULL = 1 ABCURL ?= https://github.com/YosysHQ/abc ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1 ABC_USE_NAMESPACE=abc VERBOSE=$(Q) @@ -527,6 +528,10 @@ ifneq ($(wildcard $(VERIFIC_DIR)/vhdl),) VERIFIC_COMPONENTS += vhdl endif endif +ifeq ($(ENABLE_VERIFIC_EDIF),1) +VERIFIC_COMPONENTS += edif +CXXFLAGS += -DVERIFIC_EDIF_SUPPORT +endif ifneq ($(DISABLE_VERIFIC_EXTENSIONS),1) VERIFIC_COMPONENTS += extensions CXXFLAGS += -DYOSYSHQ_VERIFIC_EXTENSIONS diff --git a/backends/blif/blif.cc b/backends/blif/blif.cc index ba29d9090..23d1d58fc 100644 --- a/backends/blif/blif.cc +++ b/backends/blif/blif.cc @@ -512,8 +512,8 @@ struct BlifBackend : public Backend { log(" suppresses the generation of this nets without fanout.\n"); log("\n"); log("The following options can be useful when the generated file is not going to be\n"); - log("read by a BLIF parser but a custom tool. It is recommended to not name the output\n"); - log("file *.blif when any of this options is used.\n"); + log("read by a BLIF parser but a custom tool. It is recommended to not name the\n"); + log("output file *.blif when any of this options is used.\n"); log("\n"); log(" -icells\n"); log(" do not translate Yosys's internal gates to generic BLIF logic\n"); diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc index 370108444..7722d0c33 100644 --- a/backends/edif/edif.cc +++ b/backends/edif/edif.cc @@ -107,8 +107,8 @@ struct EdifBackend : public Backend { log(" constant drivers first)\n"); log("\n"); log(" -gndvccy\n"); - log(" create \"GND\" and \"VCC\" cells with \"Y\" outputs. (the default is \"G\"\n"); - log(" for \"GND\" and \"P\" for \"VCC\".)\n"); + log(" create \"GND\" and \"VCC\" cells with \"Y\" outputs. (the default is\n"); + log(" \"G\" for \"GND\" and \"P\" for \"VCC\".)\n"); log("\n"); log(" -attrprop\n"); log(" create EDIF properties for cell attributes\n"); diff --git a/backends/json/json.cc b/backends/json/json.cc index 270d762ee..1ff0a6c66 100644 --- a/backends/json/json.cc +++ b/backends/json/json.cc @@ -397,8 +397,8 @@ struct JsonBackend : public Backend { log(" \"signed\": <1 if the port is signed>\n"); log(" }\n"); log("\n"); - log("The \"offset\" and \"upto\" fields are skipped if their value would be 0."); - log("They don't affect connection semantics, and are only used to preserve original"); + log("The \"offset\" and \"upto\" fields are skipped if their value would be 0.\n"); + log("They don't affect connection semantics, and are only used to preserve original\n"); log("HDL bit indexing."); log("And <cell_details> is:\n"); log("\n"); @@ -459,8 +459,8 @@ struct JsonBackend : public Backend { log("connected to a constant driver are denoted as string \"0\", \"1\", \"x\", or\n"); log("\"z\" instead of a number.\n"); log("\n"); - log("Bit vectors (including integers) are written as string holding the binary"); - log("representation of the value. Strings are written as strings, with an appended"); + log("Bit vectors (including integers) are written as string holding the binary\n"); + log("representation of the value. Strings are written as strings, with an appended\n"); log("blank in cases of strings of the form /[01xz]* */.\n"); log("\n"); log("For example the following Verilog code:\n"); diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py index de09c040e..9af454cca 100644 --- a/backends/smt2/smtio.py +++ b/backends/smt2/smtio.py @@ -847,31 +847,28 @@ class SmtIo: return result def parse(self, stmt): - def worker(stmt): - if stmt[0] == '(': + def worker(stmt, cursor=0): + while stmt[cursor] in [" ", "\t", "\r", "\n"]: + cursor += 1 + + if stmt[cursor] == '(': expr = [] - cursor = 1 + cursor += 1 while stmt[cursor] != ')': - el, le = worker(stmt[cursor:]) + el, cursor = worker(stmt, cursor) expr.append(el) - cursor += le return expr, cursor+1 - if stmt[0] == '|': + if stmt[cursor] == '|': expr = "|" - cursor = 1 + cursor += 1 while stmt[cursor] != '|': expr += stmt[cursor] cursor += 1 expr += "|" return expr, cursor+1 - if stmt[0] in [" ", "\t", "\r", "\n"]: - el, le = worker(stmt[1:]) - return el, le+1 - expr = "" - cursor = 0 while stmt[cursor] not in ["(", ")", "|", " ", "\t", "\r", "\n"]: expr += stmt[cursor] cursor += 1 diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index aa1d4558c..e60ebc70e 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -2160,7 +2160,8 @@ struct VerilogBackend : public Backend { log(" as binary numbers.\n"); log("\n"); log(" -simple-lhs\n"); - log(" Connection assignments with simple left hand side without concatenations.\n"); + log(" Connection assignments with simple left hand side without\n"); + log(" concatenations.\n"); log("\n"); log(" -extmem\n"); log(" instead of initializing memories using assignments to individual\n"); diff --git a/frontends/rpc/rpc_frontend.cc b/frontends/rpc/rpc_frontend.cc index c12640ef0..ec3952661 100644 --- a/frontends/rpc/rpc_frontend.cc +++ b/frontends/rpc/rpc_frontend.cc @@ -383,12 +383,12 @@ struct RpcFrontend : public Pass { log(" request for the module <module-name> to be derived for a specific set of\n"); log(" parameters. <param-name> starts with \\ for named parameters, and with $\n"); log(" for unnamed parameters, which are numbered starting at 1.<param-value>\n"); - log(" for integer parameters is always specified as a binary string of unlimited\n"); - log(" precision. the <source> returned by the frontend is hygienically parsed\n"); - log(" by a built-in Yosys <frontend>, allowing the RPC frontend to return any\n"); - log(" convenient representation of the module. the derived module is cached,\n"); - log(" so the response should be the same whenever the same set of parameters\n"); - log(" is provided.\n"); + log(" for integer parameters is always specified as a binary string of\n"); + log(" unlimited precision. the <source> returned by the frontend is\n"); + log(" hygienically parsedby a built-in Yosys <frontend>, allowing the RPC\n"); + log(" frontend to return anyconvenient representation of the module. the\n"); + log(" derived module is cached,so the response should be the same whenever the\n"); + log(" same set of parameters is provided.\n"); } void execute(std::vector<std::string> args, RTLIL::Design *design) override { diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index e0dbe1b32..1b9db8772 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -53,6 +53,10 @@ USING_YOSYS_NAMESPACE #include "VhdlUnits.h" #endif +#ifdef VERIFIC_EDIF_SUPPORT +#include "edif_file.h" +#endif + #include "VerificStream.h" #include "FileSystem.h" @@ -149,6 +153,8 @@ public: } }; +YosysStreamCallBackHandler verific_read_cb; + // ================================================================== VerificImporter::VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool mode_verific, bool mode_autocover, bool mode_fullinit) : @@ -188,6 +194,36 @@ RTLIL::IdString VerificImporter::new_verific_id(Verific::DesignObj *obj) return s; } +static bool isNumber(const string& str) +{ + for (auto &c : str) { + if (std::isdigit(c) == 0) return false; + } + return true; +} + +// When used as attributes or parameter values Verific constants come already processed. +// - Real string values are already under quotes +// - Numeric values with specified width are always converted to binary +// - Rest of user defined values are handled as 32bit integers +// - There could be some internal values that are strings without quotes +// so we check if value is all digits or not +// +static const RTLIL::Const verific_const(const char *value) +{ + std::string val = std::string(value); + if (val.size()>1 && val[0]=='\"' && val.back()=='\"') + return RTLIL::Const(val.substr(1,val.size()-2)); + else + if (val.find("'b") != std::string::npos) + return RTLIL::Const::from_string(val.substr(val.find("'b") + 2)); + else + if (isNumber(val)) + return RTLIL::Const(std::stoi(val),32); + else + return RTLIL::Const(val); +} + void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj, Netlist *nl) { MapIter mi; @@ -196,14 +232,10 @@ void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &att if (obj->Linefile()) attributes[ID::src] = stringf("%s:%d", LineFile::GetFileName(obj->Linefile()), LineFile::GetLineNo(obj->Linefile())); - // FIXME: Parse numeric attributes FOREACH_ATTRIBUTE(obj, mi, attr) { if (attr->Key()[0] == ' ' || attr->Value() == nullptr) continue; - std::string val = std::string(attr->Value()); - if (val.size()>1 && val[0]=='\"' && val.back()=='\"') - val = val.substr(1,val.size()-2); - attributes[RTLIL::escape_id(attr->Key())] = RTLIL::Const(val); + attributes[RTLIL::escape_id(attr->Key())] = verific_const(attr->Value()); } if (nl) { @@ -1174,6 +1206,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::ma memory->name = RTLIL::escape_id(net->Name()); log_assert(module->count_id(memory->name) == 0); module->memories[memory->name] = memory; + import_attributes(memory->attributes, net, nl); int number_of_bits = net->Size(); int bits_in_word = number_of_bits; @@ -2323,6 +2356,9 @@ void verific_import(Design *design, const std::map<std::string,std::string> &par #ifdef VERIFIC_VHDL_SUPPORT vhdl_file::Reset(); #endif +#ifdef VERIFIC_EDIF_SUPPORT + edif_file::Reset(); +#endif Libset::Reset(); Message::Reset(); RuntimeFlags::DeleteAllFlags(); @@ -2384,6 +2420,13 @@ struct VerificPass : public Pass { log("\n"); log("\n"); #endif +#ifdef VERIFIC_EDIF_SUPPORT + log(" verific {-edif} <edif-file>..\n"); + log("\n"); + log("Load the specified EDIF files into Verific.\n"); + log("\n"); + log("\n"); +#endif log(" verific {-f|-F} [-vlog95|-vlog2k|-sv2005|-sv2009|\n"); log(" -sv2012|-sv|-formal] <command-file>\n"); log("\n"); @@ -2559,6 +2602,45 @@ struct VerificPass : public Pass { log("\n"); } #ifdef YOSYS_ENABLE_VERIFIC + std::string frontent_rewrite(std::vector<std::string> &args, int &argidx, std::vector<std::string> &tmp_files) + { + std::string filename = args[argidx++]; + //Accommodate heredocs with EOT marker spaced out from "<<", e.g. "<< EOT" vs. "<<EOT" + if (filename == "<<" && (argidx < GetSize(args))) { + filename += args[argidx++]; + } + if (filename.compare(0, 2, "<<") == 0) { + if (filename.size() <= 2) + log_error("Missing EOT marker in here document!\n"); + std::string eot_marker = filename.substr(2); + if (Frontend::current_script_file == nullptr) + filename = "<stdin>"; + std::string last_here_document; + while (1) { + std::string buffer; + char block[4096]; + while (1) { + if (fgets(block, 4096, Frontend::current_script_file == nullptr? stdin : Frontend::current_script_file) == nullptr) + log_error("Unexpected end of file in here document '%s'!\n", filename.c_str()); + buffer += block; + if (buffer.size() > 0 && (buffer[buffer.size() - 1] == '\n' || buffer[buffer.size() - 1] == '\r')) + break; + } + size_t indent = buffer.find_first_not_of(" \t\r\n"); + if (indent != std::string::npos && buffer.compare(indent, eot_marker.size(), eot_marker) == 0) + break; + last_here_document += buffer; + } + filename = make_temp_file(); + tmp_files.push_back(filename); + std::ofstream file(filename); + file << last_here_document; + } else { + rewrite_filename(filename); + } + return filename; + } + void execute(std::vector<std::string> args, RTLIL::Design *design) override { static bool set_verific_global_flags = true; @@ -2631,6 +2713,7 @@ struct VerificPass : public Pass { const char *release_str = Message::ReleaseString(); time_t release_time = Message::ReleaseDate(); char *release_tmstr = ctime(&release_time); + std::vector<std::string> tmp_files; if (release_str == nullptr) release_str = "(no release string)"; @@ -2642,8 +2725,7 @@ struct VerificPass : public Pass { int argidx = 1; std::string work = "work"; - YosysStreamCallBackHandler cb; - veri_file::RegisterCallBackVerificStream(&cb); + veri_file::RegisterCallBackVerificStream(&verific_read_cb); if (GetSize(args) > argidx && (args[argidx] == "-set-error" || args[argidx] == "-set-warning" || args[argidx] == "-set-info" || args[argidx] == "-set-ignore")) @@ -2709,6 +2791,20 @@ struct VerificPass : public Pass { } veri_file::RemoveAllLOptions(); + veri_file::AddLOption("work"); + for (int i = argidx; i < GetSize(args); i++) + { + if (args[i] == "-work" && i+1 < GetSize(args)) { + ++i; + continue; + } + if (args[i] == "-L" && i+1 < GetSize(args)) { + if (args[++i] == "work") + veri_file::RemoveAllLOptions(); + continue; + } + break; + } for (; argidx < GetSize(args); argidx++) { if (args[argidx] == "-work" && argidx+1 < GetSize(args)) { @@ -2829,8 +2925,7 @@ struct VerificPass : public Pass { veri_file::AddLibExt(ext.c_str()); while (argidx < GetSize(args)) { - std::string filename(args[argidx++]); - rewrite_filename(filename); + std::string filename = frontent_rewrite(args, argidx, tmp_files); file_names.Insert(strdup(filename.c_str())); } if (!veri_file::AnalyzeMultipleFiles(&file_names, verilog_mode, work.c_str(), veri_file::MFCU)) { @@ -2845,9 +2940,9 @@ struct VerificPass : public Pass { #ifdef VERIFIC_VHDL_SUPPORT if (GetSize(args) > argidx && args[argidx] == "-vhdl87") { vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1987").c_str()); - for (argidx++; argidx < GetSize(args); argidx++) { - std::string filename(args[argidx]); - rewrite_filename(filename); + argidx++; + while (argidx < GetSize(args)) { + std::string filename = frontent_rewrite(args, argidx, tmp_files); if (!vhdl_file::Analyze(filename.c_str(), work.c_str(), vhdl_file::VHDL_87)) log_cmd_error("Reading `%s' in VHDL_87 mode failed.\n", filename.c_str()); } @@ -2857,9 +2952,9 @@ struct VerificPass : public Pass { if (GetSize(args) > argidx && args[argidx] == "-vhdl93") { vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str()); - for (argidx++; argidx < GetSize(args); argidx++) { - std::string filename(args[argidx]); - rewrite_filename(filename); + argidx++; + while (argidx < GetSize(args)) { + std::string filename = frontent_rewrite(args, argidx, tmp_files); if (!vhdl_file::Analyze(filename.c_str(), work.c_str(), vhdl_file::VHDL_93)) log_cmd_error("Reading `%s' in VHDL_93 mode failed.\n", filename.c_str()); } @@ -2869,9 +2964,9 @@ struct VerificPass : public Pass { if (GetSize(args) > argidx && args[argidx] == "-vhdl2k") { vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_1993").c_str()); - for (argidx++; argidx < GetSize(args); argidx++) { - std::string filename(args[argidx]); - rewrite_filename(filename); + argidx++; + while (argidx < GetSize(args)) { + std::string filename = frontent_rewrite(args, argidx, tmp_files); if (!vhdl_file::Analyze(filename.c_str(), work.c_str(), vhdl_file::VHDL_2K)) log_cmd_error("Reading `%s' in VHDL_2K mode failed.\n", filename.c_str()); } @@ -2881,9 +2976,9 @@ struct VerificPass : public Pass { if (GetSize(args) > argidx && (args[argidx] == "-vhdl2008" || args[argidx] == "-vhdl")) { vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str()); - for (argidx++; argidx < GetSize(args); argidx++) { - std::string filename(args[argidx]); - rewrite_filename(filename); + argidx++; + while (argidx < GetSize(args)) { + std::string filename = frontent_rewrite(args, argidx, tmp_files); if (!vhdl_file::Analyze(filename.c_str(), work.c_str(), vhdl_file::VHDL_2008)) log_cmd_error("Reading `%s' in VHDL_2008 mode failed.\n", filename.c_str()); } @@ -2891,7 +2986,18 @@ struct VerificPass : public Pass { goto check_error; } #endif - +#ifdef VERIFIC_EDIF_SUPPORT + if (GetSize(args) > argidx && args[argidx] == "-edif") { + edif_file edif; + argidx++; + while (argidx < GetSize(args)) { + std::string filename = frontent_rewrite(args, argidx, tmp_files); + if (!edif.Read(filename.c_str())) + log_cmd_error("Reading `%s' in EDIF mode failed.\n", filename.c_str()); + } + goto check_error; + } +#endif if (argidx < GetSize(args) && args[argidx] == "-pp") { const char* filename = nullptr; @@ -3155,6 +3261,9 @@ struct VerificPass : public Pass { #ifdef VERIFIC_VHDL_SUPPORT vhdl_file::Reset(); #endif +#ifdef VERIFIC_EDIF_SUPPORT + edif_file::Reset(); +#endif Libset::Reset(); Message::Reset(); RuntimeFlags::DeleteAllFlags(); @@ -3235,6 +3344,13 @@ struct VerificPass : public Pass { cmd_error(args, argidx, "Missing or unsupported mode parameter.\n"); check_error: + if (tmp_files.size()) { + log("Removing temp files.\n"); + for(auto &fn : tmp_files) { + remove(fn.c_str()); + } + } + if (!verific_error_msg.empty()) log_error("%s\n", verific_error_msg.c_str()); @@ -3274,6 +3390,13 @@ struct ReadPass : public Pass { log("\n"); log("\n"); #endif +#ifdef VERIFIC_EDIF_SUPPORT + log(" read {-edif} <edif-file>..\n"); + log("\n"); + log("Load the specified EDIF files. (Requires Verific.)\n"); + log("\n"); + log("\n"); +#endif log(" read {-f|-F} <command-file>\n"); log("\n"); log("Load and execute the specified command file. (Requires Verific.)\n"); @@ -3367,6 +3490,17 @@ struct ReadPass : public Pass { return; } #endif +#ifdef VERIFIC_EDIF_SUPPORT + if (args[1] == "-edif") { + if (use_verific) { + args[0] = "verific"; + Pass::call(design, args); + } else { + cmd_error(args, 1, "This version of Yosys is built without Verific support.\n"); + } + return; + } +#endif if (args[1] == "-f" || args[1] == "-F") { if (use_verific) { args[0] = "verific"; diff --git a/kernel/driver.cc b/kernel/driver.cc index e52e1fb0e..6d996783e 100644 --- a/kernel/driver.cc +++ b/kernel/driver.cc @@ -33,6 +33,10 @@ #include <string.h> #include <limits.h> #include <errno.h> +#ifndef __STDC_FORMAT_MACROS +# define __STDC_FORMAT_MACROS +#endif +#include <inttypes.h> #if defined (__linux__) || defined(__FreeBSD__) # include <sys/resource.h> @@ -210,6 +214,7 @@ int main(int argc, char **argv) std::string scriptfile = ""; std::string depsfile = ""; std::string topmodule = ""; + std::string perffile = ""; bool scriptfile_tcl = false; bool print_banner = true; bool print_stats = true; @@ -353,7 +358,7 @@ int main(int argc, char **argv) } int opt; - while ((opt = getopt(argc, argv, "MXAQTVSgm:f:Hh:b:o:p:l:L:qv:tds:c:W:w:e:r:D:P:E:x:")) != -1) + while ((opt = getopt(argc, argv, "MXAQTVSgm:f:Hh:b:o:p:l:L:qv:tds:c:W:w:e:r:D:P:E:x:B:")) != -1) { switch (opt) { @@ -488,6 +493,9 @@ int main(int argc, char **argv) case 'x': log_experimentals_ignored.insert(optarg); break; + case 'B': + perffile = optarg; + break; default: fprintf(stderr, "Run '%s -h' for help.\n", argv[0]); exit(1); @@ -674,6 +682,29 @@ int main(int argc, char **argv) } log("%s\n", out_count ? "" : " no commands executed"); } + if(!perffile.empty()) + { + FILE *f = fopen(perffile.c_str(), "wt"); + if (f == nullptr) + log_error("Can't open performance log file for writing: %s\n", strerror(errno)); + + fprintf(f, "{\n"); + fprintf(f, " \"generator\": \"%s\",\n", yosys_version_str); + fprintf(f, " \"total_ns\": %" PRIu64 ",\n", total_ns); + fprintf(f, " \"passes\": {"); + + bool first = true; + for (auto it = timedat.rbegin(); it != timedat.rend(); it++) { + if (!first) + fprintf(f, ","); + fprintf(f, "\n \"%s\": {\n", std::get<2>(*it).c_str()); + fprintf(f, " \"runtime_ns\": %" PRIu64 ",\n", std::get<0>(*it)); + fprintf(f, " \"num_calls\": %u\n", std::get<1>(*it)); + fprintf(f, " }"); + first = false; + } + fprintf(f, "\n }\n}\n"); + } } #if defined(YOSYS_ENABLE_COVER) && (defined(__linux__) || defined(__FreeBSD__)) @@ -724,4 +755,3 @@ int main(int argc, char **argv) } #endif /* EMSCRIPTEN */ - diff --git a/kernel/hashlib.h b/kernel/hashlib.h index 0c9f25287..af2827153 100644 --- a/kernel/hashlib.h +++ b/kernel/hashlib.h @@ -189,7 +189,7 @@ inline int hashtable_size(int min_size) if (p >= min_size) return p; if (sizeof(int) == 4) - throw std::length_error("hash table exceeded maximum size. use a ILP64 abi for larger tables."); + throw std::length_error("hash table exceeded maximum size.\nDesign is likely too large for yosys to handle, if possible try not to flatten the design."); for (auto p : zero_and_some_primes) if (100129 * p > min_size) return 100129 * p; diff --git a/kernel/log.cc b/kernel/log.cc index 4403dd0c7..af8c422b8 100644 --- a/kernel/log.cc +++ b/kernel/log.cc @@ -352,6 +352,9 @@ static void logv_error_with_prefix(const char *prefix, log_error_atexit(); YS_DEBUGTRAP_IF_DEBUGGING; + const char *e = getenv("YOSYS_ABORT_ON_LOG_ERROR"); + if (e && atoi(e)) + abort(); #ifdef EMSCRIPTEN log_files = backup_log_files; diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index bc25c35cd..671fabb81 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -23,27 +23,29 @@ library to a target architecture. if no -script parameter is given, the following scripts are used: for -liberty/-genlib without -constr: - strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; - &nf {D}; &put + strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; + &get -n; &dch -f; &nf {D}; &put for -liberty/-genlib with -constr: - strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; - &nf {D}; &put; buffer; upsize {D}; dnsize {D}; stime -p + strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; + &get -n; &dch -f; &nf {D}; &put; buffer; upsize {D}; + dnsize {D}; stime -p for -lut/-luts (only one LUT size): - strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2; - lutpack {S} + strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; + dch -f; if; mfs2; lutpack {S} for -lut/-luts (different LUT sizes): - strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2 + strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; + dch -f; if; mfs2 for -sop: - strash; ifraig; scorr; dc2; dretime; strash; dch -f; - cover {I} {P} + strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; + dch -f; cover {I} {P} otherwise: - strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; - &nf {D}; &put + strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; + &get -n; &dch -f; &nf {D}; &put -fast use different default scripts that are slightly faster (at the cost @@ -125,7 +127,8 @@ library to a target architecture. NMUX, AOI3, OAI3, AOI4, OAI4. (The NOT gate is always added to this list automatically.) - The following aliases can be used to reference common sets of gate types: + The following aliases can be used to reference common sets of gate + types: simple: AND OR XOR MUX cmos2: NAND NOR cmos3: NAND NOR AOI3 OAI3 @@ -169,8 +172,8 @@ library to a target architecture. -dress run the 'dress' command after all other ABC commands. This aims to - preserve naming by an equivalence check between the original and post-ABC - netlists (experimental). + preserve naming by an equivalence check between the original and + post-ABC netlists (experimental). When no target cell library is specified the Yosys standard cell library is loaded into ABC before the ABC script is executed. @@ -190,8 +193,8 @@ you want to use ABC to convert your design into another format. \begin{lstlisting}[numbers=left,frame=single] abc9 [options] [selection] -This script pass performs a sequence of commands to facilitate the use of the ABC -tool [1] for technology mapping of the current design to a target FPGA +This script pass performs a sequence of commands to facilitate the use of the +ABC tool [1] for technology mapping of the current design to a target FPGA architecture. Only fully-selected modules are supported. -run <from_label>:<to_label> @@ -337,8 +340,8 @@ externally if you want to use ABC to convert your design into another format. This pass uses the ABC tool [1] for technology mapping of the top module -(according to the (* top *) attribute or if only one module is currently selected) -to a target FPGA architecture. +(according to the (* top *) attribute or if only one module is currently +selected) to a target FPGA architecture. -exe <command> use the specified command instead of "<yosys-bindir>/yosys-abc" to execute ABC. @@ -413,14 +416,14 @@ mapping, and is expected to be called in conjunction with other operations from the `abc9' script pass. Only fully-selected modules are supported. -check - check that the design is valid, e.g. (* abc9_box_id *) values are unique, - (* abc9_carry *) is only given for one input/output port, etc. + check that the design is valid, e.g. (* abc9_box_id *) values are + unique, (* abc9_carry *) is only given for one input/output port, etc. -prep_hier derive all used (* abc9_box *) or (* abc9_flop *) (if -dff option) whitebox modules. with (* abc9_flop *) modules, only those containing - $dff/$_DFF_[NP]_ cells with zero initial state -- due to an ABC limitation - -- will be derived. + $dff/$_DFF_[NP]_ cells with zero initial state -- due to an ABC + limitation -- will be derived. -prep_bypass create techmap rules in the '$abc9_map' and '$abc9_unmap' designs for @@ -438,33 +441,35 @@ the `abc9' script pass. Only fully-selected modules are supported. -prep_dff_submod within (* abc9_flop *) modules, rewrite all edge-sensitive path declarations and $setup() timing checks ($specify3 and $specrule cells) - that share a 'DST' port with the $_DFF_[NP]_.Q port from this 'Q' port to - the DFF's 'D' port. this is to prepare such specify cells to be moved + that share a 'DST' port with the $_DFF_[NP]_.Q port from this 'Q' port + to the DFF's 'D' port. this is to prepare such specify cells to be moved into the flop box. -prep_dff_unmap - populate the '$abc9_unmap' design with techmap rules for mapping *_$abc9_flop - cells back into their derived cell types (where the rules created by - -prep_hier will then map back to the original cell with parameters). + populate the '$abc9_unmap' design with techmap rules for mapping + *_$abc9_flop cells back into their derived cell types (where the rules + created by -prep_hier will then map back to the original cell with + parameters). -prep_delays insert `$__ABC9_DELAY' blackbox cells into the design to account for certain required times. -break_scc - for an arbitrarily chosen cell in each unique SCC of each selected module - (tagged with an (* abc9_scc_id = <int> *) attribute) interrupt all wires - driven by this cell's outputs with a temporary $__ABC9_SCC_BREAKER cell - to break the SCC. + for an arbitrarily chosen cell in each unique SCC of each selected + module (tagged with an (* abc9_scc_id = <int> *) attribute) interrupt + all wires driven by this cell's outputs with a temporary + $__ABC9_SCC_BREAKER cell to break the SCC. -prep_xaiger prepare the design for XAIGER output. this includes computing the - topological ordering of ABC9 boxes, as well as preparing the '$abc9_holes' - design that contains the logic behaviour of ABC9 whiteboxes. + topological ordering of ABC9 boxes, as well as preparing the + '$abc9_holes' design that contains the logic behaviour of ABC9 + whiteboxes. -dff - consider flop cells (those instantiating modules marked with (* abc9_flop *)) - during -prep_{delays,xaiger,box}. + consider flop cells (those instantiating modules marked with + (* abc9_flop *)) during -prep_{delays,xaiger,box}. -prep_lut <maxlut> pre-compute the lut library by analysing all modules marked with @@ -482,8 +487,8 @@ the `abc9' script pass. Only fully-selected modules are supported. -reintegrate for each selected module, re-intergrate the module '<module-name>$abc9' - by first recovering ABC9 boxes, and then stitching in the remaining primary - inputs and outputs. + by first recovering ABC9 boxes, and then stitching in the remaining + primary inputs and outputs. \end{lstlisting} \section{add -- add objects to the design} @@ -686,10 +691,10 @@ This pass transforms $bmux cells to trees of $mux cells. This command minimizes the current design that is known to crash Yosys with the given script into a smaller testcase. It does this by removing an arbitrary part -of the design and recursively invokes a new Yosys process with this modified design -and the same script, repeating these steps while it can find a smaller design that -still causes a crash. Once this command finishes, it replaces the current design -with the smallest testcase it was able to produce. +of the design and recursively invokes a new Yosys process with this modified +design and the same script, repeating these steps while it can find a smaller +design that still causes a crash. Once this command finishes, it replaces the +current design with the smallest testcase it was able to produce. In order to save the reduced testcase you must write this out to a file with another command after `bugpoint` like `write_rtlil` or `write_verilog`. @@ -807,8 +812,8 @@ Options: chformal [types] [mode] [options] [selection] Make changes to the formal constraints of the design. The [types] options -the type of constraint to operate on. If none of the following options are given, -the command will operate on all constraint types: +the type of constraint to operate on. If none of the following options are +given, the command will operate on all constraint types: -assert $assert cells, representing assert(...) constraints -assume $assume cells, representing assume(...) constraints @@ -997,12 +1002,12 @@ of JSON. Frontend responds with data or error message by replying with exactly request for the module <module-name> to be derived for a specific set of parameters. <param-name> starts with \ for named parameters, and with $ for unnamed parameters, which are numbered starting at 1.<param-value> - for integer parameters is always specified as a binary string of unlimited - precision. the <source> returned by the frontend is hygienically parsed - by a built-in Yosys <frontend>, allowing the RPC frontend to return any - convenient representation of the module. the derived module is cached, - so the response should be the same whenever the same set of parameters - is provided. + for integer parameters is always specified as a binary string of + unlimited precision. the <source> returned by the frontend is + hygienically parsedby a built-in Yosys <frontend>, allowing the RPC + frontend to return anyconvenient representation of the module. the + derived module is cached,so the response should be the same whenever the + same set of parameters is provided. \end{lstlisting} \section{connwrappers -- match width of input-output port pairs} @@ -1294,7 +1299,9 @@ and can be specified as allowed targets): - $_DLATCHSR_[NP][NP][NP]_ The following transformations are performed by this pass: -- upconversion from a less capable cell to a more capable cell, if the less capable cell is not supported (eg. dff -> dffe, or adff -> dffsr) + +- upconversion from a less capable cell to a more capable cell, if the less + capable cell is not supported (eg. dff -> dffe, or adff -> dffsr) - unmapping FFs with clock enable (due to unsupported cell type or -mince) - unmapping FFs with sync reset (due to unsupported cell type or -minsrst) - adding inverters on the control pins (due to unsupported polarity) @@ -1307,7 +1314,8 @@ The following transformations are performed by this pass: dff + adff + dlatch + mux - emulating adlatch when the (reset, init) value combination is unsupported by - dlatch + adlatch + dlatch + mux -If the pass is unable to realize a given cell type (eg. adff when only plain dffis available), an error is raised. +If the pass is unable to realize a given cell type (eg. adff when only plain dff +is available), an error is raised. \end{lstlisting} \section{dfflibmap -- technology mapping of flip-flops} @@ -1330,7 +1338,8 @@ types that are already of exactly the right type to match the target cells, leaving remaining internal cells untouched. When called with -info, this command will only print the target cell -list, along with their associated internal cell types, and the argumentsthat would be passed to the dfflegalize pass. The design will not be +list, along with their associated internal cell types, and the arguments +that would be passed to the dfflegalize pass. The design will not be changed. \end{lstlisting} @@ -1340,8 +1349,8 @@ changed. dffunmap [options] [selection] This pass transforms FF types with clock enable and/or synchronous reset into -their base type (with neither clock enable nor sync reset) by emulating the clock -enable and synchronous reset with multiplexers on the cell input. +their base type (with neither clock enable nor sync reset) by emulating the +clock enable and synchronous reset with multiplexers on the cell input. -ce-only unmap only clock enables, leave synchronous resets alone. @@ -1690,8 +1699,8 @@ inputs. Execute a command in the operating system shell. All supplied arguments are concatenated and passed as a command to popen(3). Whitespace is not guaranteed -to be preserved, even if quoted. stdin and stderr are not connected, while stdout is -logged unless the "-q" option is specified. +to be preserved, even if quoted. stdin and stderr are not connected, while +stdout is logged unless the "-q" option is specified. -q @@ -2036,6 +2045,49 @@ model. Set clock for init sequences \end{lstlisting} +\section{formalff -- prepare FFs for formal} +\label{cmd:formalff} +\begin{lstlisting}[numbers=left,frame=single] + formalff [options] [selection] + +This pass transforms clocked flip-flops to prepare a design for formal +verification. If a design contains latches and/or multiple different clocks run +the async2sync or clk2fflogic passes before using this pass. + + -clk2ff + Replace all clocked flip-flops with $ff cells that use the implicit + global clock. This assumes, without checking, that the design uses a + single global clock. If that is not the case, the clk2fflogic pass + should be used instead. + + -ff2anyinit + Replace uninitialized bits of $ff cells with $anyinit cells. An + $anyinit cell behaves exactly like an $ff cell with an undefined + initialization value. The difference is that $anyinit inhibits + don't-care optimizations and is used to track solver-provided values + in witness traces. + + If combined with -clk2ff this also affects newly created $ff cells. + + -anyinit2ff + Replaces $anyinit cells with uninitialized $ff cells. This performs the + reverse of -ff2anyinit and can be used, before running a backend pass + (or similar) that is not yet aware of $anyinit cells. + + Note that after running -anyinit2ff, in general, performing don't-care + optimizations is not sound in a formal verification setting. + + -fine + Emit fine-grained $_FF_ cells instead of coarse-grained $ff cells for + -anyinit2ff. Cannot be combined with -clk2ff or -ff2anyinit. + + -setundef + Find FFs with undefined initialization values for which changing the + initialization does not change the observable behavior and initialize + them. For -ff2anyinit, this reduces the number of generated $anyinit + cells that drive wires with private names. +\end{lstlisting} + \section{freduce -- perform functional reduction} \label{cmd:freduce} \begin{lstlisting}[numbers=left,frame=single] @@ -2227,8 +2279,8 @@ one-hot encoding and binary encoding is supported. \begin{lstlisting}[numbers=left,frame=single] fst2tb [options] [top-level] -This command generates testbench for the circuit using the given top-level module -and simulus signal from FST file +This command generates testbench for the circuit using the given top-level +module and simulus signal from FST file -tb <name> generated testbench name. @@ -2271,44 +2323,46 @@ and CC_L2T5 cells as created by LUT tree mapping. \begin{lstlisting}[numbers=left,frame=single] glift <command> [options] [selection] -Augments the current or specified module with gate-level information flow tracking -(GLIFT) logic using the "constructive mapping" approach. Also can set up QBF-SAT -optimization problems in order to optimize GLIFT models or trade off precision and -complexity. +Augments the current or specified module with gate-level information flow +tracking (GLIFT) logic using the "constructive mapping" approach. Also can set +up QBF-SAT optimization problems in order to optimize GLIFT models or trade off +precision and complexity. Commands: -create-precise-model - Replaces the current or specified module with one that has corresponding "taint" - inputs, outputs, and internal nets along with precise taint tracking logic. - For example, precise taint tracking logic for an AND gate is: + Replaces the current or specified module with one that has corresponding + "taint" inputs, outputs, and internal nets along with precise taint + tracking logic. For example, precise taint tracking logic for an AND gate + is: y_t = a & b_t | b & a_t | a_t & b_t -create-imprecise-model - Replaces the current or specified module with one that has corresponding "taint" - inputs, outputs, and internal nets along with imprecise "All OR" taint tracking - logic: + Replaces the current or specified module with one that has corresponding + "taint" inputs, outputs, and internal nets along with imprecise "All OR" + taint tracking logic: y_t = a_t | b_t -create-instrumented-model - Replaces the current or specified module with one that has corresponding "taint" - inputs, outputs, and internal nets along with 4 varying-precision versions of taint - tracking logic. Which version of taint tracking logic is used for a given gate is - determined by a MUX selected by an $anyconst cell. By default, unless the - `-no-cost-model` option is provided, an additional wire named `__glift_weight` with - the `keep` and `minimize` attributes is added to the module along with pmuxes and - adders to calculate a rough estimate of the number of logic gates in the GLIFT model - given an assignment for the $anyconst cells. The four versions of taint tracking logic - for an AND gate are: - y_t = a & b_t | b & a_t | a_t & b_t (like `-create-precise-model`) + Replaces the current or specified module with one that has corresponding + "taint" inputs, outputs, and internal nets along with 4 varying-precision + versions of taint tracking logic. Which version of taint tracking logic is + used for a given gate is determined by a MUX selected by an $anyconst cell. + By default, unless the `-no-cost-model` option is provided, an additional + wire named `__glift_weight` with the `keep` and `minimize` attributes is + added to the module along with pmuxes and adders to calculate a rough + estimate of the number of logic gates in the GLIFT model given an assignment + for the $anyconst cells. The four versions of taint tracking logic for an + AND gate are: + y_t = a & b_t | b & a_t | a_t & b_t (like `-create-precise-model`) y_t = a_t | a & b_t y_t = b_t | b & a_t - y_t = a_t | b_t (like `-create-imprecise-model`) + y_t = a_t | b_t (like `-create-imprecise-model`) Options: @@ -2318,27 +2372,30 @@ Options: (default: label constants as un-tainted) -keep-outputs - Do not remove module outputs. Taint tracking outputs will appear in the module ports - alongside the orignal outputs. + Do not remove module outputs. Taint tracking outputs will appear in the + module ports alongside the orignal outputs. (default: original module outputs are removed) -simple-cost-model - Do not model logic area. Instead model the number of non-zero assignments to $anyconsts. - Taint tracking logic versions vary in their size, but all reduced-precision versions are - significantly smaller than the fully-precise version. A non-zero $anyconst assignment means - that reduced-precision taint tracking logic was chosen for some gate. - Only applicable in combination with `-create-instrumented-model`. - (default: use a complex model and give that wire the "keep" and "minimize" attributes) + Do not model logic area. Instead model the number of non-zero assignments to + $anyconsts. Taint tracking logic versions vary in their size, but all + reduced-precision versions are significantly smaller than the fully-precise + version. A non-zero $anyconst assignment means that reduced-precision taint + tracking logic was chosen for some gate. Only applicable in combination with + `-create-instrumented-model`. (default: use a complex model and give that + wire the "keep" and "minimize" attributes) -no-cost-model - Do not model taint tracking logic area and do not create a `__glift_weight` wire. - Only applicable in combination with `-create-instrumented-model`. - (default: model area and give that wire the "keep" and "minimize" attributes) + Do not model taint tracking logic area and do not create a `__glift_weight` + wire. Only applicable in combination with `-create-instrumented-model`. + (default: model area and give that wire the "keep" and "minimize" + attributes) -instrument-more - Allow choice from more versions of (even simpler) taint tracking logic. A total - of 8 versions of taint tracking logic will be added per gate, including the 4 - versions from `-create-instrumented-model` and these additional versions: + Allow choice from more versions of (even simpler) taint tracking logic. A + total of 8 versions of taint tracking logic will be added per gate, + including the 4 versions from `-create-instrumented-model` and these + additional versions: y_t = a_t y_t = b_t @@ -2657,8 +2714,9 @@ scripts, because the TCL command "puts" only goes to stdout but not to logfiles. -stdout - Print the output to stdout too. This is useful when all Yosys is executed - with a script and the -q (quiet operation) argument to notify the user. + Print the output to stdout too. This is useful when all Yosys is + executed with a script and the -q (quiet operation) argument to notify + the user. -stderr Print the output to stderr too. @@ -2830,7 +2888,8 @@ and a value greater than 1 means configurable. All groups with the same value greater than 1 share the same configuration bit. Using the same bram name in different bram blocks will create different variants -of the bram. Verilog configuration parameters for the bram are created as needed. +of the bram. Verilog configuration parameters for the bram are created as +needed. It is also possible to create variants by repeating statements in the bram block and appending '@<label>' to the individual statements. @@ -2902,8 +2961,8 @@ memory cells. \begin{lstlisting}[numbers=left,frame=single] memory_dff [-no-rw-check] [selection] -This pass detects DFFs at memory read ports and merges them into the memory port. -I.e. it consumes an asynchronous memory port and the flip-flops at its +This pass detects DFFs at memory read ports and merges them into the memory +port. I.e. it consumes an asynchronous memory port and the flip-flops at its interface and yields a synchronous memory port. -no-rw-check @@ -2966,6 +3025,12 @@ pass to word-wide DFFs and address decoders. -keepdc when mapping ROMs, keep x-bits shared across read ports. + + -formal + map memories for a global clock based formal verification flow. + This implies -keepdc, uses $ff cells for ROMs and sets hdlname + attributes. It also has limited support for async write ports + as generated by clk2fflogic. \end{lstlisting} \section{memory\_memx -- emulate vlog sim behavior for mem ports} @@ -3006,8 +3071,8 @@ The following methods are used to consolidate the number of memory ports: - When multiple write ports access the same address then this is converted to a single write port with a more complex data and/or enable logic path. - - When multiple read or write ports access adjacent aligned addresses, they are - merged to a single wide read or write port. This transformation can be + - When multiple read or write ports access adjacent aligned addresses, they + are merged to a single wide read or write port. This transformation can be disabled with the "-nowiden" option. - When multiple write ports are never accessed at the same time (a SAT @@ -3276,14 +3341,17 @@ overall gate count of the circuit opt_dff [-nodffe] [-nosdff] [-keepdc] [-sat] [selection] This pass converts flip-flops to a more suitable type by merging clock enables -and synchronous reset multiplexers, removing unused control inputs, or potentially -removes the flip-flop altogether, converting it to a constant driver. +and synchronous reset multiplexers, removing unused control inputs, or +potentially removes the flip-flop altogether, converting it to a constant +driver. -nodffe - disables dff -> dffe conversion, and other transforms recognizing clock enable + disables dff -> dffe conversion, and other transforms recognizing clock + enable -nosdff - disables dff -> sdff conversion, and other transforms recognizing sync resets + disables dff -> sdff conversion, and other transforms recognizing sync + resets -simple-dffe only enables clock enable recognition transform for obvious cases @@ -3804,11 +3872,11 @@ This pass converts switches into read-only memories when appropriate. \begin{lstlisting}[numbers=left,frame=single] qbfsat [options] [selection] -This command solves an "exists-forall" 2QBF-SAT problem defined over the currently -selected module. Existentially-quantified variables are declared by assigning a wire -"$anyconst". Universally-quantified variables may be explicitly declared by assigning -a wire "$allconst", but module inputs will be treated as universally-quantified -variables by default. +This command solves an "exists-forall" 2QBF-SAT problem defined over the +currently selected module. Existentially-quantified variables are declared by +assigning a wire "$anyconst". Universally-quantified variables may be +explicitly declared by assigning a wire "$allconst", but module inputs will be +treated as universally-quantified variables by default. -nocleanup Do not delete temporary files and directories. Useful for debugging. @@ -3817,23 +3885,25 @@ variables by default. Pass the --dump-smt2 option to yosys-smtbmc. -assume-outputs - Add an "$assume" cell for the conjunction of all one-bit module output wires. + Add an "$assume" cell for the conjunction of all one-bit module output + wires. -assume-negative-polarity - When adding $assume cells for one-bit module output wires, assume they are - negative polarity signals and should always be low, for example like the - miters created with the `miter` command. + When adding $assume cells for one-bit module output wires, assume they + are negative polarity signals and should always be low, for example like + the miters created with the `miter` command. -nooptimize - Ignore "\minimize" and "\maximize" attributes, do not emit "(maximize)" or - "(minimize)" in the SMT-LIBv2, and generally make no attempt to optimize anything. + Ignore "\minimize" and "\maximize" attributes, do not emit + "(maximize)" or "(minimize)" in the SMT-LIBv2, and generally make no + attempt to optimize anything. -nobisection - If a wire is marked with the "\minimize" or "\maximize" attribute, do not - attempt to optimize that value with the default iterated solving and threshold - bisection approach. Instead, have yosys-smtbmc emit a "(minimize)" or "(maximize)" - command in the SMT-LIBv2 output and hope that the solver supports optimizing - quantified bitvector problems. + If a wire is marked with the "\minimize" or "\maximize" attribute, + do not attempt to optimize that value with the default iterated solving + and threshold bisection approach. Instead, have yosys-smtbmc emit a + "(minimize)" or "(maximize)" command in the SMT-LIBv2 output and + hope that the solver supports optimizing quantified bitvector problems. -solver <solver> Use a particular solver. Choose one of: "z3", "yices", and "cvc4". @@ -3863,12 +3933,14 @@ variables by default. corresponding constant value from the model produced by the solver. -specialize-from-file <solution file> - Do not run the solver, but instead only attempt to replace each "$anyconst" - cell in the current module with a constant value provided by the specified file. + Do not run the solver, but instead only attempt to replace each + "$anyconst" cell in the current module with a constant value provided + by the specified file. -write-solution <solution file> - If the problem is satisfiable, write the corresponding constant value for each - "$anyconst" cell from the model produced by the solver to the specified file. + If the problem is satisfiable, write the corresponding constant value + for each "$anyconst" cell from the model produced by the solver to the + specified file. \end{lstlisting} \section{qwp -- quadratic wirelength placer} @@ -4261,6 +4333,14 @@ The character % in the pattern is replaced with a integer number. The default pattern is '_%_'. + rename -witness + +Assigns auto-generated names to all $any*/$all* output wires and containing +cells that do not have a public name. This ensures that, during formal +verification, a solver-found trace can be fully specified using a public +hierarchical names. + + rename -hide [selection] Assign private names (the ones with $-prefix) to all selected wires and cells @@ -4270,6 +4350,13 @@ with public names. This ignores all selected ports. rename -top new_name Rename top module. + + + rename -scramble-name [-seed <seed>] [selection] + +Assign randomly-generated names to all selected wires and cells. The seed option +can be used to change the random number generator seed from the default, but it +must be non-zero. \end{lstlisting} \section{rmports -- remove module ports with no connections} @@ -4520,7 +4607,8 @@ design. Options: copy the value of the first identifier to the second identifier. -assert <identifier> <value> - assert that the entry for the given identifier is set to the given value. + assert that the entry for the given identifier is set to the given + value. -assert-set <identifier> assert that the entry for the given identifier exists. @@ -4657,7 +4745,8 @@ Pushing (selecting) object when in -module mode: <obj_pattern> select the specified object(s) from the current module -By default, patterns will not match black/white-box modules or theircontents. To include such objects, prefix the pattern with '='. +By default, patterns will not match black/white-box modules or their +contents. To include such objects, prefix the pattern with '='. A <mod_pattern> can be a module name, wildcard expression (*, ?, [..]) matching module names, or one of the following: @@ -5069,6 +5158,10 @@ This command simulates the circuit using the given top-level module. write the simulation results to an AIGER witness file (requires a *.aim file via -map) + -hdlname + use the hdlname attribute when writing simulation results + (preserves hierarchy in a flattened design) + -x ignore constant x outputs in simulation file. @@ -5109,7 +5202,8 @@ This command simulates the circuit using the given top-level module. writeback mode: use final simulation state as new init state -r - read simulation results file (file formats supported: FST, VCD, AIW and WIT) + read simulation results file + File formats supported: FST, VCD, AIW and WIT VCD support requires vcd2fst external tool to be present -map <filename> @@ -5157,7 +5251,8 @@ primitives. The following internal cell types are mapped by this pass: $not, $pos, $and, $or, $xor, $xnor $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool $logic_not, $logic_and, $logic_or, $mux, $tribuf - $sr, $ff, $dff, $dffe, $dffsr, $dffsre, $adff, $adffe, $aldff, $aldffe, $sdff, $sdffe, $sdffce, $dlatch, $adlatch, $dlatchsr + $sr, $ff, $dff, $dffe, $dffsr, $dffsre, $adff, $adffe, $aldff, $aldffe, $sdff, + $sdffe, $sdffce, $dlatch, $adlatch, $dlatchsr \end{lstlisting} \section{splice -- create explicit splicing cells} @@ -5253,6 +5348,10 @@ design. -width annotate internal cell types with their word width. e.g. $add_8 for an 8 bit wide $add cell. + + -json + output the statistics in a machine-readable JSON format. + this is output to the console; use "tee" to output to a file. \end{lstlisting} \section{submod -- moving part of a module to a new submodule} @@ -5282,8 +5381,8 @@ or memories. -hidden instead of creating submodule ports with public names, create ports with - private names so that a subsequent 'flatten; clean' call will restore the - original module with original public names. + private names so that a subsequent 'flatten; clean' call will restore + the original module with original public names. \end{lstlisting} \section{supercover -- add hi/lo cover cells for each wire bit} @@ -6333,8 +6432,8 @@ The following commands are executed by this synthesis command: This command runs synthesis for iCE40 FPGAs. -device < hx | lp | u > - relevant only for '-abc9' flow, optimise timing for the specified device. - default: hx + relevant only for '-abc9' flow, optimise timing for the specified + device. default: hx -top <module> use the specified module as top module @@ -6517,21 +6616,22 @@ This command runs synthesis for Intel FPGAs. -family <max10 | cyclone10lp | cycloneiv | cycloneive> generate the synthesis netlist for the specified family. MAX10 is the default target if no family argument specified. - For Cyclone IV GX devices, use cycloneiv argument; for Cyclone IV E, use cycloneive. - For Cyclone V and Cyclone 10 GX, use the synth_intel_alm backend instead. + For Cyclone IV GX devices, use cycloneiv argument; for Cyclone IV E, use + cycloneive. For Cyclone V and Cyclone 10 GX, use the synth_intel_alm + backend instead. -top <module> use the specified module as top module (default='top') -vqm <file> - write the design to the specified Verilog Quartus Mapping File. Writing of an - output file is omitted if this parameter is not specified. + write the design to the specified Verilog Quartus Mapping File. Writing + of an output file is omitted if this parameter is not specified. Note that this backend has not been tested and is likely incompatible with recent versions of Quartus. -vpr <file> - write BLIF files for VPR flow experiments. The synthesized BLIF output file is not - compatible with the Quartus flow. Writing of an + write BLIF files for VPR flow experiments. The synthesized BLIF output + file is not compatible with the Quartus flow. Writing of an output file is omitted if this parameter is not specified. -run <from_label>:<to_label> @@ -6627,20 +6727,24 @@ This command runs synthesis for ALM-based Intel FPGAs. -family <family> target one of: "cyclonev" - Cyclone V (default) - "arriav" - Arria V (non-GZ) "cyclone10gx" - Cyclone 10GX + "arriav" - Arria V (non-GZ) + "cyclone10gx" - Cyclone 10GX -vqm <file> - write the design to the specified Verilog Quartus Mapping File. Writing of an - output file is omitted if this parameter is not specified. Implies -quartus. + write the design to the specified Verilog Quartus Mapping File. Writing + of an output file is omitted if this parameter is not specified. Implies + -quartus. -noflatten - do not flatten design before synthesis; useful for per-module area statistics + do not flatten design before synthesis; useful for per-module area + statistics -quartus output a netlist using Quartus cells instead of MISTRAL_* cells -dff - pass DFFs to ABC to perform sequential logic optimisations (EXPERIMENTAL) + pass DFFs to ABC to perform sequential logic optimisations + (EXPERIMENTAL) -run <from_label>:<to_label> only run the commands between the labels (see below). an empty @@ -7013,8 +7117,8 @@ This command runs synthesis for QuickLogic FPGAs is omitted if this parameter is not specified. -verilog <file> - write the design to the specified verilog file. writing of an output file - is omitted if this parameter is not specified. + write the design to the specified verilog file. writing of an output + file is omitted if this parameter is not specified. -abc use old ABC flow, which has generally worse mapping results but is less @@ -7118,8 +7222,8 @@ This command runs synthesis for SmartFusion2 and IGLOO2 FPGAs. is omitted if this parameter is not specified. -vlog <file> - write the design to the specified Verilog file. writing of an output file - is omitted if this parameter is not specified. + write the design to the specified Verilog file. writing of an output + file is omitted if this parameter is not specified. -json <file> write the design to the specified JSON file. writing of an output file @@ -7139,6 +7243,9 @@ This command runs synthesis for SmartFusion2 and IGLOO2 FPGAs. -clkbuf insert direct PAD->global_net buffers + -discard-ffinit + discard FF init value instead of emitting an error + -retime run 'abc' with '-dff -D 1' options @@ -7156,6 +7263,7 @@ The following commands are executed by this synthesis command: deminout coarse: + attrmap -remove init (only if -discard-ffinit) synth -run coarse fine: @@ -7182,8 +7290,8 @@ The following commands are executed by this synthesis command: map_iobs: clkbufmap -buf CLKINT Y:A [-inpad CLKBUF Y:PAD] (unless -noiobs, -inpad only passed if -clkbuf) - iopadmap -bits -inpad INBUF Y:PAD -outpad OUTBUF D:PAD -toutpad TRIBUFF E:D:PAD -tinoutpad BIBUF E:Y:D:PAD (unless -noiobs - clean + iopadmap -bits -inpad INBUF Y:PAD -outpad OUTBUF D:PAD -toutpad TRIBUFF E:D:PAD -tinoutpad BIBUF E:Y:D:PAD (unless -noiobs) + clean -purge check: hierarchy -check @@ -7257,7 +7365,8 @@ compatible with 7-Series Xilinx devices. do not use XORCY/MUXCY/CARRY4 cells in output netlist -nowidelut - do not use MUXF[5-9] resources to implement LUTs larger than native for the target + do not use MUXF[5-9] resources to implement LUTs larger than native for + the target -nodsp do not use DSP48*s to implement multipliers and associated logic @@ -7273,8 +7382,8 @@ compatible with 7-Series Xilinx devices. infer URAM288s for large memories (xcup only) -widemux <int> - enable inference of hard multiplexer resources (MUXF[78]) for muxes at or - above this number of inputs (minimum value 2, recommended value >= 5). + enable inference of hard multiplexer resources (MUXF[78]) for muxes at + or above this number of inputs (minimum value 2, recommended value >= 5) default: 0 (no inference) -run <from_label>:<to_label> @@ -7466,8 +7575,8 @@ file. When a module in the map file has the 'techmap_celltype' attribute set, it will match cells with a type that match the text value of this attribute. Otherwise the module name will be used to match the cell. Multiple space-separated cell -types can be listed, and wildcards using [] will be expanded (ie. "$_DFF_[PN]_" -is the same as "$_DFF_P_ $_DFF_N_"). +types can be listed, and wildcards using [] will be expanded (ie. +"$_DFF_[PN]_" is the same as "$_DFF_P_ $_DFF_N_"). When a module in the map file has the 'techmap_simplemap' attribute set, techmap will use 'simplemap' (see 'help simplemap') to map cells matching the module. @@ -7523,11 +7632,11 @@ wires are supported: It is possible to combine both prefixes to 'RECURSION; CONSTMAP; '. _TECHMAP_REMOVEINIT_<port-name>_ - When this wire is set to a constant value, the init attribute of the wire(s) - connected to this port will be consumed. This wire must have the same - width as the given port, and for every bit that is set to 1 in the value, - the corresponding init attribute bit will be changed to 1'bx. If all - bits of an init attribute are left as x, it will be removed. + When this wire is set to a constant value, the init attribute of the + wire(s) connected to this port will be consumed. This wire must have + the same width as the given port, and for every bit that is set to 1 in + the value, the corresponding init attribute bit will be changed to 1'bx. + If all bits of an init attribute are left as x, it will be removed. In addition to this special wires, techmap also supports special parameters in modules in the map file: @@ -7548,8 +7657,8 @@ modules in the map file: _TECHMAP_WIREINIT_<port-name>_ When a parameter with this name exists, it will be set to the initial - value of the wire(s) connected to the given port, as specified by the init - attribute. If the attribute doesn't exist, x will be filled for the + value of the wire(s) connected to the given port, as specified by the + init attribute. If the attribute doesn't exist, x will be filled for the missing bits. To remove the init attribute bits used, use the _TECHMAP_REMOVEINIT_*_ wires. @@ -8097,6 +8206,9 @@ invariant constraints. -no-startoffset make indexes zero based, enable using map files with smt solvers. + -ywmap <filename> + write a map file for conversion to and from yosys witness traces. + -I, -O, -B, -L If the design contains no input/output/assert/flip-flop then create one dummy input/output/bad_state-pin or latch to make the tools reading the @@ -8136,8 +8248,8 @@ Write the current design to an BLIF file. suppresses the generation of this nets without fanout. The following options can be useful when the generated file is not going to be -read by a BLIF parser but a custom tool. It is recommended to not name the output -file *.blif when any of this options is used. +read by a BLIF parser but a custom tool. It is recommended to not name the +output file *.blif when any of this options is used. -icells do not translate Yosys's internal gates to generic BLIF logic @@ -8447,8 +8559,8 @@ Write the current design to an EDIF netlist file. constant drivers first) -gndvccy - create "GND" and "VCC" cells with "Y" outputs. (the default is "G" - for "GND" and "P" for "VCC".) + create "GND" and "VCC" cells with "Y" outputs. (the default is + "G" for "GND" and "P" for "VCC".) -attrprop create EDIF properties for cell attributes @@ -8608,7 +8720,9 @@ Where <port_details> is: "signed": <1 if the port is signed> } -The "offset" and "upto" fields are skipped if their value would be 0.They don't affect connection semantics, and are only used to preserve originalHDL bit indexing.And <cell_details> is: +The "offset" and "upto" fields are skipped if their value would be 0. +They don't affect connection semantics, and are only used to preserve original +HDL bit indexing.And <cell_details> is: { "hide_name": <1 | 0>, @@ -8667,7 +8781,9 @@ values referenced above are vectors of this integers. Signal bits that are connected to a constant driver are denoted as string "0", "1", "x", or "z" instead of a number. -Bit vectors (including integers) are written as string holding the binaryrepresentation of the value. Strings are written as strings, with an appendedblank in cases of strings of the form /[01xz]* */. +Bit vectors (including integers) are written as string holding the binary +representation of the value. Strings are written as strings, with an appended +blank in cases of strings of the form /[01xz]* */. For example the following Verilog code: @@ -9103,7 +9219,8 @@ Write the current design to a Verilog file. as binary numbers. -simple-lhs - Connection assignments with simple left hand side without concatenations. + Connection assignments with simple left hand side without + concatenations. -extmem instead of initializing memories using assignments to individual @@ -9217,9 +9334,10 @@ into using the DSP48E1's pattern detector feature for overflow detection. This pass converts chains of built-in flops (bit-level: $_DFF_[NP]_, $_DFFE_* and word-level: $dff, $dffe) as well as Xilinx flops (FDRE, FDRE_1) into a -$__XILINX_SHREG cell. Chains must be of the same cell type, clock, clock polarity, -enable, and enable polarity (where relevant). +$__XILINX_SHREG cell. Chains must be of the same cell type, clock, clock +polarity, enable, and enable polarity (where relevant). Flops with resets cannot be mapped to Xilinx devices and will not be inferred. + -minlen N min length of shift register (default = 3) diff --git a/misc/yosys-config.in b/misc/yosys-config.in index a31ef38c2..f0f0f7552 100644 --- a/misc/yosys-config.in +++ b/misc/yosys-config.in @@ -1,4 +1,4 @@ -#!/bin/bash +#!/usr/bin/env bash help() { { diff --git a/passes/cmds/bugpoint.cc b/passes/cmds/bugpoint.cc index 7b621504d..e666023fa 100644 --- a/passes/cmds/bugpoint.cc +++ b/passes/cmds/bugpoint.cc @@ -34,10 +34,10 @@ struct BugpointPass : public Pass { log("\n"); log("This command minimizes the current design that is known to crash Yosys with the\n"); log("given script into a smaller testcase. It does this by removing an arbitrary part\n"); - log("of the design and recursively invokes a new Yosys process with this modified design\n"); - log("and the same script, repeating these steps while it can find a smaller design that\n"); - log("still causes a crash. Once this command finishes, it replaces the current design\n"); - log("with the smallest testcase it was able to produce.\n"); + log("of the design and recursively invokes a new Yosys process with this modified\n"); + log("design and the same script, repeating these steps while it can find a smaller\n"); + log("design that still causes a crash. Once this command finishes, it replaces the\n"); + log("current design with the smallest testcase it was able to produce.\n"); log("In order to save the reduced testcase you must write this out to a file with\n"); log("another command after `bugpoint` like `write_rtlil` or `write_verilog`.\n"); log("\n"); diff --git a/passes/cmds/chformal.cc b/passes/cmds/chformal.cc index d813a449c..66044b161 100644 --- a/passes/cmds/chformal.cc +++ b/passes/cmds/chformal.cc @@ -32,8 +32,8 @@ struct ChformalPass : public Pass { log(" chformal [types] [mode] [options] [selection]\n"); log("\n"); log("Make changes to the formal constraints of the design. The [types] options\n"); - log("the type of constraint to operate on. If none of the following options are given,\n"); - log("the command will operate on all constraint types:\n"); + log("the type of constraint to operate on. If none of the following options are\n"); + log("given, the command will operate on all constraint types:\n"); log("\n"); log(" -assert $assert cells, representing assert(...) constraints\n"); log(" -assume $assume cells, representing assume(...) constraints\n"); diff --git a/passes/cmds/exec.cc b/passes/cmds/exec.cc index f00629a02..c15ef23bf 100644 --- a/passes/cmds/exec.cc +++ b/passes/cmds/exec.cc @@ -46,8 +46,8 @@ struct ExecPass : public Pass { log("\n"); log("Execute a command in the operating system shell. All supplied arguments are\n"); log("concatenated and passed as a command to popen(3). Whitespace is not guaranteed\n"); - log("to be preserved, even if quoted. stdin and stderr are not connected, while stdout is\n"); - log("logged unless the \"-q\" option is specified.\n"); + log("to be preserved, even if quoted. stdin and stderr are not connected, while\n"); + log("stdout is logged unless the \"-q\" option is specified.\n"); log("\n"); log("\n"); log(" -q\n"); diff --git a/passes/cmds/glift.cc b/passes/cmds/glift.cc index b398c3e04..439ded076 100644 --- a/passes/cmds/glift.cc +++ b/passes/cmds/glift.cc @@ -431,45 +431,46 @@ struct GliftPass : public Pass { log("\n"); log(" glift <command> [options] [selection]\n"); log("\n"); - log("Augments the current or specified module with gate-level information flow tracking\n"); - log("(GLIFT) logic using the \"constructive mapping\" approach. Also can set up QBF-SAT\n"); - log("optimization problems in order to optimize GLIFT models or trade off precision and\n"); - log("complexity.\n"); + log("Augments the current or specified module with gate-level information flow \n"); + log("tracking (GLIFT) logic using the \"constructive mapping\" approach. Also can set\n"); + log("up QBF-SAT optimization problems in order to optimize GLIFT models or trade off\n"); + log("precision and complexity.\n"); log("\n"); log("\n"); log("Commands:\n"); log("\n"); log(" -create-precise-model\n"); - log(" Replaces the current or specified module with one that has corresponding \"taint\"\n"); - log(" inputs, outputs, and internal nets along with precise taint tracking logic.\n"); - log(" For example, precise taint tracking logic for an AND gate is:\n"); + log(" Replaces the current or specified module with one that has corresponding\n"); + log(" \"taint\" inputs, outputs, and internal nets along with precise taint\n"); + log(" tracking logic. For example, precise taint tracking logic for an AND gate\n"); + log(" is:\n"); log("\n"); log(" y_t = a & b_t | b & a_t | a_t & b_t\n"); log("\n"); log("\n"); log(" -create-imprecise-model\n"); - log(" Replaces the current or specified module with one that has corresponding \"taint\"\n"); - log(" inputs, outputs, and internal nets along with imprecise \"All OR\" taint tracking\n"); - log(" logic:\n"); + log(" Replaces the current or specified module with one that has corresponding\n"); + log(" \"taint\" inputs, outputs, and internal nets along with imprecise \"All OR\"\n"); + log(" taint tracking logic:\n"); log("\n"); log(" y_t = a_t | b_t\n"); log("\n"); log("\n"); log(" -create-instrumented-model\n"); - log(" Replaces the current or specified module with one that has corresponding \"taint\"\n"); - log(" inputs, outputs, and internal nets along with 4 varying-precision versions of taint\n"); - log(" tracking logic. Which version of taint tracking logic is used for a given gate is\n"); - log(" determined by a MUX selected by an $anyconst cell. By default, unless the\n"); - log(" `-no-cost-model` option is provided, an additional wire named `__glift_weight` with\n"); - log(" the `keep` and `minimize` attributes is added to the module along with pmuxes and\n"); - log(" adders to calculate a rough estimate of the number of logic gates in the GLIFT model\n"); - log(" given an assignment for the $anyconst cells. The four versions of taint tracking logic\n"); - log(" for an AND gate are:"); - log("\n"); - log(" y_t = a & b_t | b & a_t | a_t & b_t (like `-create-precise-model`)\n"); + log(" Replaces the current or specified module with one that has corresponding\n"); + log(" \"taint\" inputs, outputs, and internal nets along with 4 varying-precision\n"); + log(" versions of taint tracking logic. Which version of taint tracking logic is\n"); + log(" used for a given gate is determined by a MUX selected by an $anyconst cell.\n"); + log(" By default, unless the `-no-cost-model` option is provided, an additional\n"); + log(" wire named `__glift_weight` with the `keep` and `minimize` attributes is\n"); + log(" added to the module along with pmuxes and adders to calculate a rough\n"); + log(" estimate of the number of logic gates in the GLIFT model given an assignment\n"); + log(" for the $anyconst cells. The four versions of taint tracking logic for an\n"); + log(" AND gate are:\n"); + log(" y_t = a & b_t | b & a_t | a_t & b_t (like `-create-precise-model`)\n"); log(" y_t = a_t | a & b_t\n"); log(" y_t = b_t | b & a_t\n"); - log(" y_t = a_t | b_t (like `-create-imprecise-model`)\n"); + log(" y_t = a_t | b_t (like `-create-imprecise-model`)\n"); log("\n"); log("\n"); log("Options:\n"); @@ -479,27 +480,30 @@ struct GliftPass : public Pass { log(" (default: label constants as un-tainted)\n"); log("\n"); log(" -keep-outputs\n"); - log(" Do not remove module outputs. Taint tracking outputs will appear in the module ports\n"); - log(" alongside the orignal outputs.\n"); + log(" Do not remove module outputs. Taint tracking outputs will appear in the\n"); + log(" module ports alongside the orignal outputs.\n"); log(" (default: original module outputs are removed)\n"); log("\n"); log(" -simple-cost-model\n"); - log(" Do not model logic area. Instead model the number of non-zero assignments to $anyconsts.\n"); - log(" Taint tracking logic versions vary in their size, but all reduced-precision versions are\n"); - log(" significantly smaller than the fully-precise version. A non-zero $anyconst assignment means\n"); - log(" that reduced-precision taint tracking logic was chosen for some gate.\n"); - log(" Only applicable in combination with `-create-instrumented-model`.\n"); - log(" (default: use a complex model and give that wire the \"keep\" and \"minimize\" attributes)\n"); + log(" Do not model logic area. Instead model the number of non-zero assignments to\n"); + log(" $anyconsts. Taint tracking logic versions vary in their size, but all\n"); + log(" reduced-precision versions are significantly smaller than the fully-precise\n"); + log(" version. A non-zero $anyconst assignment means that reduced-precision taint\n"); + log(" tracking logic was chosen for some gate. Only applicable in combination with\n"); + log(" `-create-instrumented-model`. (default: use a complex model and give that\n"); + log(" wire the \"keep\" and \"minimize\" attributes)\n"); log("\n"); log(" -no-cost-model\n"); - log(" Do not model taint tracking logic area and do not create a `__glift_weight` wire.\n"); - log(" Only applicable in combination with `-create-instrumented-model`.\n"); - log(" (default: model area and give that wire the \"keep\" and \"minimize\" attributes)\n"); + log(" Do not model taint tracking logic area and do not create a `__glift_weight`\n"); + log(" wire. Only applicable in combination with `-create-instrumented-model`.\n"); + log(" (default: model area and give that wire the \"keep\" and \"minimize\"\n"); + log(" attributes)\n"); log("\n"); log(" -instrument-more\n"); - log(" Allow choice from more versions of (even simpler) taint tracking logic. A total\n"); - log(" of 8 versions of taint tracking logic will be added per gate, including the 4\n"); - log(" versions from `-create-instrumented-model` and these additional versions:\n"); + log(" Allow choice from more versions of (even simpler) taint tracking logic. A\n"); + log(" total of 8 versions of taint tracking logic will be added per gate,\n"); + log(" including the 4 versions from `-create-instrumented-model` and these\n"); + log(" additional versions:\n"); log("\n"); log(" y_t = a_t\n"); log(" y_t = b_t\n"); diff --git a/passes/cmds/logcmd.cc b/passes/cmds/logcmd.cc index f1702400d..20cbd8943 100644 --- a/passes/cmds/logcmd.cc +++ b/passes/cmds/logcmd.cc @@ -38,8 +38,9 @@ struct LogPass : public Pass { log("logfiles.\n"); log("\n"); log(" -stdout\n"); - log(" Print the output to stdout too. This is useful when all Yosys is executed\n"); - log(" with a script and the -q (quiet operation) argument to notify the user.\n"); + log(" Print the output to stdout too. This is useful when all Yosys is\n"); + log(" executed with a script and the -q (quiet operation) argument to notify\n"); + log(" the user.\n"); log("\n"); log(" -stderr\n"); log(" Print the output to stderr too.\n"); diff --git a/passes/cmds/scratchpad.cc b/passes/cmds/scratchpad.cc index 015eb97e7..aecc4c17d 100644 --- a/passes/cmds/scratchpad.cc +++ b/passes/cmds/scratchpad.cc @@ -49,7 +49,8 @@ struct ScratchpadPass : public Pass { log(" copy the value of the first identifier to the second identifier.\n"); log("\n"); log(" -assert <identifier> <value>\n"); - log(" assert that the entry for the given identifier is set to the given value.\n"); + log(" assert that the entry for the given identifier is set to the given\n"); + log(" value.\n"); log("\n"); log(" -assert-set <identifier>\n"); log(" assert that the entry for the given identifier exists.\n"); diff --git a/passes/cmds/select.cc b/passes/cmds/select.cc index b112b145c..fdf56641c 100644 --- a/passes/cmds/select.cc +++ b/passes/cmds/select.cc @@ -1125,7 +1125,7 @@ struct SelectPass : public Pass { log(" <obj_pattern>\n"); log(" select the specified object(s) from the current module\n"); log("\n"); - log("By default, patterns will not match black/white-box modules or their"); + log("By default, patterns will not match black/white-box modules or their\n"); log("contents. To include such objects, prefix the pattern with '='.\n"); log("\n"); log("A <mod_pattern> can be a module name, wildcard expression (*, ?, [..])\n"); diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc index 4d5605932..b186e5db2 100644 --- a/passes/cmds/show.cc +++ b/passes/cmds/show.cc @@ -825,6 +825,7 @@ struct ShowPass : public Pass { for (auto filename : libfiles) { std::ifstream f; + rewrite_filename(filename); f.open(filename.c_str()); yosys_input_files.insert(filename); if (f.fail()) diff --git a/passes/cmds/stat.cc b/passes/cmds/stat.cc index a4984597d..a998ab8e7 100644 --- a/passes/cmds/stat.cc +++ b/passes/cmds/stat.cc @@ -149,6 +149,78 @@ struct statdata_t } } + unsigned int estimate_xilinx_lc() + { + unsigned int lut6_cnt = num_cells_by_type[ID(LUT6)]; + unsigned int lut5_cnt = num_cells_by_type[ID(LUT5)]; + unsigned int lut4_cnt = num_cells_by_type[ID(LUT4)]; + unsigned int lut3_cnt = num_cells_by_type[ID(LUT3)]; + unsigned int lut2_cnt = num_cells_by_type[ID(LUT2)]; + unsigned int lut1_cnt = num_cells_by_type[ID(LUT1)]; + unsigned int lc_cnt = 0; + + lc_cnt += lut6_cnt; + + lc_cnt += lut5_cnt; + if (lut1_cnt) { + int cnt = std::min(lut5_cnt, lut1_cnt); + lut5_cnt -= cnt; + lut1_cnt -= cnt; + } + + lc_cnt += lut4_cnt; + if (lut1_cnt) { + int cnt = std::min(lut4_cnt, lut1_cnt); + lut4_cnt -= cnt; + lut1_cnt -= cnt; + } + if (lut2_cnt) { + int cnt = std::min(lut4_cnt, lut2_cnt); + lut4_cnt -= cnt; + lut2_cnt -= cnt; + } + + lc_cnt += lut3_cnt; + if (lut1_cnt) { + int cnt = std::min(lut3_cnt, lut1_cnt); + lut3_cnt -= cnt; + lut1_cnt -= cnt; + } + if (lut2_cnt) { + int cnt = std::min(lut3_cnt, lut2_cnt); + lut3_cnt -= cnt; + lut2_cnt -= cnt; + } + if (lut3_cnt) { + int cnt = (lut3_cnt + 1) / 2; + lut3_cnt -= cnt; + } + + lc_cnt += (lut2_cnt + lut1_cnt + 1) / 2; + + return lc_cnt; + } + + unsigned int cmos_transistor_count(bool *tran_cnt_exact) + { + unsigned int tran_cnt = 0; + auto &gate_costs = CellCosts::cmos_gate_cost(); + + for (auto it : num_cells_by_type) { + auto ctype = it.first; + auto cnum = it.second; + + if (gate_costs.count(ctype)) + tran_cnt += cnum * gate_costs.at(ctype); + else if (ctype.in(ID($_DFF_P_), ID($_DFF_N_))) + tran_cnt += cnum * 16; + else + *tran_cnt_exact = false; + } + + return tran_cnt; + } + void log_data(RTLIL::IdString mod_name, bool top_mod) { log(" Number of wires: %6u\n", num_wires); @@ -176,74 +248,14 @@ struct statdata_t if (tech == "xilinx") { - unsigned int lut6_cnt = num_cells_by_type[ID(LUT6)]; - unsigned int lut5_cnt = num_cells_by_type[ID(LUT5)]; - unsigned int lut4_cnt = num_cells_by_type[ID(LUT4)]; - unsigned int lut3_cnt = num_cells_by_type[ID(LUT3)]; - unsigned int lut2_cnt = num_cells_by_type[ID(LUT2)]; - unsigned int lut1_cnt = num_cells_by_type[ID(LUT1)]; - unsigned int lc_cnt = 0; - - lc_cnt += lut6_cnt; - - lc_cnt += lut5_cnt; - if (lut1_cnt) { - int cnt = std::min(lut5_cnt, lut1_cnt); - lut5_cnt -= cnt; - lut1_cnt -= cnt; - } - - lc_cnt += lut4_cnt; - if (lut1_cnt) { - int cnt = std::min(lut4_cnt, lut1_cnt); - lut4_cnt -= cnt; - lut1_cnt -= cnt; - } - if (lut2_cnt) { - int cnt = std::min(lut4_cnt, lut2_cnt); - lut4_cnt -= cnt; - lut2_cnt -= cnt; - } - - lc_cnt += lut3_cnt; - if (lut1_cnt) { - int cnt = std::min(lut3_cnt, lut1_cnt); - lut3_cnt -= cnt; - lut1_cnt -= cnt; - } - if (lut2_cnt) { - int cnt = std::min(lut3_cnt, lut2_cnt); - lut3_cnt -= cnt; - lut2_cnt -= cnt; - } - if (lut3_cnt) { - int cnt = (lut3_cnt + 1) / 2; - lut3_cnt -= cnt; - } - - lc_cnt += (lut2_cnt + lut1_cnt + 1) / 2; - log("\n"); - log(" Estimated number of LCs: %10u\n", lc_cnt); + log(" Estimated number of LCs: %10u\n", estimate_xilinx_lc()); } if (tech == "cmos") { - unsigned int tran_cnt = 0; bool tran_cnt_exact = true; - auto &gate_costs = CellCosts::cmos_gate_cost(); - - for (auto it : num_cells_by_type) { - auto ctype = it.first; - auto cnum = it.second; - - if (gate_costs.count(ctype)) - tran_cnt += cnum * gate_costs.at(ctype); - else if (ctype.in(ID($_DFF_P_), ID($_DFF_N_))) - tran_cnt += cnum * 16; - else - tran_cnt_exact = false; - } + unsigned int tran_cnt = cmos_transistor_count(&tran_cnt_exact); log("\n"); log(" Estimated number of transistors: %10u%s\n", tran_cnt, tran_cnt_exact ? "" : "+"); @@ -273,7 +285,20 @@ struct statdata_t first_line = false; } log("\n"); - log(" }\n"); + log(" }"); + if (tech == "xilinx") + { + log(",\n"); + log(" \"estimated_num_lc\": %u", estimate_xilinx_lc()); + } + if (tech == "cmos") + { + bool tran_cnt_exact = true; + unsigned int tran_cnt = cmos_transistor_count(&tran_cnt_exact); + log(",\n"); + log(" \"estimated_num_transistors\": \"%u%s\"", tran_cnt, tran_cnt_exact ? "" : "+"); + } + log("\n"); log(" }"); } }; @@ -352,8 +377,6 @@ struct StatPass : public Pass { } void execute(std::vector<std::string> args, RTLIL::Design *design) override { - log_header(design, "Printing statistics.\n"); - bool width_mode = false, json_mode = false; RTLIL::Module *top_mod = nullptr; std::map<RTLIL::IdString, statdata_t> mod_stat; @@ -391,6 +414,9 @@ struct StatPass : public Pass { } extra_args(args, argidx, design); + if(!json_mode) + log_header(design, "Printing statistics.\n"); + if (techname != "" && techname != "xilinx" && techname != "cmos" && !json_mode) log_cmd_error("Unsupported technology: '%s'\n", techname.c_str()); diff --git a/passes/hierarchy/hierarchy.cc b/passes/hierarchy/hierarchy.cc index d27fddf1c..eea6abb04 100644 --- a/passes/hierarchy/hierarchy.cc +++ b/passes/hierarchy/hierarchy.cc @@ -1058,6 +1058,7 @@ struct HierarchyPass : public Pass { if (tmp_top_mod != NULL) { if (tmp_top_mod != top_mod){ top_mod = tmp_top_mod; + top_mod->attributes[ID::initial_top] = RTLIL::Const(1); did_something = true; } } diff --git a/passes/hierarchy/submod.cc b/passes/hierarchy/submod.cc index c0c40671d..8476d392c 100644 --- a/passes/hierarchy/submod.cc +++ b/passes/hierarchy/submod.cc @@ -348,8 +348,8 @@ struct SubmodPass : public Pass { log("\n"); log(" -hidden\n"); log(" instead of creating submodule ports with public names, create ports with\n"); - log(" private names so that a subsequent 'flatten; clean' call will restore the\n"); - log(" original module with original public names.\n"); + log(" private names so that a subsequent 'flatten; clean' call will restore\n"); + log(" the original module with original public names.\n"); log("\n"); } void execute(std::vector<std::string> args, RTLIL::Design *design) override diff --git a/passes/memory/memory_bram.cc b/passes/memory/memory_bram.cc index b1f45d5fc..1cb50b3ea 100644 --- a/passes/memory/memory_bram.cc +++ b/passes/memory/memory_bram.cc @@ -1245,7 +1245,8 @@ struct MemoryBramPass : public Pass { log("greater than 1 share the same configuration bit.\n"); log("\n"); log("Using the same bram name in different bram blocks will create different variants\n"); - log("of the bram. Verilog configuration parameters for the bram are created as needed.\n"); + log("of the bram. Verilog configuration parameters for the bram are created as\n"); + log("needed.\n"); log("\n"); log("It is also possible to create variants by repeating statements in the bram block\n"); log("and appending '@<label>' to the individual statements.\n"); diff --git a/passes/memory/memory_dff.cc b/passes/memory/memory_dff.cc index 998e86491..75c6e6a3a 100644 --- a/passes/memory/memory_dff.cc +++ b/passes/memory/memory_dff.cc @@ -631,8 +631,8 @@ struct MemoryDffPass : public Pass { log("\n"); log(" memory_dff [-no-rw-check] [selection]\n"); log("\n"); - log("This pass detects DFFs at memory read ports and merges them into the memory port.\n"); - log("I.e. it consumes an asynchronous memory port and the flip-flops at its\n"); + log("This pass detects DFFs at memory read ports and merges them into the memory\n"); + log("port. I.e. it consumes an asynchronous memory port and the flip-flops at its\n"); log("interface and yields a synchronous memory port.\n"); log("\n"); log(" -no-rw-check\n"); diff --git a/passes/memory/memory_share.cc b/passes/memory/memory_share.cc index 5cb11d62b..8b2354ef8 100644 --- a/passes/memory/memory_share.cc +++ b/passes/memory/memory_share.cc @@ -523,8 +523,8 @@ struct MemorySharePass : public Pass { log(" - When multiple write ports access the same address then this is converted\n"); log(" to a single write port with a more complex data and/or enable logic path.\n"); log("\n"); - log(" - When multiple read or write ports access adjacent aligned addresses, they are\n"); - log(" merged to a single wide read or write port. This transformation can be\n"); + log(" - When multiple read or write ports access adjacent aligned addresses, they\n"); + log(" are merged to a single wide read or write port. This transformation can be\n"); log(" disabled with the \"-nowiden\" option.\n"); log("\n"); log(" - When multiple write ports are never accessed at the same time (a SAT\n"); diff --git a/passes/opt/opt_dff.cc b/passes/opt/opt_dff.cc index 6ff2d1b4b..f090d20b2 100644 --- a/passes/opt/opt_dff.cc +++ b/passes/opt/opt_dff.cc @@ -853,14 +853,17 @@ struct OptDffPass : public Pass { log(" opt_dff [-nodffe] [-nosdff] [-keepdc] [-sat] [selection]\n"); log("\n"); log("This pass converts flip-flops to a more suitable type by merging clock enables\n"); - log("and synchronous reset multiplexers, removing unused control inputs, or potentially\n"); - log("removes the flip-flop altogether, converting it to a constant driver.\n"); + log("and synchronous reset multiplexers, removing unused control inputs, or\n"); + log("potentially removes the flip-flop altogether, converting it to a constant\n"); + log("driver.\n"); log("\n"); log(" -nodffe\n"); - log(" disables dff -> dffe conversion, and other transforms recognizing clock enable\n"); + log(" disables dff -> dffe conversion, and other transforms recognizing clock\n"); + log(" enable\n"); log("\n"); log(" -nosdff\n"); - log(" disables dff -> sdff conversion, and other transforms recognizing sync resets\n"); + log(" disables dff -> sdff conversion, and other transforms recognizing sync\n"); + log(" resets\n"); log("\n"); log(" -simple-dffe\n"); log(" only enables clock enable recognition transform for obvious cases\n"); diff --git a/passes/pmgen/xilinx_srl.cc b/passes/pmgen/xilinx_srl.cc index a66a06586..eebd30017 100644 --- a/passes/pmgen/xilinx_srl.cc +++ b/passes/pmgen/xilinx_srl.cc @@ -196,9 +196,9 @@ struct XilinxSrlPass : public Pass { log("\n"); log("This pass converts chains of built-in flops (bit-level: $_DFF_[NP]_, $_DFFE_*\n"); log("and word-level: $dff, $dffe) as well as Xilinx flops (FDRE, FDRE_1) into a\n"); - log("$__XILINX_SHREG cell. Chains must be of the same cell type, clock, clock polarity,\n"); - log("enable, and enable polarity (where relevant).\n"); - log("Flops with resets cannot be mapped to Xilinx devices and will not be inferred."); + log("$__XILINX_SHREG cell. Chains must be of the same cell type, clock, clock\n"); + log("polarity, enable, and enable polarity (where relevant).\n"); + log("Flops with resets cannot be mapped to Xilinx devices and will not be inferred.\n"); log("\n"); log(" -minlen N\n"); log(" min length of shift register (default = 3)\n"); diff --git a/passes/sat/mutate.cc b/passes/sat/mutate.cc index 42eb0c6d0..02174be53 100644 --- a/passes/sat/mutate.cc +++ b/passes/sat/mutate.cc @@ -527,6 +527,8 @@ void mutate_list(Design *design, const mutate_opts_t &opts, const string &filena } log("Raw database size: %d\n", GetSize(database)); + if (N > GetSize(database)) + log_warning("%d mutations requested but only %d could be created!\n", N, GetSize(database)); if (N != 0) { database_reduce(database, opts, opts.none ? N-1 : N, rng); log("Reduced database size: %d\n", GetSize(database)); diff --git a/passes/sat/qbfsat.cc b/passes/sat/qbfsat.cc index 1302b3383..4580f194e 100644 --- a/passes/sat/qbfsat.cc +++ b/passes/sat/qbfsat.cc @@ -508,11 +508,11 @@ struct QbfSatPass : public Pass { log("\n"); log(" qbfsat [options] [selection]\n"); log("\n"); - log("This command solves an \"exists-forall\" 2QBF-SAT problem defined over the currently\n"); - log("selected module. Existentially-quantified variables are declared by assigning a wire\n"); - log("\"$anyconst\". Universally-quantified variables may be explicitly declared by assigning\n"); - log("a wire \"$allconst\", but module inputs will be treated as universally-quantified\n"); - log("variables by default.\n"); + log("This command solves an \"exists-forall\" 2QBF-SAT problem defined over the\n"); + log("currently selected module. Existentially-quantified variables are declared by\n"); + log("assigning a wire \"$anyconst\". Universally-quantified variables may be\n"); + log("explicitly declared by assigning a wire \"$allconst\", but module inputs will be\n"); + log("treated as universally-quantified variables by default.\n"); log("\n"); log(" -nocleanup\n"); log(" Do not delete temporary files and directories. Useful for debugging.\n"); @@ -521,23 +521,25 @@ struct QbfSatPass : public Pass { log(" Pass the --dump-smt2 option to yosys-smtbmc.\n"); log("\n"); log(" -assume-outputs\n"); - log(" Add an \"$assume\" cell for the conjunction of all one-bit module output wires.\n"); + log(" Add an \"$assume\" cell for the conjunction of all one-bit module output\n"); + log(" wires.\n"); log("\n"); log(" -assume-negative-polarity\n"); - log(" When adding $assume cells for one-bit module output wires, assume they are\n"); - log(" negative polarity signals and should always be low, for example like the\n"); - log(" miters created with the `miter` command.\n"); + log(" When adding $assume cells for one-bit module output wires, assume they\n"); + log(" are negative polarity signals and should always be low, for example like\n"); + log(" the miters created with the `miter` command.\n"); log("\n"); log(" -nooptimize\n"); - log(" Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit \"(maximize)\" or\n"); - log(" \"(minimize)\" in the SMT-LIBv2, and generally make no attempt to optimize anything.\n"); + log(" Ignore \"\\minimize\" and \"\\maximize\" attributes, do not emit\n"); + log(" \"(maximize)\" or \"(minimize)\" in the SMT-LIBv2, and generally make no\n"); + log(" attempt to optimize anything.\n"); log("\n"); log(" -nobisection\n"); - log(" If a wire is marked with the \"\\minimize\" or \"\\maximize\" attribute, do not\n"); - log(" attempt to optimize that value with the default iterated solving and threshold\n"); - log(" bisection approach. Instead, have yosys-smtbmc emit a \"(minimize)\" or \"(maximize)\"\n"); - log(" command in the SMT-LIBv2 output and hope that the solver supports optimizing\n"); - log(" quantified bitvector problems.\n"); + log(" If a wire is marked with the \"\\minimize\" or \"\\maximize\" attribute,\n"); + log(" do not attempt to optimize that value with the default iterated solving\n"); + log(" and threshold bisection approach. Instead, have yosys-smtbmc emit a\n"); + log(" \"(minimize)\" or \"(maximize)\" command in the SMT-LIBv2 output and\n"); + log(" hope that the solver supports optimizing quantified bitvector problems.\n"); log("\n"); log(" -solver <solver>\n"); log(" Use a particular solver. Choose one of: \"z3\", \"yices\", and \"cvc4\".\n"); @@ -567,13 +569,14 @@ struct QbfSatPass : public Pass { log(" corresponding constant value from the model produced by the solver.\n"); log("\n"); log(" -specialize-from-file <solution file>\n"); - log(" Do not run the solver, but instead only attempt to replace each \"$anyconst\"\n"); - log(" cell in the current module with a constant value provided by the specified file.\n"); + log(" Do not run the solver, but instead only attempt to replace each\n"); + log(" \"$anyconst\" cell in the current module with a constant value provided\n"); + log(" by the specified file.\n"); log("\n"); log(" -write-solution <solution file>\n"); - log(" If the problem is satisfiable, write the corresponding constant value for each\n"); - log(" \"$anyconst\" cell from the model produced by the solver to the specified file."); - log("\n"); + log(" If the problem is satisfiable, write the corresponding constant value\n"); + log(" for each \"$anyconst\" cell from the model produced by the solver to the\n"); + log(" specified file.\n"); log("\n"); } diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index 18a25a097..b68783f20 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -2013,7 +2013,8 @@ struct SimPass : public Pass { log(" writeback mode: use final simulation state as new init state\n"); log("\n"); log(" -r\n"); - log(" read simulation results file (file formats supported: FST, VCD, AIW and WIT)\n"); + log(" read simulation results file\n"); + log(" File formats supported: FST, VCD, AIW and WIT\n"); log(" VCD support requires vcd2fst external tool to be present\n"); log("\n"); log(" -map <filename>\n"); @@ -2248,8 +2249,8 @@ struct Fst2TbPass : public Pass { log("\n"); log(" fst2tb [options] [top-level]\n"); log("\n"); - log("This command generates testbench for the circuit using the given top-level module\n"); - log("and simulus signal from FST file\n"); + log("This command generates testbench for the circuit using the given top-level\n"); + log("module and simulus signal from FST file\n"); log("\n"); log(" -tb <name>\n"); log(" generated testbench name.\n"); diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc index 656c36b84..da601a856 100644 --- a/passes/techmap/abc.cc +++ b/passes/techmap/abc.cc @@ -29,11 +29,11 @@ // Kahn, Arthur B. (1962), "Topological sorting of large networks", Communications of the ACM 5 (11): 558-562, doi:10.1145/368996.369025 // http://en.wikipedia.org/wiki/Topological_sorting -#define ABC_COMMAND_LIB "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put" -#define ABC_COMMAND_CTR "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put; buffer; upsize {D}; dnsize {D}; stime -p" -#define ABC_COMMAND_LUT "strash; ifraig; scorr; dc2; dretime; strash; dch -f; if; mfs2" -#define ABC_COMMAND_SOP "strash; ifraig; scorr; dc2; dretime; strash; dch -f; cover {I} {P}" -#define ABC_COMMAND_DFL "strash; ifraig; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put" +#define ABC_COMMAND_LIB "strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put" +#define ABC_COMMAND_CTR "strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put; buffer; upsize {D}; dnsize {D}; stime -p" +#define ABC_COMMAND_LUT "strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; dch -f; if; mfs2" +#define ABC_COMMAND_SOP "strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; dch -f; cover {I} {P}" +#define ABC_COMMAND_DFL "strash; &get -n; &fraig -x; &put; scorr; dc2; dretime; strash; &get -n; &dch -f; &nf {D}; &put" #define ABC_FAST_COMMAND_LIB "strash; dretime; map {D}" #define ABC_FAST_COMMAND_CTR "strash; dretime; map {D}; buffer; upsize {D}; dnsize {D}; stime -p" @@ -782,9 +782,12 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin if (dff_mode && clk_sig.empty()) log_cmd_error("Clock domain %s not found.\n", clk_str.c_str()); - std::string tempdir_name = get_base_tmpdir() + "/" + proc_program_prefix()+ "yosys-abc-XXXXXX"; - if (!cleanup) - tempdir_name[0] = tempdir_name[4] = '_'; + std::string tempdir_name; + if (cleanup) + tempdir_name = get_base_tmpdir() + "/"; + else + tempdir_name = "_tmp_"; + tempdir_name += proc_program_prefix() + "yosys-abc-XXXXXX"; tempdir_name = make_temp_dir(tempdir_name); log_header(design, "Extracting gate netlist of module `%s' to `%s/input.blif'..\n", module->name.c_str(), replace_tempdir(tempdir_name, tempdir_name, show_tempdir).c_str()); @@ -846,7 +849,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin for (size_t pos = abc_script.find("{S}"); pos != std::string::npos; pos = abc_script.find("{S}", pos)) abc_script = abc_script.substr(0, pos) + lutin_shared + abc_script.substr(pos+3); if (abc_dress) - abc_script += "; dress"; + abc_script += stringf("; dress \"%s/input.blif\"", tempdir_name.c_str()); abc_script += stringf("; write_blif %s/output.blif", tempdir_name.c_str()); abc_script = add_echos_to_abc_cmd(abc_script); @@ -1532,7 +1535,8 @@ struct AbcPass : public Pass { log(" NMUX, AOI3, OAI3, AOI4, OAI4.\n"); log(" (The NOT gate is always added to this list automatically.)\n"); log("\n"); - log(" The following aliases can be used to reference common sets of gate types:\n"); + log(" The following aliases can be used to reference common sets of gate\n"); + log(" types:\n"); log(" simple: AND OR XOR MUX\n"); log(" cmos2: NAND NOR\n"); log(" cmos3: NAND NOR AOI3 OAI3\n"); @@ -1576,8 +1580,8 @@ struct AbcPass : public Pass { log("\n"); log(" -dress\n"); log(" run the 'dress' command after all other ABC commands. This aims to\n"); - log(" preserve naming by an equivalence check between the original and post-ABC\n"); - log(" netlists (experimental).\n"); + log(" preserve naming by an equivalence check between the original and\n"); + log(" post-ABC netlists (experimental).\n"); log("\n"); log("When no target cell library is specified the Yosys standard cell library is\n"); log("loaded into ABC before the ABC script is executed.\n"); diff --git a/passes/techmap/abc9.cc b/passes/techmap/abc9.cc index 79c994b11..876917e56 100644 --- a/passes/techmap/abc9.cc +++ b/passes/techmap/abc9.cc @@ -93,8 +93,8 @@ struct Abc9Pass : public ScriptPass log("\n"); log(" abc9 [options] [selection]\n"); log("\n"); - log("This script pass performs a sequence of commands to facilitate the use of the ABC\n"); - log("tool [1] for technology mapping of the current design to a target FPGA\n"); + log("This script pass performs a sequence of commands to facilitate the use of the\n"); + log("ABC tool [1] for technology mapping of the current design to a target FPGA\n"); log("architecture. Only fully-selected modules are supported.\n"); log("\n"); log(" -run <from_label>:<to_label>\n"); @@ -404,9 +404,12 @@ struct Abc9Pass : public ScriptPass if (!active_design->selected_whole_module(mod)) log_error("Can't handle partially selected module %s!\n", log_id(mod)); - std::string tempdir_name = get_base_tmpdir() + "/" + proc_program_prefix() + "yosys-abc-XXXXXX"; - if (!cleanup) - tempdir_name[0] = tempdir_name[4] = '_'; + std::string tempdir_name; + if (cleanup) + tempdir_name = get_base_tmpdir() + "/"; + else + tempdir_name = "_tmp_"; + tempdir_name += proc_program_prefix() + "yosys-abc-XXXXXX"; tempdir_name = make_temp_dir(tempdir_name); if (!lut_mode) diff --git a/passes/techmap/abc9_exe.cc b/passes/techmap/abc9_exe.cc index 2f46c89f4..1d9bb4332 100644 --- a/passes/techmap/abc9_exe.cc +++ b/passes/techmap/abc9_exe.cc @@ -303,8 +303,8 @@ struct Abc9ExePass : public Pass { log("\n"); log(" \n"); log("This pass uses the ABC tool [1] for technology mapping of the top module\n"); - log("(according to the (* top *) attribute or if only one module is currently selected)\n"); - log("to a target FPGA architecture.\n"); + log("(according to the (* top *) attribute or if only one module is currently\n"); + log("selected) to a target FPGA architecture.\n"); log("\n"); log(" -exe <command>\n"); #ifdef ABCEXTERNAL diff --git a/passes/techmap/abc9_ops.cc b/passes/techmap/abc9_ops.cc index acafb0b65..9766e81cb 100644 --- a/passes/techmap/abc9_ops.cc +++ b/passes/techmap/abc9_ops.cc @@ -1572,14 +1572,14 @@ struct Abc9OpsPass : public Pass { log("the `abc9' script pass. Only fully-selected modules are supported.\n"); log("\n"); log(" -check\n"); - log(" check that the design is valid, e.g. (* abc9_box_id *) values are unique,\n"); - log(" (* abc9_carry *) is only given for one input/output port, etc.\n"); + log(" check that the design is valid, e.g. (* abc9_box_id *) values are\n"); + log(" unique, (* abc9_carry *) is only given for one input/output port, etc.\n"); log("\n"); log(" -prep_hier\n"); log(" derive all used (* abc9_box *) or (* abc9_flop *) (if -dff option)\n"); log(" whitebox modules. with (* abc9_flop *) modules, only those containing\n"); - log(" $dff/$_DFF_[NP]_ cells with zero initial state -- due to an ABC limitation\n"); - log(" -- will be derived.\n"); + log(" $dff/$_DFF_[NP]_ cells with zero initial state -- due to an ABC\n"); + log(" limitation -- will be derived.\n"); log("\n"); log(" -prep_bypass\n"); log(" create techmap rules in the '$abc9_map' and '$abc9_unmap' designs for\n"); @@ -1597,33 +1597,35 @@ struct Abc9OpsPass : public Pass { log(" -prep_dff_submod\n"); log(" within (* abc9_flop *) modules, rewrite all edge-sensitive path\n"); log(" declarations and $setup() timing checks ($specify3 and $specrule cells)\n"); - log(" that share a 'DST' port with the $_DFF_[NP]_.Q port from this 'Q' port to\n"); - log(" the DFF's 'D' port. this is to prepare such specify cells to be moved\n"); + log(" that share a 'DST' port with the $_DFF_[NP]_.Q port from this 'Q' port\n"); + log(" to the DFF's 'D' port. this is to prepare such specify cells to be moved\n"); log(" into the flop box.\n"); log("\n"); log(" -prep_dff_unmap\n"); - log(" populate the '$abc9_unmap' design with techmap rules for mapping *_$abc9_flop\n"); - log(" cells back into their derived cell types (where the rules created by\n"); - log(" -prep_hier will then map back to the original cell with parameters).\n"); + log(" populate the '$abc9_unmap' design with techmap rules for mapping\n"); + log(" *_$abc9_flop cells back into their derived cell types (where the rules\n"); + log(" created by -prep_hier will then map back to the original cell with\n"); + log(" parameters).\n"); log("\n"); log(" -prep_delays\n"); log(" insert `$__ABC9_DELAY' blackbox cells into the design to account for\n"); log(" certain required times.\n"); log("\n"); log(" -break_scc\n"); - log(" for an arbitrarily chosen cell in each unique SCC of each selected module\n"); - log(" (tagged with an (* abc9_scc_id = <int> *) attribute) interrupt all wires\n"); - log(" driven by this cell's outputs with a temporary $__ABC9_SCC_BREAKER cell\n"); - log(" to break the SCC.\n"); + log(" for an arbitrarily chosen cell in each unique SCC of each selected\n"); + log(" module (tagged with an (* abc9_scc_id = <int> *) attribute) interrupt\n"); + log(" all wires driven by this cell's outputs with a temporary\n"); + log(" $__ABC9_SCC_BREAKER cell to break the SCC.\n"); log("\n"); log(" -prep_xaiger\n"); log(" prepare the design for XAIGER output. this includes computing the\n"); - log(" topological ordering of ABC9 boxes, as well as preparing the '$abc9_holes'\n"); - log(" design that contains the logic behaviour of ABC9 whiteboxes.\n"); + log(" topological ordering of ABC9 boxes, as well as preparing the \n"); + log(" '$abc9_holes' design that contains the logic behaviour of ABC9\n"); + log(" whiteboxes.\n"); log("\n"); log(" -dff\n"); - log(" consider flop cells (those instantiating modules marked with (* abc9_flop *))\n"); - log(" during -prep_{delays,xaiger,box}.\n"); + log(" consider flop cells (those instantiating modules marked with\n"); + log(" (* abc9_flop *)) during -prep_{delays,xaiger,box}.\n"); log("\n"); log(" -prep_lut <maxlut>\n"); log(" pre-compute the lut library by analysing all modules marked with\n"); @@ -1641,8 +1643,8 @@ struct Abc9OpsPass : public Pass { log("\n"); log(" -reintegrate\n"); log(" for each selected module, re-intergrate the module '<module-name>$abc9'\n"); - log(" by first recovering ABC9 boxes, and then stitching in the remaining primary\n"); - log(" inputs and outputs.\n"); + log(" by first recovering ABC9 boxes, and then stitching in the remaining\n"); + log(" primary inputs and outputs.\n"); log("\n"); } void execute(std::vector<std::string> args, RTLIL::Design *design) override diff --git a/passes/techmap/dfflegalize.cc b/passes/techmap/dfflegalize.cc index 1d99caa3a..c6c3a58c5 100644 --- a/passes/techmap/dfflegalize.cc +++ b/passes/techmap/dfflegalize.cc @@ -118,34 +118,24 @@ struct DffLegalizePass : public Pass { log("- $_DLATCH_[NP][NP][01]_\n"); log("- $_DLATCHSR_[NP][NP][NP]_\n"); log("\n"); - log("The following transformations are performed by this pass:"); - log("\n"); - log("- upconversion from a less capable cell to a more capable cell, if the less"); - log(" capable cell is not supported (eg. dff -> dffe, or adff -> dffsr)"); - log("\n"); - log("- unmapping FFs with clock enable (due to unsupported cell type or -mince)"); - log("\n"); - log("- unmapping FFs with sync reset (due to unsupported cell type or -minsrst)"); - log("\n"); - log("- adding inverters on the control pins (due to unsupported polarity)"); + log("The following transformations are performed by this pass:\n"); log("\n"); + log("- upconversion from a less capable cell to a more capable cell, if the less\n"); + log(" capable cell is not supported (eg. dff -> dffe, or adff -> dffsr)\n"); + log("- unmapping FFs with clock enable (due to unsupported cell type or -mince)\n"); + log("- unmapping FFs with sync reset (due to unsupported cell type or -minsrst)\n"); + log("- adding inverters on the control pins (due to unsupported polarity)\n"); log("- adding inverters on the D and Q pins and inverting the init/reset values\n"); - log(" (due to unsupported init or reset value)"); - log("\n"); - log("- converting sr into adlatch (by tying D to 1 and using E as set input)"); - log("\n"); - log("- emulating unsupported dffsr cell by adff + adff + sr + mux"); - log("\n"); - log("- emulating unsupported dlatchsr cell by adlatch + adlatch + sr + mux"); - log("\n"); + log(" (due to unsupported init or reset value)\n"); + log("- converting sr into adlatch (by tying D to 1 and using E as set input)\n"); + log("- emulating unsupported dffsr cell by adff + adff + sr + mux\n"); + log("- emulating unsupported dlatchsr cell by adlatch + adlatch + sr + mux\n"); log("- emulating adff when the (reset, init) value combination is unsupported by\n"); - log(" dff + adff + dlatch + mux"); - log("\n"); + log(" dff + adff + dlatch + mux\n"); log("- emulating adlatch when the (reset, init) value combination is unsupported by\n"); - log("- dlatch + adlatch + dlatch + mux"); - log("\n"); - log("If the pass is unable to realize a given cell type (eg. adff when only plain dff"); - log("is available), an error is raised."); + log("- dlatch + adlatch + dlatch + mux\n"); + log("If the pass is unable to realize a given cell type (eg. adff when only plain dff\n"); + log("is available), an error is raised.\n"); } // Table of all supported cell types. diff --git a/passes/techmap/dfflibmap.cc b/passes/techmap/dfflibmap.cc index 252baae9a..12c3a95de 100644 --- a/passes/techmap/dfflibmap.cc +++ b/passes/techmap/dfflibmap.cc @@ -431,7 +431,7 @@ struct DfflibmapPass : public Pass { log("cells, leaving remaining internal cells untouched.\n"); log("\n"); log("When called with -info, this command will only print the target cell\n"); - log("list, along with their associated internal cell types, and the arguments"); + log("list, along with their associated internal cell types, and the arguments\n"); log("that would be passed to the dfflegalize pass. The design will not be\n"); log("changed.\n"); log("\n"); diff --git a/passes/techmap/dffunmap.cc b/passes/techmap/dffunmap.cc index 7312015f1..8703bf1a0 100644 --- a/passes/techmap/dffunmap.cc +++ b/passes/techmap/dffunmap.cc @@ -33,8 +33,8 @@ struct DffunmapPass : public Pass { log(" dffunmap [options] [selection]\n"); log("\n"); log("This pass transforms FF types with clock enable and/or synchronous reset into\n"); - log("their base type (with neither clock enable nor sync reset) by emulating the clock\n"); - log("enable and synchronous reset with multiplexers on the cell input.\n"); + log("their base type (with neither clock enable nor sync reset) by emulating the\n"); + log("clock enable and synchronous reset with multiplexers on the cell input.\n"); log("\n"); log(" -ce-only\n"); log(" unmap only clock enables, leave synchronous resets alone.\n"); diff --git a/passes/techmap/flowmap.cc b/passes/techmap/flowmap.cc index dfdbe6b88..579503a0b 100644 --- a/passes/techmap/flowmap.cc +++ b/passes/techmap/flowmap.cc @@ -1406,7 +1406,8 @@ struct FlowmapWorker RTLIL::SigSpec lut_a, lut_y = node; for (auto input_node : input_nodes) lut_a.append(input_node); - lut_a.append(RTLIL::Const(State::Sx, minlut - input_nodes.size())); + if ((int)input_nodes.size() < minlut) + lut_a.append(RTLIL::Const(State::Sx, minlut - input_nodes.size())); RTLIL::Cell *lut = module->addLut(NEW_ID, lut_a, lut_y, lut_table); mapped_nodes.insert(node); diff --git a/passes/techmap/simplemap.cc b/passes/techmap/simplemap.cc index 7d8dba439..f75b82919 100644 --- a/passes/techmap/simplemap.cc +++ b/passes/techmap/simplemap.cc @@ -476,7 +476,8 @@ struct SimplemapPass : public Pass { log(" $not, $pos, $and, $or, $xor, $xnor\n"); log(" $reduce_and, $reduce_or, $reduce_xor, $reduce_xnor, $reduce_bool\n"); log(" $logic_not, $logic_and, $logic_or, $mux, $tribuf\n"); - log(" $sr, $ff, $dff, $dffe, $dffsr, $dffsre, $adff, $adffe, $aldff, $aldffe, $sdff, $sdffe, $sdffce, $dlatch, $adlatch, $dlatchsr\n"); + log(" $sr, $ff, $dff, $dffe, $dffsr, $dffsre, $adff, $adffe, $aldff, $aldffe, $sdff,\n"); + log(" $sdffe, $sdffce, $dlatch, $adlatch, $dlatchsr\n"); log("\n"); } void execute(std::vector<std::string> args, RTLIL::Design *design) override diff --git a/passes/techmap/techmap.cc b/passes/techmap/techmap.cc index 5cd78fe28..144f596c8 100644 --- a/passes/techmap/techmap.cc +++ b/passes/techmap/techmap.cc @@ -1026,8 +1026,8 @@ struct TechmapPass : public Pass { log("When a module in the map file has the 'techmap_celltype' attribute set, it will\n"); log("match cells with a type that match the text value of this attribute. Otherwise\n"); log("the module name will be used to match the cell. Multiple space-separated cell\n"); - log("types can be listed, and wildcards using [] will be expanded (ie. \"$_DFF_[PN]_\"\n"); - log("is the same as \"$_DFF_P_ $_DFF_N_\").\n"); + log("types can be listed, and wildcards using [] will be expanded (ie.\n"); + log("\"$_DFF_[PN]_\" is the same as \"$_DFF_P_ $_DFF_N_\").\n"); log("\n"); log("When a module in the map file has the 'techmap_simplemap' attribute set, techmap\n"); log("will use 'simplemap' (see 'help simplemap') to map cells matching the module.\n"); @@ -1083,11 +1083,11 @@ struct TechmapPass : public Pass { log(" It is possible to combine both prefixes to 'RECURSION; CONSTMAP; '.\n"); log("\n"); log(" _TECHMAP_REMOVEINIT_<port-name>_\n"); - log(" When this wire is set to a constant value, the init attribute of the wire(s)\n"); - log(" connected to this port will be consumed. This wire must have the same\n"); - log(" width as the given port, and for every bit that is set to 1 in the value,\n"); - log(" the corresponding init attribute bit will be changed to 1'bx. If all\n"); - log(" bits of an init attribute are left as x, it will be removed.\n"); + log(" When this wire is set to a constant value, the init attribute of the\n"); + log(" wire(s) connected to this port will be consumed. This wire must have\n"); + log(" the same width as the given port, and for every bit that is set to 1 in\n"); + log(" the value, the corresponding init attribute bit will be changed to 1'bx.\n"); + log(" If all bits of an init attribute are left as x, it will be removed.\n"); log("\n"); log("In addition to this special wires, techmap also supports special parameters in\n"); log("modules in the map file:\n"); @@ -1108,8 +1108,8 @@ struct TechmapPass : public Pass { log("\n"); log(" _TECHMAP_WIREINIT_<port-name>_\n"); log(" When a parameter with this name exists, it will be set to the initial\n"); - log(" value of the wire(s) connected to the given port, as specified by the init\n"); - log(" attribute. If the attribute doesn't exist, x will be filled for the\n"); + log(" value of the wire(s) connected to the given port, as specified by the\n"); + log(" init attribute. If the attribute doesn't exist, x will be filled for the\n"); log(" missing bits. To remove the init attribute bits used, use the\n"); log(" _TECHMAP_REMOVEINIT_*_ wires.\n"); log("\n"); diff --git a/techlibs/achronix/speedster22i/cells_sim.v b/techlibs/achronix/speedster22i/cells_sim.v index 6c87adb94..fc15e0966 100644 --- a/techlibs/achronix/speedster22i/cells_sim.v +++ b/techlibs/achronix/speedster22i/cells_sim.v @@ -68,9 +68,8 @@ end assign dout = combout_rt & 1'b1; endmodule -module DFF (output q, +module DFF (output reg q, input d, ck); - reg q; always @(posedge ck) q <= d; diff --git a/techlibs/ice40/synth_ice40.cc b/techlibs/ice40/synth_ice40.cc index 1174f6e04..2ae859efe 100644 --- a/techlibs/ice40/synth_ice40.cc +++ b/techlibs/ice40/synth_ice40.cc @@ -45,8 +45,8 @@ struct SynthIce40Pass : public ScriptPass log("This command runs synthesis for iCE40 FPGAs.\n"); log("\n"); log(" -device < hx | lp | u >\n"); - log(" relevant only for '-abc9' flow, optimise timing for the specified device.\n"); - log(" default: hx\n"); + log(" relevant only for '-abc9' flow, optimise timing for the specified\n"); + log(" device. default: hx\n"); log("\n"); log(" -top <module>\n"); log(" use the specified module as top module\n"); diff --git a/techlibs/intel/synth_intel.cc b/techlibs/intel/synth_intel.cc index 166c81843..e9594e6d8 100644 --- a/techlibs/intel/synth_intel.cc +++ b/techlibs/intel/synth_intel.cc @@ -39,21 +39,22 @@ struct SynthIntelPass : public ScriptPass { log(" -family <max10 | cyclone10lp | cycloneiv | cycloneive>\n"); log(" generate the synthesis netlist for the specified family.\n"); log(" MAX10 is the default target if no family argument specified.\n"); - log(" For Cyclone IV GX devices, use cycloneiv argument; for Cyclone IV E, use cycloneive.\n"); - log(" For Cyclone V and Cyclone 10 GX, use the synth_intel_alm backend instead.\n"); + log(" For Cyclone IV GX devices, use cycloneiv argument; for Cyclone IV E, use\n"); + log(" cycloneive. For Cyclone V and Cyclone 10 GX, use the synth_intel_alm\n"); + log(" backend instead.\n"); log("\n"); log(" -top <module>\n"); log(" use the specified module as top module (default='top')\n"); log("\n"); log(" -vqm <file>\n"); - log(" write the design to the specified Verilog Quartus Mapping File. Writing of an\n"); - log(" output file is omitted if this parameter is not specified.\n"); + log(" write the design to the specified Verilog Quartus Mapping File. Writing\n"); + log(" of an output file is omitted if this parameter is not specified.\n"); log(" Note that this backend has not been tested and is likely incompatible\n"); log(" with recent versions of Quartus.\n"); log("\n"); log(" -vpr <file>\n"); - log(" write BLIF files for VPR flow experiments. The synthesized BLIF output file is not\n"); - log(" compatible with the Quartus flow. Writing of an\n"); + log(" write BLIF files for VPR flow experiments. The synthesized BLIF output\n"); + log(" file is not compatible with the Quartus flow. Writing of an\n"); log(" output file is omitted if this parameter is not specified.\n"); log("\n"); log(" -run <from_label>:<to_label>\n"); diff --git a/techlibs/intel_alm/synth_intel_alm.cc b/techlibs/intel_alm/synth_intel_alm.cc index 43d3592d5..c33eb43bf 100644 --- a/techlibs/intel_alm/synth_intel_alm.cc +++ b/techlibs/intel_alm/synth_intel_alm.cc @@ -43,21 +43,24 @@ struct SynthIntelALMPass : public ScriptPass { log(" -family <family>\n"); log(" target one of:\n"); log(" \"cyclonev\" - Cyclone V (default)\n"); - log(" \"arriav\" - Arria V (non-GZ)"); + log(" \"arriav\" - Arria V (non-GZ)\n"); log(" \"cyclone10gx\" - Cyclone 10GX\n"); log("\n"); log(" -vqm <file>\n"); - log(" write the design to the specified Verilog Quartus Mapping File. Writing of an\n"); - log(" output file is omitted if this parameter is not specified. Implies -quartus.\n"); + log(" write the design to the specified Verilog Quartus Mapping File. Writing\n"); + log(" of an output file is omitted if this parameter is not specified. Implies\n"); + log(" -quartus.\n"); log("\n"); log(" -noflatten\n"); - log(" do not flatten design before synthesis; useful for per-module area statistics\n"); + log(" do not flatten design before synthesis; useful for per-module area\n"); + log(" statistics\n"); log("\n"); log(" -quartus\n"); log(" output a netlist using Quartus cells instead of MISTRAL_* cells\n"); log("\n"); log(" -dff\n"); - log(" pass DFFs to ABC to perform sequential logic optimisations (EXPERIMENTAL)\n"); + log(" pass DFFs to ABC to perform sequential logic optimisations\n"); + log(" (EXPERIMENTAL)\n"); log("\n"); log(" -run <from_label>:<to_label>\n"); log(" only run the commands between the labels (see below). an empty\n"); diff --git a/techlibs/quicklogic/synth_quicklogic.cc b/techlibs/quicklogic/synth_quicklogic.cc index 754de2de6..94bd44db0 100644 --- a/techlibs/quicklogic/synth_quicklogic.cc +++ b/techlibs/quicklogic/synth_quicklogic.cc @@ -48,8 +48,8 @@ struct SynthQuickLogicPass : public ScriptPass { log(" is omitted if this parameter is not specified.\n"); log("\n"); log(" -verilog <file>\n"); - log(" write the design to the specified verilog file. writing of an output file\n"); - log(" is omitted if this parameter is not specified.\n"); + log(" write the design to the specified verilog file. writing of an output\n"); + log(" file is omitted if this parameter is not specified.\n"); log("\n"); log(" -abc\n"); log(" use old ABC flow, which has generally worse mapping results but is less\n"); diff --git a/techlibs/sf2/NOTES.txt b/techlibs/sf2/NOTES.txt new file mode 100644 index 000000000..67784b546 --- /dev/null +++ b/techlibs/sf2/NOTES.txt @@ -0,0 +1,84 @@ +Using yosys with Libero Soc +=========================== + +Yosys does synthesis and therefore could be used instead of Synplify in +the Libero workflow. You still have to use LiberoSoc for place, route, +bitsteam generation, timing analysis... + +This is unfortunately not trivial, but this is also not too difficult. +When you run the Synthesize step, three tools are executed one after the other. + +You'd better to write a simple script, like this one (assuming the top module +is top): + +----------- run_yosys.sh -------------- +#!/bin/sh + +set -e + +yosys -p 'read_verilog hdl/top.v; synth_sf2; write_verilog -defparam synthesis/top_yosys.v' + +rwnetlist64 --script yosys/rwnetlist.tcl + +echo "##### run g4compile" + +g4compile --script yosys/run_compile.tcl + +libero SCRIPT:run_yosys.tcl +------------------------------------ + +Yosys will do the synthesis and write a netlist in verilog. Then you have +to call microsemi tools to build the netlist for the P&R tools. + +The first one do a file format conversion. During the normal workflow, the +tcl file is created in a temporary file. You can use this one: + +------------- tcl/rwnetlist.tcl --------- +set_device -fam SmartFusion2 +read_verilog \ + -file {../synthesis/top_yosys.v} +write_adl -file {../designer/top/top.adl} +---------------------------------------- + +Probably, you will have to change the family for Igloo2. + +The second command link the netlists. The tcl script is generated by +liberoSoc in designer/top/run_compile.tcl. You can use it as it. +The "Source Files" value could be changed but it looks to have no effect. +This commands create the .afl file. + +Then you can use the normal flow. This is done by the run_yosys.tcl: + +----------- run_yosys.tcl -------------- +open_project -file {./top.prjx} +run_tool -name {PLACEROUTE} +run_tool -name {PROGRAMDEVICE} +----------------------------------------- + + +Using MSS, HPMS or other IPs +============================ + +This works. You'd better to configure CCC (~ the PLL) and the MSS using +liberoSoc as the configuration bits are not documented. +Then you have to manually gather the HDL sources generated for the IPs. +They are in the component subdirectory. Sometimes there are both a _syn and +a _pre version of the same file. They are for symplify and precision. +Use only once, the symplify version should be OK. For the MSS, these are the +blackboxes, so you don't need them. + +SYSRESET and XTLOSC have one fake port. This is handled, provided you use +the blackbox module declared by Yosys in cell_sim.v. This is OK by default +too. + + +What is missing +=============== + +Always flatten your design (this is the default). Hierarchical designs +don't work. + +Constraints (SDC files) are not supported by Yosys. Furthermore, due to +flattening and optimization, nets name may change. + +More testing... diff --git a/techlibs/sf2/arith_map.v b/techlibs/sf2/arith_map.v index f16b1abb8..eb367799b 100644 --- a/techlibs/sf2/arith_map.v +++ b/techlibs/sf2/arith_map.v @@ -17,5 +17,53 @@ * */ +(* techmap_celltype = "$alu" *) +module \$__SF2_ALU (A, B, CI, BI, X, Y, CO); + parameter A_SIGNED = 0; + parameter B_SIGNED = 0; + parameter A_WIDTH = 1; + parameter B_WIDTH = 1; + parameter Y_WIDTH = 1; + + (* force_downto *) + input [A_WIDTH-1:0] A; + (* force_downto *) + input [B_WIDTH-1:0] B; + (* force_downto *) + output [Y_WIDTH-1:0] X, Y; + + input CI, BI; + (* force_downto *) + output [Y_WIDTH-1:0] CO; + + wire _TECHMAP_FAIL_ = Y_WIDTH <= 2; + + (* force_downto *) + wire [Y_WIDTH-1:0] AA, BB; + \$pos #(.A_SIGNED(A_SIGNED), .A_WIDTH(A_WIDTH), .Y_WIDTH(Y_WIDTH)) A_conv (.A(A), .Y(AA)); + \$pos #(.A_SIGNED(B_SIGNED), .A_WIDTH(B_WIDTH), .Y_WIDTH(Y_WIDTH)) B_conv (.A(B), .Y(BB)); + + (* force_downto *) + wire [Y_WIDTH-1:0] C = {CO, CI}; + + genvar i; + generate for (i = 0; i < Y_WIDTH; i = i + 1) begin:slice + ARI1 #( + // G = F1 = A[i] & (B[i]^BI) + // Y = F0 = A[i]^B[i]^BI + // P = Y + // ADCB + .INIT(20'b 01_11_0010_1000_1001_0110) + ) carry ( + .A(1'b0), + .B(AA[i]), + .C(BB[i]), + .D(BI), + .FCI(C[i]), + .Y(X[i]), + .S(Y[i]), + .FCO(CO[i]) + ); + end endgenerate +endmodule -// nothing here yet diff --git a/techlibs/sf2/cells_sim.v b/techlibs/sf2/cells_sim.v index 4b57bad7b..b5438e44c 100644 --- a/techlibs/sf2/cells_sim.v +++ b/techlibs/sf2/cells_sim.v @@ -152,12 +152,26 @@ module SLE ( assign Q = LAT ? q_latch : q_ff; endmodule -// module AR1 +module ARI1 ( + input A, B, C, D, FCI, + output Y, S, FCO +); + parameter [19:0] INIT = 20'h0; + wire [2:0] Fsel = {D, C, B}; + wire F0 = INIT[Fsel]; + wire F1 = INIT[8 + Fsel]; + wire Yout = A ? F1 : F0; + assign Y = Yout; + assign S = FCI ^ Yout; + wire G = INIT[16] ? (INIT[17] ? F1 : F0) : INIT[17]; + wire P = INIT[19] ? 1'b1 : (INIT[18] ? Yout : 1'b0); + assign FCO = P ? FCI : G; +endmodule + // module FCEND_BUFF // module FCINIT_BUFF // module FLASH_FREEZE // module OSCILLATOR -// module SYSRESET // module SYSCTRL_RESET_STATUS // module LIVE_PROBE_FB @@ -333,6 +347,7 @@ module BIBUF ( inout PAD, output Y ); + parameter IOSTD = ""; assign PAD = E ? D : 1'bz; assign Y = PAD; endmodule @@ -347,6 +362,7 @@ module BIBUF_DIFF ( inout PADN, output Y ); + parameter IOSTD = ""; endmodule module CLKBIBUF ( @@ -357,6 +373,7 @@ module CLKBIBUF ( (* clkbuf_driver *) output Y ); + parameter IOSTD = ""; assign PAD = E ? D : 1'bz; assign Y = PAD; endmodule @@ -367,6 +384,7 @@ module CLKBUF ( (* clkbuf_driver *) output Y ); + parameter IOSTD = ""; assign Y = PAD; endmodule @@ -379,6 +397,7 @@ module CLKBUF_DIFF ( (* clkbuf_driver *) output Y ); + parameter IOSTD = ""; endmodule module INBUF ( @@ -386,6 +405,7 @@ module INBUF ( input PAD, output Y ); + parameter IOSTD = ""; assign Y = PAD; endmodule @@ -397,6 +417,7 @@ module INBUF_DIFF ( input PADN, output Y ); + parameter IOSTD = ""; endmodule module OUTBUF ( @@ -404,6 +425,7 @@ module OUTBUF ( (* iopad_external_pin *) output PAD ); + parameter IOSTD = ""; assign PAD = D; endmodule @@ -415,6 +437,7 @@ module OUTBUF_DIFF ( (* iopad_external_pin *) output PADN ); + parameter IOSTD = ""; endmodule module TRIBUFF ( @@ -423,6 +446,7 @@ module TRIBUFF ( (* iopad_external_pin *) output PAD ); + parameter IOSTD = ""; assign PAD = E ? D : 1'bz; endmodule @@ -435,6 +459,7 @@ module TRIBUFF_DIFF ( (* iopad_external_pin *) output PADN ); + parameter IOSTD = ""; endmodule // module DDR_IN @@ -442,3 +467,113 @@ endmodule // module RAM1K18 // module RAM64x18 // module MACC + +(* blackbox *) +module SYSRESET ( + (* iopad_external_pin *) + input DEVRST_N, + output POWER_ON_RESET_N); +endmodule + + +(* blackbox *) +module XTLOSC ( + (* iopad_external_pin *) + input XTL, + output CLKOUT); + parameter [1:0] MODE = 2'h3; + parameter real FREQUENCY = 20.0; +endmodule + +(* blackbox *) +module RAM1K18 ( + input [13:0] A_ADDR, + input [2:0] A_BLK, + (* clkbuf_sink *) + input A_CLK, + input [17:0] A_DIN, + output [17:0] A_DOUT, + input [1:0] A_WEN, + input [2:0] A_WIDTH, + input A_WMODE, + input A_ARST_N, + input A_DOUT_LAT, + input A_DOUT_ARST_N, + (* clkbuf_sink *) + input A_DOUT_CLK, + input A_DOUT_EN, + input A_DOUT_SRST_N, + + input [13:0] B_ADDR, + input [2:0] B_BLK, + (* clkbuf_sink *) + input B_CLK, + input [17:0] B_DIN, + output [17:0] B_DOUT, + input [1:0] B_WEN, + input [2:0] B_WIDTH, + input B_WMODE, + input B_ARST_N, + input B_DOUT_LAT, + input B_DOUT_ARST_N, + (* clkbuf_sink *) + input B_DOUT_CLK, + input B_DOUT_EN, + input B_DOUT_SRST_N, + + input A_EN, + input B_EN, + input SII_LOCK, + output BUSY); +endmodule + +(* blackbox *) +module RAM64x18 ( + input [9:0] A_ADDR, + input [1:0] A_BLK, + input [2:0] A_WIDTH, + output [17:0] A_DOUT, + input A_DOUT_ARST_N, + (* clkbuf_sink *) + input A_DOUT_CLK, + input A_DOUT_EN, + input A_DOUT_LAT, + input A_DOUT_SRST_N, + (* clkbuf_sink *) + input A_ADDR_CLK, + input A_ADDR_EN, + input A_ADDR_LAT, + input A_ADDR_SRST_N, + input A_ADDR_ARST_N, + + input [9:0] B_ADDR, + input [1:0] B_BLK, + input [2:0] B_WIDTH, + output [17:0] B_DOUT, + input B_DOUT_ARST_N, + (* clkbuf_sink *) + input B_DOUT_CLK, + input B_DOUT_EN, + input B_DOUT_LAT, + input B_DOUT_SRST_N, + (* clkbuf_sink *) + input B_ADDR_CLK, + input B_ADDR_EN, + input B_ADDR_LAT, + input B_ADDR_SRST_N, + input B_ADDR_ARST_N, + + input [9:0] C_ADDR, + (* clkbuf_sink *) + input C_CLK, + input [17:0] C_DIN, + input C_WEN, + input [1:0] C_BLK, + input [2:0] C_WIDTH, + + input A_EN, + input B_EN, + input C_EN, + input SII_LOCK, + output BUSY); +endmodule diff --git a/techlibs/sf2/synth_sf2.cc b/techlibs/sf2/synth_sf2.cc index 8d78a6097..bf4a6e031 100644 --- a/techlibs/sf2/synth_sf2.cc +++ b/techlibs/sf2/synth_sf2.cc @@ -45,8 +45,8 @@ struct SynthSf2Pass : public ScriptPass log(" is omitted if this parameter is not specified.\n"); log("\n"); log(" -vlog <file>\n"); - log(" write the design to the specified Verilog file. writing of an output file\n"); - log(" is omitted if this parameter is not specified.\n"); + log(" write the design to the specified Verilog file. writing of an output\n"); + log(" file is omitted if this parameter is not specified.\n"); log("\n"); log(" -json <file>\n"); log(" write the design to the specified JSON file. writing of an output file\n"); @@ -66,6 +66,9 @@ struct SynthSf2Pass : public ScriptPass log(" -clkbuf\n"); log(" insert direct PAD->global_net buffers\n"); log("\n"); + log(" -discard-ffinit\n"); + log(" discard FF init value instead of emitting an error\n"); + log("\n"); log(" -retime\n"); log(" run 'abc' with '-dff -D 1' options\n"); log("\n"); @@ -76,7 +79,7 @@ struct SynthSf2Pass : public ScriptPass } string top_opt, edif_file, vlog_file, json_file; - bool flatten, retime, iobs, clkbuf; + bool flatten, retime, iobs, clkbuf, discard_ffinit; void clear_flags() override { @@ -88,6 +91,7 @@ struct SynthSf2Pass : public ScriptPass retime = false; iobs = true; clkbuf = false; + discard_ffinit = false; } void execute(std::vector<std::string> args, RTLIL::Design *design) override @@ -138,6 +142,10 @@ struct SynthSf2Pass : public ScriptPass clkbuf = true; continue; } + if (args[argidx] == "-discard-ffinit") { + discard_ffinit = true; + continue; + } break; } extra_args(args, argidx, design); @@ -171,6 +179,8 @@ struct SynthSf2Pass : public ScriptPass if (check_label("coarse")) { + if (discard_ffinit || help_mode) + run("attrmap -remove init", "(only if -discard-ffinit)"); run("synth -run coarse"); } @@ -218,9 +228,9 @@ struct SynthSf2Pass : public ScriptPass } else { run("clkbufmap -buf CLKINT Y:A"); } - run("iopadmap -bits -inpad INBUF Y:PAD -outpad OUTBUF D:PAD -toutpad TRIBUFF E:D:PAD -tinoutpad BIBUF E:Y:D:PAD", "(unless -noiobs"); + run("iopadmap -bits -inpad INBUF Y:PAD -outpad OUTBUF D:PAD -toutpad TRIBUFF E:D:PAD -tinoutpad BIBUF E:Y:D:PAD", "(unless -noiobs)"); } - run("clean"); + run("clean -purge"); } if (check_label("check")) diff --git a/techlibs/sf2/tests/test_arith.ys b/techlibs/sf2/tests/test_arith.ys new file mode 100644 index 000000000..da7b96602 --- /dev/null +++ b/techlibs/sf2/tests/test_arith.ys @@ -0,0 +1,22 @@ +# Our implementation +read_verilog ../arith_map.v +read_verilog ../cells_sim.v +read_verilog -DSIMLIB_NOCHECKS ../../common/simlib.v +rename \$__SF2_ALU gate +hierarchy -top gate -chparam A_WIDTH 4 -chparam B_WIDTH 5 -chparam Y_WIDTH 5 +flatten +opt +write_verilog gate.v + +# The reference +read_verilog -DSIMLIB_NOCHECKS ../../common/simlib.v +rename \$alu gold +hierarchy -top gold -chparam A_WIDTH 4 -chparam B_WIDTH 5 -chparam Y_WIDTH 5 +flatten +proc +clean +write_verilog gold.v + +read_verilog gate.v +miter -equiv -flatten -make_outputs gold gate miter +sat -verify -prove trigger 0 -show-ports miter diff --git a/techlibs/xilinx/synth_xilinx.cc b/techlibs/xilinx/synth_xilinx.cc index 6214e1411..a242cdef1 100644 --- a/techlibs/xilinx/synth_xilinx.cc +++ b/techlibs/xilinx/synth_xilinx.cc @@ -93,7 +93,8 @@ struct SynthXilinxPass : public ScriptPass log(" do not use XORCY/MUXCY/CARRY4 cells in output netlist\n"); log("\n"); log(" -nowidelut\n"); - log(" do not use MUXF[5-9] resources to implement LUTs larger than native for the target\n"); + log(" do not use MUXF[5-9] resources to implement LUTs larger than native for\n"); + log(" the target\n"); log("\n"); log(" -nodsp\n"); log(" do not use DSP48*s to implement multipliers and associated logic\n"); @@ -109,8 +110,8 @@ struct SynthXilinxPass : public ScriptPass log(" infer URAM288s for large memories (xcup only)\n"); log("\n"); log(" -widemux <int>\n"); - log(" enable inference of hard multiplexer resources (MUXF[78]) for muxes at or\n"); - log(" above this number of inputs (minimum value 2, recommended value >= 5).\n"); + log(" enable inference of hard multiplexer resources (MUXF[78]) for muxes at\n"); + log(" or above this number of inputs (minimum value 2, recommended value >= 5)\n"); log(" default: 0 (no inference)\n"); log("\n"); log(" -run <from_label>:<to_label>\n"); diff --git a/tests/simple/memory.v b/tests/simple/memory.v index f38bdafd3..b478d9409 100644 --- a/tests/simple/memory.v +++ b/tests/simple/memory.v @@ -137,8 +137,13 @@ endmodule // ---------------------------------------------------------- -module memtest06_sync(input clk, input rst, input [2:0] idx, input [7:0] din, output [7:0] dout); +module memtest06_sync(clk, rst, idx, din, dout); + input clk; + input rst; (* gentb_constant=0 *) wire rst; + input [2:0] idx; + input [7:0] din; + output [7:0] dout; reg [7:0] test [0:7]; integer i; always @(posedge clk) begin @@ -156,8 +161,13 @@ module memtest06_sync(input clk, input rst, input [2:0] idx, input [7:0] din, ou assign dout = test[idx]; endmodule -module memtest06_async(input clk, input rst, input [2:0] idx, input [7:0] din, output [7:0] dout); +module memtest06_async(clk, rst, idx, din, dout); + input clk; + input rst; (* gentb_constant=0 *) wire rst; + input [2:0] idx; + input [7:0] din; + output [7:0] dout; reg [7:0] test [0:7]; integer i; always @(posedge clk or posedge rst) begin diff --git a/tests/various/bug3462.ys b/tests/various/bug3462.ys new file mode 100644 index 000000000..c85dc9470 --- /dev/null +++ b/tests/various/bug3462.ys @@ -0,0 +1,12 @@ +read_verilog <<EOT +module top(); + wire array[0:0]; + wire out; + sub #(.d(1)) inst( + .in(array[0]), + .out(out) + ); +endmodule +EOT + +hierarchy -top top -libdir . diff --git a/tests/various/sub.v b/tests/various/sub.v new file mode 100644 index 000000000..63422ca5c --- /dev/null +++ b/tests/various/sub.v @@ -0,0 +1,3 @@ +module sub #(parameter d=1) (input in, output out); + assign out = in; +endmodule |