summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--.github/issue_template.md2
-rw-r--r--CHANGELOG110
-rw-r--r--Makefile9
-rw-r--r--README.md4
-rw-r--r--backends/edif/edif.cc39
-rw-r--r--backends/firrtl/firrtl.cc22
-rw-r--r--backends/verilog/verilog_backend.cc19
-rw-r--r--frontends/ast/genrtlil.cc3
-rw-r--r--frontends/ast/simplify.cc7
-rw-r--r--frontends/verific/verific.cc29
-rw-r--r--frontends/verific/verific.h2
-rw-r--r--frontends/verific/verificsva.cc5
-rw-r--r--frontends/verilog/verilog_frontend.cc23
-rw-r--r--frontends/verilog/verilog_frontend.h9
-rw-r--r--frontends/verilog/verilog_parser.y35
-rw-r--r--kernel/celltypes.h2
-rw-r--r--kernel/yosys.cc2
-rw-r--r--manual/command-reference-manual.tex4
-rw-r--r--misc/create_vcxsrc.sh8
-rw-r--r--passes/cmds/setundef.cc8
-rw-r--r--passes/sat/sim.cc2
-rw-r--r--techlibs/ecp5/dram.txt1
-rw-r--r--techlibs/ice40/cells_sim.v39
-rw-r--r--techlibs/xilinx/cells_xtra.sh4
-rw-r--r--techlibs/xilinx/cells_xtra.v13
25 files changed, 337 insertions, 64 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
diff --git a/CHANGELOG b/CHANGELOG
index 01c78ab3..5499c309 100644
--- a/CHANGELOG
+++ b/CHANGELOG
@@ -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
diff --git a/Makefile b/Makefile
index 7698047e..365b92ea 100644
--- a/Makefile
+++ b/Makefile
@@ -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
diff --git a/README.md b/README.md
index 424d9bbf..41ae4ac1 100644
--- a/README.md
+++ b/README.md
@@ -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/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 (...);