diff options
32 files changed, 350 insertions, 77 deletions
diff --git a/.github/issue_template.md b/.github/issue_template.md index 24e91a4e..4563a71d 100644 --- a/.github/issue_template.md +++ b/.github/issue_template.md @@ -1,7 +1,7 @@ ## Steps to reproduce the issue *Provide instructions for reproducing the issue. Make sure to include -all neccessary source files. (You can simply drag&drop a .zip file into +all necessary source files. (You can simply drag&drop a .zip file into the issue editor.)* ## Expected behavior @@ -3,9 +3,116 @@ List of major changes and improvements between releases ======================================================= -Yosys 0.7 .. Yosys ??? +Yosys 0.7 .. Yosys 0.8 ---------------------- + * Various + - Many bugfixes and small improvements + - Strip debug symbols from installed binary + - Replace -ignore_redef with -[no]overwrite in front-ends + - Added write_verilog hex dump support, add -nohex option + - Added "write_verilog -decimal" + - Added "scc -set_attr" + - Added "verilog_defines" command + - Remeber defines from one read_verilog to next + - Added support for hierarchical defparam + - Added FIRRTL back-end + - Improved ABC default scripts + - Added "design -reset-vlog" + - Added "yosys -W regex", "yosys -w regex", and "yosys -e regex" + - Added Verilog $rtoi and $itor support + - Added "check -initdrv" + - Added "read_blif -wideports" + - Added support for systemVerilog "++" and "--" operators + - Added support for SystemVerilog unique, unique0, and priority case + - Added "write_edif" options for edif "flavors" + - Added support for resetall compiler directive + - Added simple C beck-end (bitwise combinatorical only atm) + - Added $_ANDNOT_ and $_ORNOT_ cell types + - Added cell library aliases to "abc -g" + - Added "setundef -anyseq" + - Added "chtype" command + - Added "design -import" + - Added "write_table" command + - Added "read_json" command + - Added "sim" command + - Added "extract_fa" and "extract_reduce" commands + - Added "extract_counter" command + - Added "opt_demorgan" command + - Added support for $size and $bits SystemVerilog functions + - Added "blackbox" command + - Added "ltp" command + - Added support for editline as replacement for readline + - Added warnings for driver-driver conflicts between FFs (and other cells) and constants + - Added "yosys -E" for creating Makefile dependencies files + - Added "synth -noshare" + - Added "memory_nordff" + - Added "setundef -undef -expose -anyconst" + - Added "expose -input" + - Added specify/specparam parser support (simply ignore them) + - Added "write_blif -inames -iattr" + - Added "hierarchy -simcheck" + - Added an option to statically link abc into yosys + - Added protobuf back-end + - Added BLIF parsing support for .conn and .cname + - Added read_verilog error checking for reg/wire/logic misuse + - Added "make coverage" and ENABLE_GCOV build option + + * Changes in Yosys APIs + - Added ConstEval defaultval feature + - Added {get,set}_src_attribute() methods on RTLIL::AttrObject + - Added SigSpec::is_fully_ones() and Const::is_fully_ones() + - Added log_file_warning() and log_file_error() functions + + * Formal Verification + - Added "write_aiger" + - Added "yosys-smtbmc --aig" + - Added "always <positive_int>" to .smtc format + - Added $cover cell type and support for cover properties + - Added $fair/$live cell type and support for liveness properties + - Added smtbmc support for memory vcd dumping + - Added "chformal" command + - Added "write_smt2 -stbv" and "write_smt2 -stdt" + - Fix equiv_simple, old behavior now available with "equiv_simple -short" + - Change to Yices2 as default SMT solver (it is GPL now) + - Added "yosys-smtbmc --presat" (now default in SymbiYosys) + - Added "yosys-smtbmc --smtc-init --smtc-top --noinit" + - Added a brand new "write_btor" command for BTOR2 + - Added clk2fflogic memory support and other improvements + - Added "async memory write" support to write_smt2 + - Simulate clock toggling in yosys-smtbmc VCD output + - Added $allseq/$allconst cells for EA-solving + - Make -nordff the default in "prep" + - Added (* gclk *) attribute + - Added "async2sync" pass for single-clock designs with async resets + + * Verific support + - Many improvements in Verific front-end + - Added proper handling of concurent SVA properties + - Map "const" and "rand const" to $anyseq/$anyconst + - Added "verific -import -flatten" and "verific -import -extnets" + - Added "verific -vlog-incdir -vlog-define -vlog-libdir" + - Remove PSL support (because PSL has been removed in upstream Verific) + - Improve integration with "hierarchy" command design elaboration + - Added YOSYS_NOVERIFIC for running non-verific test cases with verific bin + - Added simpilied "read" command that automatically uses verific if available + - Added "verific -set-<severity> <msg_id>.." + - Added "verific -work <libname>" + + * New back-ends + - Added initial Coolrunner-II support + - Added initial eASIC support + - Added initial ECP5 support + + * GreenPAK Support + - Added support for GP_DLATCH, GP_SPI, GP_DCMx, GP_COUNTx, etc. + + * iCE40 Support + - Add "synth_ice40 -vpr" + - Add "synth_ice40 -nodffe" + - Add "synth_ice40 -json" + - Add Support for UltraPlus cells + * MAX10 and Cyclone IV Support - Added initial version of metacommand "synth_intel". - Improved write_verilog command to produce VQM netlist for Quartus Prime. @@ -14,6 +121,7 @@ Yosys 0.7 .. Yosys ??? - Added example of implementation for DE2i-150 board. - Added example of implementation for MAX10 development kit. - Added LFSR example from Asic World. + - Added "dffinit -highlow" for mapping to Intel primitives Yosys 0.6 .. Yosys 0.7 @@ -175,6 +175,12 @@ LD = gcc-4.8 CXXFLAGS += -std=c++11 -Os ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H" +else ifeq ($(CONFIG),cygwin) +CXX = gcc +LD = gcc +CXXFLAGS += -std=gnu++11 -Os +ABCMKARGS += ARCHFLAGS="-DABC_USE_STDINT_H" + else ifeq ($(CONFIG),emcc) CXX = emcc LD = emcc @@ -729,6 +735,9 @@ config-msys2: clean config-msys2-64: clean echo 'CONFIG := msys2-64' > Makefile.conf +config-cygwin: clean + echo 'CONFIG := cygwin' > Makefile.conf + config-gcov: clean echo 'CONFIG := gcc' > Makefile.conf echo 'ENABLE_GCOV := 1' >> Makefile.conf @@ -69,6 +69,10 @@ On FreeBSD use the following command to install all prerequisites: On FreeBSD system use gmake instead of make. To run tests use: % MAKE=gmake CC=cc gmake test +For Cygwin use the following command to install all prerequisites, or select these additional packages: + + setup-x86_64.exe -q --packages=bison,flex,gcc-core,gcc-g++,git,libffi-devel,libreadline-devel,make,pkg-config,python3,tcl-devel + There are also pre-compiled Yosys binary packages for Ubuntu and Win32 as well as a source distribution for Visual Studio. Visit the Yosys download page for more information: http://www.clifford.at/yosys/download.html diff --git a/backends/edif/edif.cc b/backends/edif/edif.cc index 5f9ec54f..d4e56a9e 100644 --- a/backends/edif/edif.cc +++ b/backends/edif/edif.cc @@ -106,6 +106,9 @@ struct EdifBackend : public Backend { log(" if the design contains constant nets. use \"hilomap\" to map to custom\n"); log(" constant drivers first)\n"); log("\n"); + log(" -attrprop\n"); + log(" create EDIF properties for cell attributes\n"); + log("\n"); log(" -pvector {par|bra|ang}\n"); log(" sets the delimiting character for module port rename clauses to\n"); log(" parentheses, square brackets, or angle brackets.\n"); @@ -121,6 +124,7 @@ struct EdifBackend : public Backend { log_header(design, "Executing EDIF backend.\n"); std::string top_module_name; bool port_rename = false; + bool attr_properties = false; std::map<RTLIL::IdString, std::map<RTLIL::IdString, int>> lib_cell_ports; bool nogndvcc = false; CellTypes ct(design); @@ -137,6 +141,10 @@ struct EdifBackend : public Backend { nogndvcc = true; continue; } + if (args[argidx] == "-attrprop") { + attr_properties = true; + continue; + } if (args[argidx] == "-pvector" && argidx+1 < args.size()) { std::string parray; port_rename = true; @@ -332,24 +340,33 @@ struct EdifBackend : public Backend { *f << stringf(" (instance %s\n", EDIF_DEF(cell->name)); *f << stringf(" (viewRef VIEW_NETLIST (cellRef %s%s))", EDIF_REF(cell->type), lib_cell_ports.count(cell->type) > 0 ? " (libraryRef LIB)" : ""); - for (auto &p : cell->parameters) - if ((p.second.flags & RTLIL::CONST_FLAG_STRING) != 0) - *f << stringf("\n (property %s (string \"%s\"))", EDIF_DEF(p.first), p.second.decode_string().c_str()); - else if (p.second.bits.size() <= 32 && RTLIL::SigSpec(p.second).is_fully_def()) - *f << stringf("\n (property %s (integer %u))", EDIF_DEF(p.first), p.second.as_int()); + + auto add_prop = [&](IdString name, Const val) { + if ((val.flags & RTLIL::CONST_FLAG_STRING) != 0) + *f << stringf("\n (property %s (string \"%s\"))", EDIF_DEF(name), val.decode_string().c_str()); + else if (val.bits.size() <= 32 && RTLIL::SigSpec(val).is_fully_def()) + *f << stringf("\n (property %s (integer %u))", EDIF_DEF(name), val.as_int()); else { std::string hex_string = ""; - for (size_t i = 0; i < p.second.bits.size(); i += 4) { + for (size_t i = 0; i < val.bits.size(); i += 4) { int digit_value = 0; - if (i+0 < p.second.bits.size() && p.second.bits.at(i+0) == RTLIL::State::S1) digit_value |= 1; - if (i+1 < p.second.bits.size() && p.second.bits.at(i+1) == RTLIL::State::S1) digit_value |= 2; - if (i+2 < p.second.bits.size() && p.second.bits.at(i+2) == RTLIL::State::S1) digit_value |= 4; - if (i+3 < p.second.bits.size() && p.second.bits.at(i+3) == RTLIL::State::S1) digit_value |= 8; + if (i+0 < val.bits.size() && val.bits.at(i+0) == RTLIL::State::S1) digit_value |= 1; + if (i+1 < val.bits.size() && val.bits.at(i+1) == RTLIL::State::S1) digit_value |= 2; + if (i+2 < val.bits.size() && val.bits.at(i+2) == RTLIL::State::S1) digit_value |= 4; + if (i+3 < val.bits.size() && val.bits.at(i+3) == RTLIL::State::S1) digit_value |= 8; char digit_str[2] = { "0123456789abcdef"[digit_value], 0 }; hex_string = std::string(digit_str) + hex_string; } - *f << stringf("\n (property %s (string \"%d'h%s\"))", EDIF_DEF(p.first), GetSize(p.second.bits), hex_string.c_str()); + *f << stringf("\n (property %s (string \"%d'h%s\"))", EDIF_DEF(name), GetSize(val.bits), hex_string.c_str()); } + }; + + for (auto &p : cell->parameters) + add_prop(p.first, p.second); + if (attr_properties) + for (auto &p : cell->attributes) + add_prop(p.first, p.second); + *f << stringf(")\n"); for (auto &p : cell->connections()) { RTLIL::SigSpec sig = sigmap(p.second); diff --git a/backends/firrtl/firrtl.cc b/backends/firrtl/firrtl.cc index 94236d0b..32410a65 100644 --- a/backends/firrtl/firrtl.cc +++ b/backends/firrtl/firrtl.cc @@ -33,22 +33,22 @@ dict<IdString, string> namecache; int autoid_counter; typedef unsigned FDirection; -static const FDirection NODIRECTION = 0x0; -static const FDirection IN = 0x1; -static const FDirection OUT = 0x2; -static const FDirection INOUT = 0x3; +static const FDirection FD_NODIRECTION = 0x0; +static const FDirection FD_IN = 0x1; +static const FDirection FD_OUT = 0x2; +static const FDirection FD_INOUT = 0x3; // Get a port direction with respect to a specific module. FDirection getPortFDirection(IdString id, Module *module) { Wire *wire = module->wires_.at(id); - FDirection direction = NODIRECTION; + FDirection direction = FD_NODIRECTION; if (wire && wire->port_id) { if (wire->port_input) - direction |= IN; + direction |= FD_IN; if (wire->port_output) - direction |= OUT; + direction |= FD_OUT; } return direction; } @@ -193,16 +193,16 @@ struct FirrtlWorker FDirection dir = getPortFDirection(it->first, instModule); std::string source, sink; switch (dir) { - case INOUT: + case FD_INOUT: log_warning("Instance port connection %s.%s is INOUT; treating as OUT\n", log_id(cell_type), log_signal(it->second)); - case OUT: + case FD_OUT: source = firstName; sink = secondName; break; - case NODIRECTION: + case FD_NODIRECTION: log_warning("Instance port connection %s.%s is NODIRECTION; treating as IN\n", log_id(cell_type), log_signal(it->second)); /* FALL_THROUGH */ - case IN: + case FD_IN: source = secondName; sink = firstName; break; diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc index 44e4e5f9..ae903151 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc @@ -779,6 +779,19 @@ bool dump_cell_expr(std::ostream &f, std::string indent, RTLIL::Cell *cell) return true; } + if (cell->type == "$lut") + { + f << stringf("%s" "assign ", indent.c_str()); + dump_sigspec(f, cell->getPort("\\Y")); + f << stringf(" = "); + dump_const(f, cell->parameters.at("\\LUT")); + f << stringf(" >> "); + dump_attributes(f, "", cell->attributes, ' '); + dump_sigspec(f, cell->getPort("\\A")); + f << stringf(";\n"); + return true; + } + if (cell->type == "$dffsr") { SigSpec sig_clk = cell->getPort("\\CLK"); @@ -1510,7 +1523,7 @@ struct VerilogBackend : public Backend { log("\n"); log(" -nodec\n"); log(" 32-bit constant values are by default dumped as decimal numbers,\n"); - log(" not bit pattern. This option decativates this feature and instead\n"); + log(" not bit pattern. This option deactivates this feature and instead\n"); log(" will write out all constants in binary.\n"); log("\n"); log(" -decimal\n"); @@ -1518,13 +1531,13 @@ struct VerilogBackend : public Backend { log("\n"); log(" -nohex\n"); log(" constant values that are compatible with hex output are usually\n"); - log(" dumped as hex values. This option decativates this feature and\n"); + log(" dumped as hex values. This option deactivates this feature and\n"); log(" instead will write out all constants in binary.\n"); log("\n"); log(" -nostr\n"); log(" Parameters and attributes that are specified as strings in the\n"); log(" original input will be output as strings by this back-end. This\n"); - log(" decativates this feature and instead will write string constants\n"); + log(" deactivates this feature and instead will write string constants\n"); log(" as binary numbers.\n"); log("\n"); log(" -defparam\n"); diff --git a/debian/patches/0007-Disable-pretty-build.patch b/debian/patches/0007-Disable-pretty-build.patch index 1191bdfd..7a999a2c 100644 --- a/debian/patches/0007-Disable-pretty-build.patch +++ b/debian/patches/0007-Disable-pretty-build.patch @@ -7,7 +7,7 @@ Subject: Disable pretty build 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile -index b021cd4..d95e368 100644 +index c888b2c..ebefd2a 100644 --- a/Makefile +++ b/Makefile @@ -52,7 +52,7 @@ EXTRA_OBJS = diff --git a/debian/patches/0009-Some-spelling-errors-fixed.patch b/debian/patches/0009-Some-spelling-errors-fixed.patch index 163c21c2..05780d3b 100644 --- a/debian/patches/0009-Some-spelling-errors-fixed.patch +++ b/debian/patches/0009-Some-spelling-errors-fixed.patch @@ -11,10 +11,10 @@ Subject: Some spelling errors fixed 5 files changed, 5 insertions(+), 5 deletions(-) diff --git a/backends/verilog/verilog_backend.cc b/backends/verilog/verilog_backend.cc -index 44e4e5f..ea468ed 100644 +index ae90315..d53df2e 100644 --- a/backends/verilog/verilog_backend.cc +++ b/backends/verilog/verilog_backend.cc -@@ -1402,7 +1402,7 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module) +@@ -1415,7 +1415,7 @@ void dump_module(std::ostream &f, std::string indent, RTLIL::Module *module) } if (!module->processes.empty()) @@ -50,7 +50,7 @@ index 964875d..ae5cf09 100644 This makes some aspects of RTLIL more complex but enables Yosys to be used for coarse grain synthesis where the cells of the target architecture operate on diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex -index 8af8ccd..3452ccb 100644 +index fea2354..c530186 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -2859,7 +2859,7 @@ to a graphics file (usually SVG or PostScript). diff --git a/debian/patches/0010-Fix-reproducibility-of-PDF-documents-in-yosys-doc.patch b/debian/patches/0010-Fix-reproducibility-of-PDF-documents-in-yosys-doc.patch index 0eebf558..f5e4236c 100644 --- a/debian/patches/0010-Fix-reproducibility-of-PDF-documents-in-yosys-doc.patch +++ b/debian/patches/0010-Fix-reproducibility-of-PDF-documents-in-yosys-doc.patch @@ -11,10 +11,10 @@ Subject: Fix reproducibility of PDF documents in yosys-doc 5 files changed, 21 insertions(+), 8 deletions(-) diff --git a/Makefile b/Makefile -index d95e368..4719844 100644 +index ebefd2a..1fdb05f 100644 --- a/Makefile +++ b/Makefile -@@ -632,9 +632,9 @@ update-manual: $(TARGETS) $(EXTRA_TARGETS) +@@ -638,9 +638,9 @@ update-manual: $(TARGETS) $(EXTRA_TARGETS) cd manual && ../yosys -p 'help -write-tex-command-reference-manual' manual: $(TARGETS) $(EXTRA_TARGETS) diff --git a/debian/patches/0011-Do-not-show-g-build-flags-in-Version-string.patch b/debian/patches/0011-Do-not-show-g-build-flags-in-Version-string.patch index ece49fb1..ff3fff03 100644 --- a/debian/patches/0011-Do-not-show-g-build-flags-in-Version-string.patch +++ b/debian/patches/0011-Do-not-show-g-build-flags-in-Version-string.patch @@ -7,10 +7,10 @@ Subject: Do not show g++ build flags in Version string 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/Makefile b/Makefile -index 4719844..34ba839 100644 +index 1fdb05f..0fe949b 100644 --- a/Makefile +++ b/Makefile -@@ -498,8 +498,7 @@ libyosys.so: $(filter-out kernel/driver.o,$(OBJS)) +@@ -504,8 +504,7 @@ libyosys.so: $(filter-out kernel/driver.o,$(OBJS)) $(Q) mkdir -p $(dir $@) $(P) $(CXX) -o $@ -c $(CPPFLAGS) $(CXXFLAGS) $< @@ -20,7 +20,7 @@ index 4719844..34ba839 100644 kernel/version_$(GIT_REV).cc: $(YOSYS_SRC)/Makefile $(P) rm -f kernel/version_*.o kernel/version_*.d kernel/version_*.cc -@@ -513,8 +512,10 @@ CXXFLAGS_NOVERIFIC = $(CXXFLAGS) +@@ -519,8 +518,10 @@ CXXFLAGS_NOVERIFIC = $(CXXFLAGS) LDLIBS_NOVERIFIC = $(LDLIBS) endif diff --git a/debian/patches/01_gitrevision.patch b/debian/patches/01_gitrevision.patch index 89515890..4a519944 100644 --- a/debian/patches/01_gitrevision.patch +++ b/debian/patches/01_gitrevision.patch @@ -11,7 +11,7 @@ Forwarded: doesn't make sense upstream 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/Makefile b/Makefile -index 7698047..087ccb3 100644 +index 365b92e..3839e34 100644 --- a/Makefile +++ b/Makefile @@ -99,8 +99,8 @@ LDFLAGS += -rdynamic diff --git a/debian/patches/02_removeabc.patch b/debian/patches/02_removeabc.patch index 9a9f4dcc..a56f15ee 100644 --- a/debian/patches/02_removeabc.patch +++ b/debian/patches/02_removeabc.patch @@ -9,10 +9,10 @@ Forwarded: doesn't make sense upstream 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile b/Makefile -index 087ccb3..b021cd4 100644 +index 3839e34..c888b2c 100644 --- a/Makefile +++ b/Makefile -@@ -344,7 +344,7 @@ LDLIBS += -lpthread +@@ -350,7 +350,7 @@ LDLIBS += -lpthread endif else ifeq ($(ABCEXTERNAL),) diff --git a/debian/patches/kfreebsd-support.patch b/debian/patches/kfreebsd-support.patch index c9b9b3b1..d1ae9201 100644 --- a/debian/patches/kfreebsd-support.patch +++ b/debian/patches/kfreebsd-support.patch @@ -100,7 +100,7 @@ index 0b4905c..0f068a1 100644 #define cover(_id) do { \ static CoverData __d __attribute__((section("yosys_cover_list"), aligned(1), used)) = { __FILE__, __FUNCTION__, _id, __LINE__, 0 }; \ diff --git a/kernel/yosys.cc b/kernel/yosys.cc -index 264b1f6..91e9279 100644 +index ad03289..822cab9 100644 --- a/kernel/yosys.cc +++ b/kernel/yosys.cc @@ -77,7 +77,7 @@ std::vector<void*> memhasher_store; diff --git a/frontends/ast/genrtlil.cc b/frontends/ast/genrtlil.cc index 0f7e910f..c9345ff0 100644 --- a/frontends/ast/genrtlil.cc +++ b/frontends/ast/genrtlil.cc @@ -985,7 +985,8 @@ RTLIL::SigSpec AstNode::genRTLIL(int width_hint, bool sign_hint) use_const_chunk: if (children.size() != 0) { - log_assert(children[0]->type == AST_RANGE); + if (children[0]->type != AST_RANGE) + log_file_error(filename, linenum, "Single range expected.\n"); int source_width = id2ast->range_left - id2ast->range_right + 1; int source_offset = id2ast->range_right; if (!children[0]->range_valid) { diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc index 04c429f7..71eba547 100644 --- a/frontends/ast/simplify.cc +++ b/frontends/ast/simplify.cc @@ -1781,7 +1781,7 @@ skip_dynamic_range_lvalue_expansion:; if (GetSize(children) == 2) { AstNode *buf = children[1]->clone(); - while (buf->simplify(true, false, false, stage, width_hint, sign_hint, false)) { } + while (buf->simplify(true, false, false, stage, -1, false, false)) { } if (buf->type != AST_CONSTANT) log_file_error(filename, linenum, "Failed to evaluate system function `%s' with non-constant value.\n", str.c_str()); @@ -1836,7 +1836,7 @@ skip_dynamic_range_lvalue_expansion:; goto apply_newNode; } - if (str == "\\$stable" || str == "\\$rose" || str == "\\$fell") + if (str == "\\$stable" || str == "\\$rose" || str == "\\$fell" || str == "\\$changed") { if (GetSize(children) != 1) log_file_error(filename, linenum, "System function %s got %d arguments, expected 1.\n", @@ -1853,6 +1853,9 @@ skip_dynamic_range_lvalue_expansion:; if (str == "\\$stable") newNode = new AstNode(AST_EQ, past, present); + else if (str == "\\$changed") + newNode = new AstNode(AST_NE, past, present); + else if (str == "\\$rose") newNode = new AstNode(AST_LOGIC_AND, new AstNode(AST_LOGIC_NOT, past), present); diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc index 1dd6d7e2..dba3b0f0 100644 --- a/frontends/verific/verific.cc +++ b/frontends/verific/verific.cc @@ -64,6 +64,7 @@ YOSYS_NAMESPACE_BEGIN int verific_verbose; bool verific_import_pending; string verific_error_msg; +int verific_sva_fsm_limit; vector<string> verific_incdirs, verific_libdirs; @@ -117,6 +118,18 @@ RTLIL::SigBit VerificImporter::net_map_at(Net *net) return net_map.at(net); } +bool is_blackbox(Netlist *nl) +{ + if (nl->IsBlackBox()) + return true; + + const char *attr = nl->GetAttValue("blackbox"); + if (attr != nullptr && strcmp(attr, "0")) + return true; + + return false; +} + void VerificImporter::import_attributes(dict<RTLIL::IdString, RTLIL::Const> &attributes, DesignObj *obj) { MapIter mi; @@ -708,7 +721,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se netlist = nl; if (design->has(module_name)) { - if (!nl->IsOperator()) + if (!nl->IsOperator() && !is_blackbox(nl)) log_cmd_error("Re-definition of module `%s'.\n", nl->Owner()->Name()); return; } @@ -717,7 +730,7 @@ void VerificImporter::import_netlist(RTLIL::Design *design, Netlist *nl, std::se module->name = module_name; design->add(module); - if (nl->IsBlackBox()) { + if (is_blackbox(nl)) { log("Importing blackbox module %s.\n", RTLIL::id2cstr(module->name)); module->set_bool_attribute("\\blackbox"); } else { @@ -1618,6 +1631,8 @@ struct VerificExtNets void verific_import(Design *design, std::string top) { + verific_sva_fsm_limit = 16; + std::set<Netlist*> nl_todo, nl_done; { @@ -1673,6 +1688,7 @@ YOSYS_NAMESPACE_END PRIVATE_NAMESPACE_BEGIN +#ifdef YOSYS_ENABLE_VERIFIC bool check_noverific_env() { const char *e = getenv("YOSYS_NOVERIFIC"); @@ -1682,6 +1698,7 @@ bool check_noverific_env() return false; return true; } +#endif struct VerificPass : public Pass { VerificPass() : Pass("verific", "load Verilog and VHDL designs using Verific") { } @@ -1789,6 +1806,9 @@ struct VerificPass : public Pass { log(" -nosva\n"); log(" Ignore SVA properties, do not infer checker logic.\n"); log("\n"); + log(" -L <int>\n"); + log(" Maximum number of ctrl bits for SVA checker FSMs (default=16).\n"); + log("\n"); log(" -n\n"); log(" Keep all Verific names on instances and nets. By default only\n"); log(" user-declared names are preserved.\n"); @@ -1830,6 +1850,7 @@ struct VerificPass : public Pass { } verific_verbose = 0; + verific_sva_fsm_limit = 16; const char *release_str = Message::ReleaseString(); time_t release_time = Message::ReleaseDate(); @@ -2036,6 +2057,10 @@ struct VerificPass : public Pass { mode_nosva = true; continue; } + if (args[argidx] == "-L" && argidx+1 < GetSize(args)) { + verific_sva_fsm_limit = atoi(args[++argidx].c_str()); + continue; + } if (args[argidx] == "-n") { mode_names = true; continue; diff --git a/frontends/verific/verific.h b/frontends/verific/verific.h index cbd9314d..334a436a 100644 --- a/frontends/verific/verific.h +++ b/frontends/verific/verific.h @@ -101,6 +101,8 @@ void verific_import_sva_cover(VerificImporter *importer, Verific::Instance *inst void verific_import_sva_trigger(VerificImporter *importer, Verific::Instance *inst); bool verific_is_sva_net(VerificImporter *importer, Verific::Net *net); +extern int verific_sva_fsm_limit; + YOSYS_NAMESPACE_END #endif diff --git a/frontends/verific/verificsva.cc b/frontends/verific/verificsva.cc index 85b84218..cdc9ece8 100644 --- a/frontends/verific/verificsva.cc +++ b/frontends/verific/verificsva.cc @@ -466,13 +466,14 @@ struct SvaFsm dnode.ctrl.sort_and_unify(); - if (GetSize(dnode.ctrl) > 16) { + if (GetSize(dnode.ctrl) > verific_sva_fsm_limit) { if (verific_verbose >= 2) { log(" detected state explosion in DFSM generation:\n"); dump(); log(" ctrl signal: %s\n", log_signal(dnode.ctrl)); } - log_error("SVA DFSM state ctrl signal has %d (>16) bits. Stopping to prevent exponential design size explosion.\n", GetSize(dnode.ctrl)); + log_error("SVA DFSM state ctrl signal has %d (>%d) bits. Stopping to prevent exponential design size explosion.\n", + GetSize(dnode.ctrl), verific_sva_fsm_limit); } for (int i = 0; i < (1 << GetSize(dnode.ctrl)); i++) diff --git a/frontends/verilog/verilog_frontend.cc b/frontends/verilog/verilog_frontend.cc index 8dcc7c5a..aeea36a2 100644 --- a/frontends/verilog/verilog_frontend.cc +++ b/frontends/verilog/verilog_frontend.cc @@ -66,12 +66,21 @@ struct VerilogFrontend : public Frontend { log(" enable support for SystemVerilog assertions and some Yosys extensions\n"); log(" replace the implicit -D SYNTHESIS with -D FORMAL\n"); log("\n"); + log(" -noassert\n"); + log(" ignore assert() statements\n"); + log("\n"); + log(" -noassume\n"); + log(" ignore assume() statements\n"); + log("\n"); log(" -norestrict\n"); - log(" ignore restrict() assertions\n"); + log(" ignore restrict() statements\n"); log("\n"); log(" -assume-asserts\n"); log(" treat all assert() statements like assume() statements\n"); log("\n"); + log(" -assert-assumes\n"); + log(" treat all assume() statements like assert() statements\n"); + log("\n"); log(" -dump_ast1\n"); log(" dump abstract syntax tree (before simplification)\n"); log("\n"); @@ -229,6 +238,14 @@ struct VerilogFrontend : public Frontend { formal_mode = true; continue; } + if (arg == "-noassert") { + noassert_mode = true; + continue; + } + if (arg == "-noassume") { + noassume_mode = true; + continue; + } if (arg == "-norestrict") { norestrict_mode = true; continue; @@ -237,6 +254,10 @@ struct VerilogFrontend : public Frontend { assume_asserts_mode = true; continue; } + if (arg == "-assert-assumes") { + assert_assumes_mode = true; + continue; + } if (arg == "-dump_ast1") { flag_dump_ast1 = true; continue; diff --git a/frontends/verilog/verilog_frontend.h b/frontends/verilog/verilog_frontend.h index 16edc798..523bbc89 100644 --- a/frontends/verilog/verilog_frontend.h +++ b/frontends/verilog/verilog_frontend.h @@ -54,12 +54,21 @@ namespace VERILOG_FRONTEND // running in -formal mode extern bool formal_mode; + // running in -noassert mode + extern bool noassert_mode; + + // running in -noassume mode + extern bool noassume_mode; + // running in -norestrict mode extern bool norestrict_mode; // running in -assume-asserts mode extern bool assume_asserts_mode; + // running in -assert-assumes mode + extern bool assert_assumes_mode; + // running in -lib mode extern bool lib_mode; diff --git a/frontends/verilog/verilog_parser.y b/frontends/verilog/verilog_parser.y index 2389d7d3..16cac146 100644 --- a/frontends/verilog/verilog_parser.y +++ b/frontends/verilog/verilog_parser.y @@ -58,7 +58,8 @@ namespace VERILOG_FRONTEND { bool do_not_require_port_stubs; bool default_nettype_wire; bool sv_mode, formal_mode, lib_mode; - bool norestrict_mode, assume_asserts_mode; + bool noassert_mode, noassume_mode, norestrict_mode; + bool assume_asserts_mode, assert_assumes_mode; bool current_wire_rand, current_wire_const; std::istream *lexin; } @@ -881,9 +882,15 @@ param_decl_list: single_param_decl: TOK_ID '=' expr { - if (astbuf1 == nullptr) - frontend_verilog_yyerror("syntax error"); - AstNode *node = astbuf1->clone(); + AstNode *node; + if (astbuf1 == nullptr) { + if (!sv_mode) + frontend_verilog_yyerror("syntax error"); + node = new AstNode(AST_PARAMETER); + node->children.push_back(AstNode::mkconst_int(0, true)); + } else { + node = astbuf1->clone(); + } node->str = *$1; delete node->children[0]; node->children[0] = $3; @@ -1275,16 +1282,28 @@ opt_stmt_label: assert: opt_stmt_label TOK_ASSERT opt_property '(' expr ')' ';' { - ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5)); + if (noassert_mode) + delete $5; + else + ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_ASSUME : AST_ASSERT, $5)); } | opt_stmt_label TOK_ASSUME opt_property '(' expr ')' ';' { - ast_stack.back()->children.push_back(new AstNode(AST_ASSUME, $5)); + if (noassume_mode) + delete $5; + else + ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_ASSERT : AST_ASSUME, $5)); } | opt_stmt_label TOK_ASSERT opt_property '(' TOK_EVENTUALLY expr ')' ';' { - ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6)); + if (noassert_mode) + delete $6; + else + ast_stack.back()->children.push_back(new AstNode(assume_asserts_mode ? AST_FAIR : AST_LIVE, $6)); } | opt_stmt_label TOK_ASSUME opt_property '(' TOK_EVENTUALLY expr ')' ';' { - ast_stack.back()->children.push_back(new AstNode(AST_FAIR, $6)); + if (noassume_mode) + delete $6; + else + ast_stack.back()->children.push_back(new AstNode(assert_assumes_mode ? AST_LIVE : AST_FAIR, $6)); } | opt_stmt_label TOK_COVER opt_property '(' expr ')' ';' { ast_stack.back()->children.push_back(new AstNode(AST_COVER, $5)); diff --git a/kernel/celltypes.h b/kernel/celltypes.h index fcc4fcc4..6041168b 100644 --- a/kernel/celltypes.h +++ b/kernel/celltypes.h @@ -157,7 +157,7 @@ struct CellTypes IdString A = "\\A", B = "\\B", C = "\\C", D = "\\D"; IdString E = "\\E", F = "\\F", G = "\\G", H = "\\H"; IdString I = "\\I", J = "\\J", K = "\\K", L = "\\L"; - IdString M = "\\I", N = "\\N", O = "\\O", P = "\\P"; + IdString M = "\\M", N = "\\N", O = "\\O", P = "\\P"; IdString S = "\\S", T = "\\T", U = "\\U", V = "\\V"; IdString Y = "\\Y"; diff --git a/kernel/yosys.cc b/kernel/yosys.cc index 264b1f63..ad032899 100644 --- a/kernel/yosys.cc +++ b/kernel/yosys.cc @@ -166,7 +166,7 @@ std::string vstringf(const char *fmt, va_list ap) std::string string; char *str = NULL; -#ifdef _WIN32 +#if defined(_WIN32 )|| defined(__CYGWIN__) int sz = 64, rc; while (1) { va_list apc; diff --git a/manual/command-reference-manual.tex b/manual/command-reference-manual.tex index 8af8ccdd..fea2354e 100644 --- a/manual/command-reference-manual.tex +++ b/manual/command-reference-manual.tex @@ -4421,13 +4421,13 @@ Write the current design to a Verilog file. -nodec 32-bit constant values are by default dumped as decimal numbers, - not bit pattern. This option decativates this feature and instead + not bit pattern. This option deactivates this feature and instead will write out all constants in binary. -nostr Parameters and attributes that are specified as strings in the original input will be output as strings by this back-end. This - decativates this feature and instead will write string constants + deactivates this feature and instead will write string constants as binary numbers. -defparam diff --git a/misc/create_vcxsrc.sh b/misc/create_vcxsrc.sh index 215e27c5..924d2722 100644 --- a/misc/create_vcxsrc.sh +++ b/misc/create_vcxsrc.sh @@ -5,11 +5,11 @@ vcxsrc="$1-$2" yosysver="$2" gitsha="$3" -rm -rf YosysVS-Tpl-v1.zip YosysVS -wget http://www.clifford.at/yosys/nogit/YosysVS-Tpl-v1.zip +rm -rf YosysVS-Tpl-v2.zip YosysVS +wget http://www.clifford.at/yosys/nogit/YosysVS-Tpl-v2.zip -unzip YosysVS-Tpl-v1.zip -rm -f YosysVS-Tpl-v1.zip +unzip YosysVS-Tpl-v2.zip +rm -f YosysVS-Tpl-v2.zip mv YosysVS "$vcxsrc" { diff --git a/passes/cmds/setundef.cc b/passes/cmds/setundef.cc index 62d940ce..a1dfa9b5 100644 --- a/passes/cmds/setundef.cc +++ b/passes/cmds/setundef.cc @@ -162,7 +162,6 @@ struct SetundefPass : public Pass { continue; } if (args[argidx] == "-expose") { - got_value = true; expose_mode = true; continue; } @@ -212,6 +211,13 @@ struct SetundefPass : public Pass { } extra_args(args, argidx, design); + if (!got_value && expose_mode) { + log("Using default as -undef with -expose.\n"); + got_value = true; + worker.next_bit_mode = MODE_UNDEF; + worker.next_bit_state = 0; + } + if (expose_mode && !undriven_mode) log_cmd_error("Option -expose must be used with option -undriven.\n"); if (!got_value) diff --git a/passes/sat/sim.cc b/passes/sat/sim.cc index fadffcdb..53e248ad 100644 --- a/passes/sat/sim.cc +++ b/passes/sat/sim.cc @@ -778,7 +778,7 @@ struct SimPass : public Pass { log(" number of cycles to simulate (default: 20)\n"); log("\n"); log(" -a\n"); - log(" include all nets in VCD output, nut just those with public names\n"); + log(" include all nets in VCD output, not just those with public names\n"); log("\n"); log(" -w\n"); log(" writeback mode: use final simulation state as new init state\n"); diff --git a/techlibs/ecp5/dram.txt b/techlibs/ecp5/dram.txt index b3252fa9..b9435742 100644 --- a/techlibs/ecp5/dram.txt +++ b/techlibs/ecp5/dram.txt @@ -13,4 +13,5 @@ endbram match $__TRELLIS_DPR16X4 make_outreg + min wports 1 endmatch diff --git a/techlibs/ice40/cells_sim.v b/techlibs/ice40/cells_sim.v index 9f73aeb0..e0a07af3 100644 --- a/techlibs/ice40/cells_sim.v +++ b/techlibs/ice40/cells_sim.v @@ -920,19 +920,40 @@ parameter A_SIGNED = 1'b0; parameter B_SIGNED = 1'b0; endmodule -(* blackbox *) -module SB_SPRAM256KA( +module SB_SPRAM256KA ( input [13:0] ADDRESS, input [15:0] DATAIN, input [3:0] MASKWREN, - input WREN, - input CHIPSELECT, - input CLOCK, - input STANDBY, - input SLEEP, - input POWEROFF, - output [15:0] DATAOUT + input WREN, CHIPSELECT, CLOCK, STANDBY, SLEEP, POWEROFF, + output reg [15:0] DATAOUT ); +`ifndef BLACKBOX + reg [15:0] mem [0:16383]; + wire off = SLEEP || !POWEROFF; + integer i; + + always @(negedge POWEROFF) begin + for (i = 0; i <= 16383; i = i+1) + mem[i] = 'bx; + end + + always @(posedge CLOCK, posedge off) begin + if (off) begin + DATAOUT <= 0; + end else + if (CHIPSELECT && !STANDBY && !WREN) begin + DATAOUT <= mem[ADDRESS]; + end else begin + if (CHIPSELECT && !STANDBY && WREN) begin + if (MASKWREN[0]) mem[ADDRESS][ 3: 0] = DATAIN[ 3: 0]; + if (MASKWREN[1]) mem[ADDRESS][ 7: 4] = DATAIN[ 7: 4]; + if (MASKWREN[2]) mem[ADDRESS][11: 8] = DATAIN[11: 8]; + if (MASKWREN[3]) mem[ADDRESS][15:12] = DATAIN[15:12]; + end + DATAOUT <= 'bx; + end + end +`endif endmodule (* blackbox *) diff --git a/techlibs/xilinx/cells_xtra.sh b/techlibs/xilinx/cells_xtra.sh index c7ad1604..e7c7d17b 100644 --- a/techlibs/xilinx/cells_xtra.sh +++ b/techlibs/xilinx/cells_xtra.sh @@ -1,13 +1,13 @@ #!/bin/bash set -e -libdir="/opt/Xilinx/Vivado/2015.4/data/verilog/src" +libdir="/opt/Xilinx/Vivado/2018.1/data/verilog/src" function xtract_cell_decl() { for dir in $libdir/xeclib $libdir/retarget; do [ -f $dir/$1.v ] || continue - egrep '^\s*((end)?module|parameter|input|output|(end)?function|(end)?task)' $dir/$1.v | + egrep '^\s*((end)?module|parameter|input|inout|output|(end)?function|(end)?task)' $dir/$1.v | sed -re '/UNPLACED/ d; /^\s*function/,/endfunction/ d; /^\s*task/,/endtask/ d; s,//.*,,; s/#?\(.*/(...);/; s/^(input|output|parameter)/ \1/; s/\s+$//; s/,$/;/; /input|output|parameter/ s/[^;]$/&;/; s/\s+/ /g; diff --git a/techlibs/xilinx/cells_xtra.v b/techlibs/xilinx/cells_xtra.v index a2dd01ad..69e54233 100644 --- a/techlibs/xilinx/cells_xtra.v +++ b/techlibs/xilinx/cells_xtra.v @@ -2225,6 +2225,7 @@ module IOBUF (...); parameter IOSTANDARD = "DEFAULT"; parameter SLEW = "SLOW"; output O; + inout IO; input I, T; endmodule @@ -2236,6 +2237,7 @@ module IOBUF_DCIEN (...); parameter SLEW = "SLOW"; parameter USE_IBUFDISABLE = "TRUE"; output O; + inout IO; input DCITERMDISABLE; input I; input IBUFDISABLE; @@ -2250,6 +2252,7 @@ module IOBUF_INTERMDISABLE (...); parameter SLEW = "SLOW"; parameter USE_IBUFDISABLE = "TRUE"; output O; + inout IO; input I; input IBUFDISABLE; input INTERMDISABLE; @@ -2263,6 +2266,7 @@ module IOBUFDS (...); parameter IOSTANDARD = "DEFAULT"; parameter SLEW = "SLOW"; output O; + inout IO, IOB; input I, T; endmodule @@ -2275,6 +2279,8 @@ module IOBUFDS_DCIEN (...); parameter SLEW = "SLOW"; parameter USE_IBUFDISABLE = "TRUE"; output O; + inout IO; + inout IOB; input DCITERMDISABLE; input I; input IBUFDISABLE; @@ -2288,6 +2294,8 @@ module IOBUFDS_DIFF_OUT (...); parameter IOSTANDARD = "DEFAULT"; output O; output OB; + inout IO; + inout IOB; input I; input TM; input TS; @@ -2302,6 +2310,8 @@ module IOBUFDS_DIFF_OUT_DCIEN (...); parameter USE_IBUFDISABLE = "TRUE"; output O; output OB; + inout IO; + inout IOB; input DCITERMDISABLE; input I; input IBUFDISABLE; @@ -2318,6 +2328,8 @@ module IOBUFDS_DIFF_OUT_INTERMDISABLE (...); parameter USE_IBUFDISABLE = "TRUE"; output O; output OB; + inout IO; + inout IOB; input I; input IBUFDISABLE; input INTERMDISABLE; @@ -2381,6 +2393,7 @@ module ISERDESE2 (...); endmodule module KEEPER (...); + inout O; endmodule module LDCE (...); |