aboutsummaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.travis.yml4
-rw-r--r--COPYING13
-rw-r--r--Makefile19
-rw-r--r--README.md2
-rw-r--r--backends/smt2/smt2.cc3
-rw-r--r--backends/smt2/smtbmc.py3
-rw-r--r--backends/smt2/smtio.py79
-rw-r--r--examples/osu035/Makefile2
-rw-r--r--examples/osu035/example.constr2
-rw-r--r--examples/osu035/example.ys2
-rw-r--r--frontends/ast/simplify.cc21
-rw-r--r--frontends/verific/README7
-rw-r--r--frontends/verific/verific.cc407
-rw-r--r--frontends/vhdl2verilog/Makefile.inc1
-rw-r--r--frontends/vhdl2verilog/vhdl2verilog.cc183
-rw-r--r--kernel/driver.cc16
-rw-r--r--kernel/yosys.cc23
-rw-r--r--passes/cmds/Makefile.inc1
-rw-r--r--passes/cmds/ltp.cc185
-rw-r--r--passes/cmds/show.cc4
-rw-r--r--passes/opt/opt_clean.cc2
-rw-r--r--passes/opt/opt_rmdff.cc3
-rw-r--r--passes/techmap/abc.cc19
-rw-r--r--tests/sva/runtest.sh2
-rw-r--r--tests/sva/vhdlpsl00.vhd34
25 files changed, 588 insertions, 449 deletions
diff --git a/.travis.yml b/.travis.yml
index d8cd5b298..1c08c21a8 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -29,8 +29,8 @@ before_install:
- (cd iverilog && autoconf && ./configure --prefix=$HOME/iverilog && make && make install)
- export PATH=$PATH:$HOME/iverilog/bin
compiler:
-# - clang
+# - clang
- gcc
os:
- linux
- - osx
+# - osx
diff --git a/COPYING b/COPYING
new file mode 100644
index 000000000..a01b7b697
--- /dev/null
+++ b/COPYING
@@ -0,0 +1,13 @@
+Copyright (C) 2012 - 2017 Clifford Wolf <clifford@clifford.at>
+
+Permission to use, copy, modify, and/or distribute this software for any
+purpose with or without fee is hereby granted, provided that the above
+copyright notice and this permission notice appear in all copies.
+
+THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
diff --git a/Makefile b/Makefile
index 393701019..924fd88b7 100644
--- a/Makefile
+++ b/Makefile
@@ -11,12 +11,14 @@ ENABLE_TCL := 1
ENABLE_ABC := 1
ENABLE_PLUGINS := 1
ENABLE_READLINE := 1
+ENABLE_EDITLINE := 0
ENABLE_VERIFIC := 0
ENABLE_COVER := 1
ENABLE_LIBYOSYS := 0
# other configuration flags
ENABLE_GPROF := 0
+ENABLE_DEBUG := 0
ENABLE_NDEBUG := 0
LINK_CURSES := 0
LINK_TERMCAP := 0
@@ -99,7 +101,7 @@ OBJS = kernel/version_$(GIT_REV).o
# 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 = 0fc1803a77c0
+ABCREV = f6838749f234
ABCPULL = 1
ABCURL ?= https://bitbucket.org/alanmi/abc
ABCMKARGS = CC="$(CXX)" CXX="$(CXX)" ABC_USE_LIBSTDCXX=1
@@ -225,6 +227,11 @@ endif
ifeq ($(CONFIG),mxe)
LDLIBS += -ltermcap
endif
+else
+ifeq ($(ENABLE_EDITLINE),1)
+CXXFLAGS += -DYOSYS_ENABLE_EDITLINE
+LDLIBS += -ledit -ltinfo -lbsd
+endif
endif
ifeq ($(ENABLE_PLUGINS),1)
@@ -251,7 +258,15 @@ LDFLAGS += -pg
endif
ifeq ($(ENABLE_NDEBUG),1)
-CXXFLAGS := -O3 -DNDEBUG $(filter-out -Os,$(CXXFLAGS))
+CXXFLAGS := -O3 -DNDEBUG $(filter-out -Os -ggdb,$(CXXFLAGS))
+endif
+
+ifeq ($(ENABLE_DEBUG),1)
+ifeq ($(CONFIG),clang)
+CXXFLAGS := -O0 $(filter-out -Os,$(CXXFLAGS))
+else
+CXXFLAGS := -Og $(filter-out -Os,$(CXXFLAGS))
+endif
endif
ifeq ($(ENABLE_ABC),1)
diff --git a/README.md b/README.md
index 514e32b35..92dc68a6a 100644
--- a/README.md
+++ b/README.md
@@ -1,7 +1,7 @@
```
yosys -- Yosys Open SYnthesis Suite
-Copyright (C) 2012 - 2016 Clifford Wolf <clifford@clifford.at>
+Copyright (C) 2012 - 2017 Clifford Wolf <clifford@clifford.at>
Permission to use, copy, modify, and/or distribute this software for any
purpose with or without fee is hereby granted, provided that the above
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index dce7c25de..8daa52eb3 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -811,6 +811,9 @@ struct Smt2Worker
Module *m = module->design->module(cell->type);
log_assert(m != nullptr);
+ hier.push_back(stringf(" (= (|%s_is| state) (|%s_is| %s))\n",
+ get_id(module), get_id(cell->type), cell_state.c_str()));
+
for (auto &conn : cell->connections())
{
Wire *w = m->wire(conn.first);
diff --git a/backends/smt2/smtbmc.py b/backends/smt2/smtbmc.py
index c8151c266..d9b79e26e 100644
--- a/backends/smt2/smtbmc.py
+++ b/backends/smt2/smtbmc.py
@@ -644,6 +644,9 @@ def write_vcd_trace(steps_start, steps_stop, index):
data = ["x"] * width
gotread = False
+ if len(wdata) == 0 and len(rdata) != 0:
+ wdata = [[]] * len(rdata)
+
assert len(rdata) == len(wdata)
for i in range(len(wdata)):
diff --git a/backends/smt2/smtio.py b/backends/smt2/smtio.py
index abf8e812d..61ac14c82 100644
--- a/backends/smt2/smtio.py
+++ b/backends/smt2/smtio.py
@@ -20,6 +20,8 @@ import sys, subprocess, re, os
from copy import deepcopy
from select import select
from time import time
+from queue import Queue, Empty
+from threading import Thread
hex_dict = {
@@ -126,7 +128,7 @@ class SmtIo:
if self.dummy_file is not None:
self.dummy_fd = open(self.dummy_file, "w")
if not self.noincr:
- self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+ self.p_open()
if self.unroll:
self.logic_uf = False
@@ -209,6 +211,57 @@ class SmtIo:
return stmt
+ def p_thread_main(self):
+ while True:
+ data = self.p.stdout.readline().decode("ascii")
+ if data == "": break
+ self.p_queue.put(data)
+ self.p_running = False
+
+ def p_open(self):
+ assert self.p is None
+ self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+ self.p_running = True
+ self.p_next = None
+ self.p_queue = Queue()
+ self.p_thread = Thread(target=self.p_thread_main)
+ self.p_thread.start()
+
+ def p_write(self, data, flush):
+ assert self.p is not None
+ self.p.stdin.write(bytes(data, "ascii"))
+ if flush: self.p.stdin.flush()
+
+ def p_read(self):
+ assert self.p is not None
+ assert self.p_running
+ if self.p_next is not None:
+ data = self.p_next
+ self.p_next = None
+ return data
+ return self.p_queue.get()
+
+ def p_poll(self):
+ assert self.p is not None
+ assert self.p_running
+ if self.p_next is not None:
+ return False
+ try:
+ self.p_next = self.p_queue.get(True, 0.1)
+ return False
+ except Empty:
+ return True
+
+ def p_close(self):
+ assert self.p is not None
+ self.p.stdin.close()
+ self.p_thread.join()
+ assert not self.p_running
+ self.p = None
+ self.p_next = None
+ self.p_queue = None
+ self.p_thread = None
+
def write(self, stmt, unroll=True):
if stmt.startswith(";"):
self.info(stmt)
@@ -281,20 +334,17 @@ class SmtIo:
if self.solver != "dummy":
if self.noincr:
if self.p is not None and not stmt.startswith("(get-"):
- self.p.stdin.close()
- self.p = None
+ self.p_close()
if stmt == "(push 1)":
self.smt2cache.append(list())
elif stmt == "(pop 1)":
self.smt2cache.pop()
else:
if self.p is not None:
- self.p.stdin.write(bytes(stmt + "\n", "ascii"))
- self.p.stdin.flush()
+ self.p_write(stmt + "\n", True)
self.smt2cache[-1].append(stmt)
else:
- self.p.stdin.write(bytes(stmt + "\n", "ascii"))
- self.p.stdin.flush()
+ self.p_write(stmt + "\n", True)
def info(self, stmt):
if not stmt.startswith("; yosys-smt2-"):
@@ -408,7 +458,7 @@ class SmtIo:
if self.solver == "dummy":
line = self.dummy_fd.readline().strip()
else:
- line = self.p.stdout.readline().decode("ascii").strip()
+ line = self.p_read().strip()
if self.dummy_file is not None:
self.dummy_fd.write(line + "\n")
@@ -441,15 +491,13 @@ class SmtIo:
if self.solver != "dummy":
if self.noincr:
if self.p is not None:
- self.p.stdin.close()
- self.p = None
- self.p = subprocess.Popen(self.popen_vargs, stdin=subprocess.PIPE, stdout=subprocess.PIPE, stderr=subprocess.STDOUT)
+ self.p_close()
+ self.p_open()
for cache_ctx in self.smt2cache:
for cache_stmt in cache_ctx:
- self.p.stdin.write(bytes(cache_stmt + "\n", "ascii"))
+ self.p_write(cache_stmt + "\n", False)
- self.p.stdin.write(bytes("(check-sat)\n", "ascii"))
- self.p.stdin.flush()
+ self.p_write("(check-sat)\n", True)
if self.timeinfo:
i = 0
@@ -457,7 +505,7 @@ class SmtIo:
count = 0
num_bs = 0
- while select([self.p.stdout], [], [], 0.1) == ([], [], []):
+ while self.p_poll():
count += 1
if count < 25:
@@ -672,6 +720,7 @@ class SmtIo:
def wait(self):
if self.p is not None:
self.p.wait()
+ self.p_close()
class SmtOpts:
diff --git a/examples/osu035/Makefile b/examples/osu035/Makefile
index 8d8e247e3..2bb8162b3 100644
--- a/examples/osu035/Makefile
+++ b/examples/osu035/Makefile
@@ -1,5 +1,5 @@
-example.edif: example.ys example.v osu035_stdcells.lib
+example.edif: example.ys example.v example.constr osu035_stdcells.lib
yosys -l example.yslog -q example.ys
osu035_stdcells.lib:
diff --git a/examples/osu035/example.constr b/examples/osu035/example.constr
new file mode 100644
index 000000000..eb2c6e8d5
--- /dev/null
+++ b/examples/osu035/example.constr
@@ -0,0 +1,2 @@
+set_driving_cell INVX1
+set_load 0.015
diff --git a/examples/osu035/example.ys b/examples/osu035/example.ys
index 040f776a6..6821ef426 100644
--- a/examples/osu035/example.ys
+++ b/examples/osu035/example.ys
@@ -4,7 +4,7 @@ read_liberty -lib osu035_stdcells.lib
synth -top top
dfflibmap -liberty osu035_stdcells.lib
-abc -liberty osu035_stdcells.lib
+abc -D 10000 -constr example.constr -liberty osu035_stdcells.lib
opt_clean
stat -liberty osu035_stdcells.lib
diff --git a/frontends/ast/simplify.cc b/frontends/ast/simplify.cc
index cd2120b8c..74e7b4675 100644
--- a/frontends/ast/simplify.cc
+++ b/frontends/ast/simplify.cc
@@ -405,9 +405,13 @@ bool AstNode::simplify(bool const_fold, bool at_zero, bool in_lvalue, int stage,
current_always_clocked = false;
if (type == AST_ALWAYS)
- for (auto child : children)
+ for (auto child : children) {
if (child->type == AST_POSEDGE || child->type == AST_NEGEDGE)
current_always_clocked = true;
+ if (child->type == AST_EDGE && GetSize(child->children) == 1 &&
+ child->children[0]->type == AST_IDENTIFIER && child->children[0]->str == "\\$global_clock")
+ current_always_clocked = true;
+ }
}
int backup_width_hint = width_hint;
@@ -1824,21 +1828,6 @@ skip_dynamic_range_lvalue_expansion:;
goto apply_newNode;
}
- if (str == "\\$rose" || str == "\\$fell")
- {
- if (GetSize(children) != 1)
- log_error("System function %s got %d arguments, expected 1 at %s:%d.\n",
- RTLIL::unescape_id(str).c_str(), int(children.size()), filename.c_str(), linenum);
-
- if (!current_always_clocked)
- log_error("System function %s is only allowed in clocked blocks at %s:%d.\n",
- RTLIL::unescape_id(str).c_str(), filename.c_str(), linenum);
-
- newNode = new AstNode(AST_EQ, children.at(0)->clone(), clone());
- newNode->children.at(1)->str = "\\$past";
- goto apply_newNode;
- }
-
// $anyconst and $anyseq are mapped in AstNode::genRTLIL()
if (str == "\\$anyconst" || str == "\\$anyseq") {
recursion_counter--;
diff --git a/frontends/verific/README b/frontends/verific/README
index e747255db..b4c436a3a 100644
--- a/frontends/verific/README
+++ b/frontends/verific/README
@@ -33,6 +33,13 @@ make -j8
./yosys -p 'verific -sv frontends/verific/example.sv; verific -import top'
+Verific Features that should be enabled in your Verific library
+===============================================================
+
+database/DBCompileFlags.h:
+ DB_PRESERVE_INITIAL_VALUE
+
+
Testing Verific+Yosys+SymbiYosys for formal verification
========================================================
diff --git a/frontends/verific/verific.cc b/frontends/verific/verific.cc
index ae39f7c9d..54210f98a 100644
--- a/frontends/verific/verific.cc
+++ b/frontends/verific/verific.cc
@@ -99,11 +99,14 @@ struct VerificImporter;
void import_sva_assert(VerificImporter *importer, Instance *inst);
void import_sva_assume(VerificImporter *importer, Instance *inst);
void import_sva_cover(VerificImporter *importer, Instance *inst);
+void svapp_assert(VerificImporter *importer, Instance *inst);
+void svapp_assume(VerificImporter *importer, Instance *inst);
+void svapp_cover(VerificImporter *importer, Instance *inst);
struct VerificClockEdge {
- Net *clock_net;
- SigBit clock_sig;
- bool posedge;
+ Net *clock_net = nullptr;
+ SigBit clock_sig = State::Sx;
+ bool posedge = false;
VerificClockEdge(VerificImporter *importer, Instance *inst);
};
@@ -115,14 +118,13 @@ struct VerificImporter
std::map<Net*, RTLIL::SigBit> net_map;
std::map<Net*, Net*> sva_posedge_map;
- bool mode_gates, mode_keep, mode_nosva, mode_names, verbose;
+ bool mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose;
pool<int> verific_sva_prims;
- pool<int> verific_psl_prims;
- VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_names, bool verbose) :
- mode_gates(mode_gates), mode_keep(mode_keep),
- mode_nosva(mode_nosva), mode_names(mode_names), verbose(verbose)
+ VerificImporter(bool mode_gates, bool mode_keep, bool mode_nosva, bool mode_nosvapp, bool mode_names, bool verbose) :
+ mode_gates(mode_gates), mode_keep(mode_keep), mode_nosva(mode_nosva),
+ mode_nosvapp(mode_nosvapp), mode_names(mode_names), verbose(verbose)
{
// Copy&paste from Verific 3.16_484_32_170630 Netlist.h
vector<int> sva_prims {
@@ -149,29 +151,6 @@ struct VerificImporter
for (int p : sva_prims)
verific_sva_prims.insert(p);
-
- // Copy&paste from Verific 3.16_484_32_170630 Netlist.h
- vector<int> psl_prims {
- OPER_PSLPREV, OPER_PSLNEXTFUNC, PRIM_PSL_ASSERT, PRIM_PSL_ASSUME,
- PRIM_PSL_ASSUME_GUARANTEE, PRIM_PSL_RESTRICT, PRIM_PSL_RESTRICT_GUARANTEE,
- PRIM_PSL_COVER, PRIM_ENDPOINT, PRIM_ROSE, PRIM_FELL, PRIM_AT, PRIM_ATSTRONG,
- PRIM_ABORT, PRIM_PSL_NOT, PRIM_PSL_AND, PRIM_PSL_OR, PRIM_IMPL, PRIM_EQUIV,
- PRIM_PSL_X, PRIM_PSL_XSTRONG, PRIM_PSL_G, PRIM_PSL_F, PRIM_PSL_U, PRIM_PSL_W,
- PRIM_NEXT, PRIM_NEXTSTRONG, PRIM_ALWAYS, PRIM_NEVER, PRIM_EVENTUALLY,
- PRIM_UNTIL, PRIM_UNTIL_, PRIM_UNTILSTRONG, PRIM_UNTILSTRONG_, PRIM_BEFORE,
- PRIM_BEFORE_, PRIM_BEFORESTRONG, PRIM_BEFORESTRONG_, PRIM_NEXT_A,
- PRIM_NEXT_ASTRONG, PRIM_NEXT_E, PRIM_NEXT_ESTRONG, PRIM_NEXT_EVENT,
- PRIM_NEXT_EVENTSTRONG, PRIM_NEXT_EVENT_A, PRIM_NEXT_EVENT_ASTRONG,
- PRIM_NEXT_EVENT_E, PRIM_NEXT_EVENT_ESTRONG, PRIM_SEQ_IMPL, PRIM_OSUFFIX_IMPL,
- PRIM_SUFFIX_IMPL, PRIM_OSUFFIX_IMPLSTRONG, PRIM_SUFFIX_IMPLSTRONG, PRIM_WITHIN,
- PRIM_WITHIN_, PRIM_WITHINSTRONG, PRIM_WITHINSTRONG_, PRIM_WHILENOT,
- PRIM_WHILENOT_, PRIM_WHILENOTSTRONG, PRIM_WHILENOTSTRONG_, PRIM_CONCAT,
- PRIM_FUSION, PRIM_SEQ_AND_LEN, PRIM_SEQ_AND, PRIM_SEQ_OR, PRIM_CONS_REP,
- PRIM_NONCONS_REP, PRIM_GOTO_REP
- };
-
- for (int p : psl_prims)
- verific_psl_prims.insert(p);
}
RTLIL::SigBit net_map_at(Net *net)
@@ -1123,20 +1102,20 @@ struct VerificImporter
if (!mode_gates) {
if (import_netlist_instance_cells(inst, inst_name))
continue;
- if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()) && !verific_psl_prims.count(inst->Type()))
+ if (inst->IsOperator() && !verific_sva_prims.count(inst->Type()))
log_warning("Unsupported Verific operator: %s (fallback to gate level implementation provided by verific)\n", inst->View()->Owner()->Name());
} else {
if (import_netlist_instance_gates(inst, inst_name))
continue;
}
- if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_PSL_ASSERT)
+ if (inst->Type() == PRIM_SVA_ASSERT)
sva_asserts.insert(inst);
- if (inst->Type() == PRIM_SVA_ASSUME || inst->Type() == PRIM_PSL_ASSUME)
+ if (inst->Type() == PRIM_SVA_ASSUME)
sva_assumes.insert(inst);
- if (inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_PSL_COVER)
+ if (inst->Type() == PRIM_SVA_COVER)
sva_covers.insert(inst);
if (inst->Type() == PRIM_SVA_PAST && !mode_nosva)
@@ -1156,38 +1135,9 @@ struct VerificImporter
continue;
}
- if (inst->Type() == OPER_PSLPREV && !mode_nosva)
- {
- Net *clock = inst->GetClock();
-
- if (!clock->IsConstant())
- {
- VerificClockEdge clock_edge(this, clock->Driver());
-
- SigSpec sig_d, sig_q;
-
- for (int i = 0; i < int(inst->InputSize()); i++) {
- sig_d.append(net_map_at(inst->GetInputBit(i)));
- sig_q.append(net_map_at(inst->GetOutputBit(i)));
- }
-
- if (verbose)
- log(" %sedge FF with D=%s, Q=%s, C=%s.\n", clock_edge.posedge ? "pos" : "neg",
- log_signal(sig_d), log_signal(sig_q), log_signal(clock_edge.clock_sig));
-
- RTLIL::Cell *ff = module->addDff(NEW_ID, clock_edge.clock_sig, sig_d, sig_q, clock_edge.posedge);
-
- if (inst->InputSize() == 1)
- past_ffs.insert(ff);
-
- if (!mode_keep)
- continue;
- }
- }
-
- if (!mode_keep && (verific_sva_prims.count(inst->Type()) || verific_psl_prims.count(inst->Type()))) {
+ if (!mode_keep && verific_sva_prims.count(inst->Type())) {
if (verbose)
- log(" skipping SVA/PSL cell in non k-mode\n");
+ log(" skipping SVA cell in non k-mode\n");
continue;
}
@@ -1199,7 +1149,7 @@ struct VerificImporter
if (!mode_keep)
log_error("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
- if (!verific_sva_prims.count(inst->Type()) && !verific_psl_prims.count(inst->Type()))
+ if (!verific_sva_prims.count(inst->Type()))
log_warning("Unsupported Verific primitive %s of type %s\n", inst->Name(), inst->View()->Owner()->Name());
}
@@ -1246,6 +1196,18 @@ struct VerificImporter
}
}
+ if (!mode_nosvapp)
+ {
+ for (auto inst : sva_asserts)
+ svapp_assert(this, inst);
+
+ for (auto inst : sva_assumes)
+ svapp_assume(this, inst);
+
+ for (auto inst : sva_covers)
+ svapp_cover(this, inst);
+ }
+
if (!mode_nosva)
{
for (auto inst : sva_asserts)
@@ -1262,36 +1224,6 @@ struct VerificImporter
}
};
-Net *verific_follow_inv(Net *w)
-{
- if (w == nullptr || w->IsMultipleDriven())
- return nullptr;
-
- Instance *i = w->Driver();
- if (i == nullptr || i->Type() != PRIM_INV)
- return nullptr;
-
- return i->GetInput();
-}
-
-Net *verific_follow_pslprev(Net *w)
-{
- if (w == nullptr || w->IsMultipleDriven())
- return nullptr;
-
- Instance *i = w->Driver();
- if (i == nullptr || i->Type() != OPER_PSLPREV || i->InputSize() != 1)
- return nullptr;
-
- return i->GetInputBit(0);
-}
-
-Net *verific_follow_inv_pslprev(Net *w)
-{
- w = verific_follow_inv(w);
- return verific_follow_pslprev(w);
-}
-
VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst)
{
log_assert(importer != nullptr);
@@ -1312,45 +1244,125 @@ VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst)
clock_sig = importer->net_map_at(clock_net);
return;
}
+}
+
+// ==================================================================
+
+struct VerificSvaPP
+{
+ VerificImporter *importer;
+ Module *module;
- // VHDL-flavored PSL clock
- if (inst->Type() == PRIM_AND)
+ Netlist *netlist;
+ Instance *root;
+
+ bool mode_assert = false;
+ bool mode_assume = false;
+ bool mode_cover = false;
+
+ Instance *net_to_ast_driver(Net *n)
{
- Net *w1 = inst->GetInput1();
- Net *w2 = inst->GetInput2();
+ if (n == nullptr)
+ return nullptr;
- clock_net = verific_follow_inv_pslprev(w1);
- if (clock_net == w2) {
- clock_sig = importer->net_map_at(clock_net);
- posedge = true;
- return;
- }
+ if (n->IsMultipleDriven())
+ return nullptr;
- clock_net = verific_follow_inv_pslprev(w2);
- if (clock_net == w1) {
- clock_sig = importer->net_map_at(clock_net);
- posedge = true;
- return;
+ Instance *inst = n->Driver();
+
+ if (inst == nullptr)
+ return nullptr;
+
+ if (!importer->verific_sva_prims.count(inst->Type()))
+ return nullptr;
+
+ if (inst->Type() == PRIM_SVA_PAST)
+ return nullptr;
+
+ return inst;
+ }
+
+ Instance *get_ast_input(Instance *inst) { return net_to_ast_driver(inst->GetInput()); }
+ Instance *get_ast_input1(Instance *inst) { return net_to_ast_driver(inst->GetInput1()); }
+ Instance *get_ast_input2(Instance *inst) { return net_to_ast_driver(inst->GetInput2()); }
+ Instance *get_ast_input3(Instance *inst) { return net_to_ast_driver(inst->GetInput3()); }
+ Instance *get_ast_control(Instance *inst) { return net_to_ast_driver(inst->GetControl()); }
+
+ Net *impl_to_seq(Instance *inst)
+ {
+ if (inst == nullptr)
+ return nullptr;
+
+ if (inst->Type() == PRIM_SVA_ASSERT || inst->Type() == PRIM_SVA_COVER || inst->Type() == PRIM_SVA_ASSUME) {
+ Net *new_net = impl_to_seq(get_ast_input(inst));
+ if (new_net) {
+ inst->Disconnect(inst->View()->GetInput());
+ inst->Connect(inst->View()->GetInput(), new_net);
+ }
+ return nullptr;
}
- clock_net = verific_follow_pslprev(w1);
- if (clock_net == verific_follow_inv(w2)) {
- clock_sig = importer->net_map_at(clock_net);
- posedge = false;
- return;
+ if (inst->Type() == PRIM_SVA_AT) {
+ Net *new_net = impl_to_seq(get_ast_input2(inst));
+ if (new_net) {
+ inst->Disconnect(inst->View()->GetInput2());
+ inst->Connect(inst->View()->GetInput2(), new_net);
+ }
+ return nullptr;
}
- clock_net = verific_follow_pslprev(w2);
- if (clock_net == verific_follow_inv(w1)) {
- clock_sig = importer->net_map_at(clock_net);
- posedge = false;
- return;
+ if (inst->Type() == PRIM_SVA_NON_OVERLAPPED_IMPLICATION)
+ {
+ if (mode_cover) {
+ Net *new_in1 = impl_to_seq(get_ast_input1(inst));
+ Net *new_in2 = impl_to_seq(get_ast_input2(inst));
+ if (!new_in1) new_in1 = inst->GetInput1();
+ if (!new_in2) new_in2 = inst->GetInput2();
+ return netlist->SvaBinary(PRIM_SVA_SEQ_CONCAT, new_in1, new_in2, inst->Linefile());
+ }
}
- log_abort();
+ return nullptr;
}
+
+ void run()
+ {
+ module = importer->module;
+ netlist = root->Owner();
+
+ // impl_to_seq(root);
+ }
+};
+
+void svapp_assert(VerificImporter *importer, Instance *inst)
+{
+ VerificSvaPP worker;
+ worker.importer = importer;
+ worker.root = inst;
+ worker.mode_assert = true;
+ worker.run();
+}
+
+void svapp_assume(VerificImporter *importer, Instance *inst)
+{
+ VerificSvaPP worker;
+ worker.importer = importer;
+ worker.root = inst;
+ worker.mode_assume = true;
+ worker.run();
}
+void svapp_cover(VerificImporter *importer, Instance *inst)
+{
+ VerificSvaPP worker;
+ worker.importer = importer;
+ worker.root = inst;
+ worker.mode_cover = true;
+ worker.run();
+}
+
+// ==================================================================
+
struct VerificSvaImporter
{
VerificImporter *importer;
@@ -1367,6 +1379,7 @@ struct VerificSvaImporter
bool mode_assert = false;
bool mode_assume = false;
bool mode_cover = false;
+ bool eventually = false;
Instance *net_to_ast_driver(Net *n)
{
@@ -1381,8 +1394,7 @@ struct VerificSvaImporter
if (inst == nullptr)
return nullptr;
- if (!importer->verific_sva_prims.count(inst->Type()) &&
- !importer->verific_psl_prims.count(inst->Type()))
+ if (!importer->verific_sva_prims.count(inst->Type()))
return nullptr;
if (inst->Type() == PRIM_SVA_PAST)
@@ -1491,31 +1503,6 @@ struct VerificSvaImporter
return;
}
- // PSL Primitives
-
- if (inst->Type() == PRIM_ALWAYS)
- {
- parse_sequence(seq, inst->GetInput());
- return;
- }
-
- if (inst->Type() == PRIM_IMPL)
- {
- parse_sequence(seq, inst->GetInput1());
- seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
- parse_sequence(seq, inst->GetInput2());
- return;
- }
-
- if (inst->Type() == PRIM_SUFFIX_IMPL)
- {
- parse_sequence(seq, inst->GetInput1());
- seq.sig_en = module->And(NEW_ID, seq.sig_en, seq.sig_a);
- sequence_ff(seq);
- parse_sequence(seq, inst->GetInput2());
- return;
- }
-
// Handle unsupported primitives
if (!importer->mode_keep)
@@ -1531,24 +1518,33 @@ struct VerificSvaImporter
// parse SVA property clock event
Instance *at_node = get_ast_input(root);
- log_assert(at_node && (at_node->Type() == PRIM_SVA_AT || at_node->Type() == PRIM_AT));
+ log_assert(at_node && at_node->Type() == PRIM_SVA_AT);
- VerificClockEdge clock_edge(importer, at_node->Type() == PRIM_SVA_AT ? get_ast_input1(at_node) : at_node->GetInput2()->Driver());
+ VerificClockEdge clock_edge(importer, get_ast_input1(at_node));
clock = clock_edge.clock_sig;
clock_posedge = clock_edge.posedge;
// parse disable_iff expression
- Net *sequence_net = at_node->Type() == PRIM_SVA_AT ? at_node->GetInput2() : at_node->GetInput1();
- Instance *sequence_node = net_to_ast_driver(sequence_net);
+ Net *sequence_net = at_node->GetInput2();
+
+ while (1)
+ {
+ Instance *sequence_node = net_to_ast_driver(sequence_net);
+
+ if (sequence_node && sequence_node->Type() == PRIM_SVA_S_EVENTUALLY) {
+ eventually = true;
+ sequence_net = sequence_node->GetInput();
+ continue;
+ }
- if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) {
- disable_iff = importer->net_map_at(sequence_node->GetInput1());
- sequence_net = sequence_node->GetInput2();
- } else
- if (sequence_node && sequence_node->Type() == PRIM_ABORT) {
- disable_iff = importer->net_map_at(sequence_node->GetInput2());
- sequence_net = sequence_node->GetInput1();
+ if (sequence_node && sequence_node->Type() == PRIM_SVA_DISABLE_IFF) {
+ disable_iff = importer->net_map_at(sequence_node->GetInput1());
+ sequence_net = sequence_node->GetInput2();
+ continue;
+ }
+
+ break;
}
// parse SVA sequence into trigger signal
@@ -1561,9 +1557,14 @@ struct VerificSvaImporter
RTLIL::IdString root_name = module->uniquify(importer->mode_names || root->IsUserDeclared() ? RTLIL::escape_id(root->Name()) : NEW_ID);
- if (mode_assert) module->addAssert(root_name, seq.sig_a, seq.sig_en);
- if (mode_assume) module->addAssume(root_name, seq.sig_a, seq.sig_en);
- if (mode_cover) module->addCover(root_name, seq.sig_a, seq.sig_en);
+ if (eventually) {
+ if (mode_assert) module->addLive(root_name, seq.sig_a, seq.sig_en);
+ if (mode_assume) module->addFair(root_name, seq.sig_a, seq.sig_en);
+ } else {
+ if (mode_assert) module->addAssert(root_name, seq.sig_a, seq.sig_en);
+ if (mode_assume) module->addAssume(root_name, seq.sig_a, seq.sig_en);
+ if (mode_cover) module->addCover(root_name, seq.sig_a, seq.sig_en);
+ }
}
};
@@ -1594,6 +1595,8 @@ void import_sva_cover(VerificImporter *importer, Instance *inst)
worker.run();
}
+// ==================================================================
+
struct VerificExtNets
{
int portname_cnt = 0;
@@ -1690,11 +1693,27 @@ struct VerificPass : public Pass {
log("Load the specified Verilog/SystemVerilog files into Verific.\n");
log("\n");
log("\n");
- log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl|-vhdpsl} <vhdl-file>..\n");
+ log(" verific {-vhdl87|-vhdl93|-vhdl2k|-vhdl2008|-vhdl} <vhdl-file>..\n");
log("\n");
log("Load the specified VHDL files into Verific.\n");
log("\n");
log("\n");
+ log(" verific -vlog-incdir <directory>..\n");
+ log("\n");
+ log("Add Verilog include directories.\n");
+ log("\n");
+ log("\n");
+ log(" verific -vlog-libdir <directory>..\n");
+ log("\n");
+ log("Add Verilog library directories. Verific will search in this directories to\n");
+ log("find undefined modules.\n");
+ log("\n");
+ log("\n");
+ log(" verific -vlog-define <macro>[=<value>]..\n");
+ log("\n");
+ log("Add Verilog defines. (The macros SYNTHESIS and VERIFIC are defined implicitly.)\n");
+ log("\n");
+ log("\n");
log(" verific -import [options] <top-module>..\n");
log("\n");
log("Elaborate the design for the specified top modules, import to Yosys and\n");
@@ -1715,10 +1734,6 @@ struct VerificPass : public Pass {
log(" -extnets\n");
log(" Resolve references to external nets by adding module ports as needed.\n");
log("\n");
- log(" -nosva\n");
- log(" Ignore SVA properties, do not infer checker logic. (This also disables\n");
- log(" PSL properties in -vhdpsl mode.)\n");
- log("\n");
log(" -v\n");
log(" Verbose log messages.\n");
log("\n");
@@ -1731,6 +1746,12 @@ struct VerificPass : public Pass {
log(" This will also add all SVA related cells to the design parallel to\n");
log(" the checker logic inferred by it.\n");
log("\n");
+ log(" -nosva\n");
+ log(" Ignore SVA properties, do not infer checker logic.\n");
+ log("\n");
+ log(" -nosvapp\n");
+ log(" Disable SVA properties pre-processing pass. This implies -nosva.\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");
@@ -1750,6 +1771,8 @@ struct VerificPass : public Pass {
Message::RegisterCallBackMsg(msg_func);
RuntimeFlags::SetVar("db_allow_external_nets", 1);
RuntimeFlags::SetVar("vhdl_ignore_assertion_statements", 0);
+ veri_file::DefineCmdLineMacro("VERIFIC");
+ veri_file::DefineCmdLineMacro("SYNTHESIS");
const char *release_str = Message::ReleaseString();
time_t release_time = Message::ReleaseDate();
@@ -1765,6 +1788,33 @@ struct VerificPass : public Pass {
int argidx = 1;
+ if (GetSize(args) > argidx && args[argidx] == "-vlog-incdir") {
+ for (argidx++; argidx < GetSize(args); argidx++)
+ veri_file::AddIncludeDir(args[argidx].c_str());
+ goto check_error;
+ }
+
+ if (GetSize(args) > argidx && args[argidx] == "-vlog-libdir") {
+ for (argidx++; argidx < GetSize(args); argidx++)
+ veri_file::AddYDir(args[argidx].c_str());
+ goto check_error;
+ }
+
+ if (GetSize(args) > argidx && args[argidx] == "-vlog-define") {
+ for (argidx++; argidx < GetSize(args); argidx++) {
+ string name = args[argidx];
+ size_t equal = name.find('=');
+ if (equal != std::string::npos) {
+ string value = name.substr(equal+1);
+ name = name.substr(0, equal);
+ veri_file::DefineCmdLineMacro(name.c_str(), value.c_str());
+ } else {
+ veri_file::DefineCmdLineMacro(name.c_str());
+ }
+ }
+ goto check_error;
+ }
+
if (GetSize(args) > argidx && args[argidx] == "-vlog95") {
for (argidx++; argidx < GetSize(args); argidx++)
if (!veri_file::Analyze(args[argidx].c_str(), veri_file::VERILOG_95))
@@ -1832,19 +1882,11 @@ struct VerificPass : public Pass {
goto check_error;
}
- if (GetSize(args) > argidx && args[argidx] == "-vhdpsl") {
- vhdl_file::SetDefaultLibraryPath((proc_share_dirname() + "verific/vhdl_vdbs_2008").c_str());
- for (argidx++; argidx < GetSize(args); argidx++)
- if (!vhdl_file::Analyze(args[argidx].c_str(), "work", vhdl_file::VHDL_PSL))
- log_cmd_error("Reading `%s' in VHDL_PSL mode failed.\n", args[argidx].c_str());
- goto check_error;
- }
-
if (GetSize(args) > argidx && args[argidx] == "-import")
{
std::set<Netlist*> nl_todo, nl_done;
bool mode_all = false, mode_gates = false, mode_keep = false;
- bool mode_nosva = false, mode_names = false;
+ bool mode_nosva = false, mode_nosvapp = false, mode_names = false;
bool verbose = false, flatten = false, extnets = false;
string dumpfile;
@@ -1873,6 +1915,11 @@ struct VerificPass : public Pass {
mode_nosva = true;
continue;
}
+ if (args[argidx] == "-nosvapp") {
+ mode_nosva = true;
+ mode_nosvapp = true;
+ continue;
+ }
if (args[argidx] == "-n") {
mode_names = true;
continue;
@@ -1968,13 +2015,15 @@ struct VerificPass : public Pass {
while (!nl_todo.empty()) {
Netlist *nl = *nl_todo.begin();
if (nl_done.count(nl) == 0) {
- VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_names, verbose);
+ VerificImporter importer(mode_gates, mode_keep, mode_nosva, mode_nosvapp, mode_names, verbose);
importer.import_netlist(design, nl, nl_todo);
}
nl_todo.erase(nl);
nl_done.insert(nl);
}
+ veri_file::Reset();
+ vhdl_file::Reset();
Libset::Reset();
goto check_error;
}
diff --git a/frontends/vhdl2verilog/Makefile.inc b/frontends/vhdl2verilog/Makefile.inc
deleted file mode 100644
index 003d89c4a..000000000
--- a/frontends/vhdl2verilog/Makefile.inc
+++ /dev/null
@@ -1 +0,0 @@
-OBJS += frontends/vhdl2verilog/vhdl2verilog.o
diff --git a/frontends/vhdl2verilog/vhdl2verilog.cc b/frontends/vhdl2verilog/vhdl2verilog.cc
deleted file mode 100644
index 6f9c0e3f5..000000000
--- a/frontends/vhdl2verilog/vhdl2verilog.cc
+++ /dev/null
@@ -1,183 +0,0 @@
-/*
- * yosys -- Yosys Open SYnthesis Suite
- *
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
- *
- * Permission to use, copy, modify, and/or distribute this software for any
- * purpose with or without fee is hereby granted, provided that the above
- * copyright notice and this permission notice appear in all copies.
- *
- * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
- * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
- * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
- * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
- * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
- * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
- * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
- *
- */
-
-#include "kernel/register.h"
-#include "kernel/sigtools.h"
-#include "kernel/log.h"
-#include <stdlib.h>
-#include <stdio.h>
-#include <string.h>
-#include <errno.h>
-#include <limits.h>
-
-#ifndef _WIN32
-# include <unistd.h>
-# include <dirent.h>
-#endif
-
-YOSYS_NAMESPACE_BEGIN
-
-struct Vhdl2verilogPass : public Pass {
- Vhdl2verilogPass() : Pass("vhdl2verilog", "importing VHDL designs using vhdl2verilog") { }
- virtual void help()
- {
- // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
- log("\n");
- log(" vhdl2verilog [options] <vhdl-file>..\n");
- log("\n");
- log("This command reads VHDL source files using the 'vhdl2verilog' tool and the\n");
- log("Yosys Verilog frontend.\n");
- log("\n");
- log(" -out <out_file>\n");
- log(" do not import the vhdl2verilog output. instead write it to the\n");
- log(" specified file.\n");
- log("\n");
- log(" -vhdl2verilog_dir <directory>\n");
- log(" do use the specified vhdl2verilog installation. this is the directory\n");
- log(" that contains the setup_env.sh file. when this option is not present,\n");
- log(" it is assumed that vhdl2verilog is in the PATH environment variable.\n");
- log("\n");
- log(" -top <top-entity-name>\n");
- log(" The name of the top entity. This option is mandatory.\n");
- log("\n");
- log("The following options are passed as-is to vhdl2verilog:\n");
- log("\n");
- log(" -arch <architecture_name>\n");
- log(" -unroll_generate\n");
- log(" -nogenericeval\n");
- log(" -nouniquify\n");
- log(" -oldparser\n");
- log(" -suppress <list>\n");
- log(" -quiet\n");
- log(" -nobanner\n");
- log(" -mapfile <file>\n");
- log("\n");
- log("vhdl2verilog can be obtained from:\n");
- log("http://www.edautils.com/vhdl2verilog.html\n");
- log("\n");
- }
- virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
- {
- log_header(design, "Executing VHDL2VERILOG (importing VHDL designs using vhdl2verilog).\n");
- log_push();
-
- std::string out_file, top_entity;
- std::string vhdl2verilog_dir;
- std::string extra_opts;
-
- size_t argidx;
- for (argidx = 1; argidx < args.size(); argidx++) {
- if (args[argidx] == "-out" && argidx+1 < args.size()) {
- out_file = args[++argidx];
- continue;
- }
- if (args[argidx] == "-top" && argidx+1 < args.size()) {
- top_entity = args[++argidx];
- continue;
- }
- if (args[argidx] == "-vhdl2verilog_dir" && argidx+1 < args.size()) {
- vhdl2verilog_dir = args[++argidx];
- continue;
- }
- if ((args[argidx] == "-arch" || args[argidx] == "-suppress" || args[argidx] == "-mapfile") && argidx+1 < args.size()) {
- if (args[argidx] == "-mapfile" && !args[argidx+1].empty() && args[argidx+1][0] != '/') {
- char pwd[PATH_MAX];
- if (!getcwd(pwd, sizeof(pwd))) {
- log_cmd_error("getcwd failed: %s", strerror(errno));
- log_abort();
- }
- args[argidx+1] = pwd + ("/" + args[argidx+1]);
- }
- extra_opts += std::string(" ") + args[argidx];
- extra_opts += std::string(" '") + args[++argidx] + std::string("'");
- continue;
- }
- if (args[argidx] == "-unroll_generate" || args[argidx] == "-nogenericeval" || args[argidx] == "-nouniquify" ||
- args[argidx] == "-oldparser" || args[argidx] == "-quiet" || args[argidx] == "-nobanner") {
- extra_opts += std::string(" ") + args[argidx];
- continue;
- }
- break;
- }
-
- if (argidx == args.size())
- cmd_error(args, argidx, "Missing filenames.");
- if (args[argidx].substr(0, 1) == "-")
- cmd_error(args, argidx, "Unknown option.");
- if (top_entity.empty())
- log_cmd_error("Missing -top option.\n");
-
- std::string tempdir_name = make_temp_dir("/tmp/yosys-vhdl2verilog-XXXXXX");
- log("Using temp directory %s.\n", tempdir_name.c_str());
-
- if (!out_file.empty() && out_file[0] != '/') {
- char pwd[PATH_MAX];
- if (!getcwd(pwd, sizeof(pwd))) {
- log_cmd_error("getcwd failed: %s", strerror(errno));
- log_abort();
- }
- out_file = pwd + ("/" + out_file);
- }
-
- FILE *f = fopen(stringf("%s/files.list", tempdir_name.c_str()).c_str(), "wt");
- while (argidx < args.size()) {
- std::string file = args[argidx++];
- if (file.empty())
- continue;
- if (file[0] != '/') {
- char pwd[PATH_MAX];
- if (!getcwd(pwd, sizeof(pwd))) {
- log_cmd_error("getcwd failed: %s", strerror(errno));
- log_abort();
- }
- file = pwd + ("/" + file);
- }
- fprintf(f, "%s\n", file.c_str());
- log("Adding '%s' to the file list.\n", file.c_str());
- }
- fclose(f);
-
- std::string command = "exec 2>&1; ";
- if (!vhdl2verilog_dir.empty())
- command += stringf("cd '%s'; . ./setup_env.sh; ", vhdl2verilog_dir.c_str());
- command += stringf("cd '%s'; vhdl2verilog -out '%s' -filelist files.list -top '%s'%s", tempdir_name.c_str(),
- out_file.empty() ? "vhdl2verilog_output.v" : out_file.c_str(), top_entity.c_str(), extra_opts.c_str());
-
- log("Running '%s'..\n", command.c_str());
-
- int ret = run_command(command, [](const std::string &line) { log("%s", line.c_str()); });
- if (ret != 0)
- log_error("Execution of command \"%s\" failed: return code %d.\n", command.c_str(), ret);
-
- if (out_file.empty()) {
- std::ifstream ff;
- ff.open(stringf("%s/vhdl2verilog_output.v", tempdir_name.c_str()).c_str());
- if (ff.fail())
- log_error("Can't open vhdl2verilog output file `vhdl2verilog_output.v'.\n");
- Frontend::frontend_call(design, &ff, stringf("%s/vhdl2verilog_output.v", tempdir_name.c_str()), "verilog");
- }
-
- log_header(design, "Removing temp directory `%s':\n", tempdir_name.c_str());
- remove_directory(tempdir_name);
- log_pop();
- }
-} Vhdl2verilogPass;
-
-YOSYS_NAMESPACE_END
-
diff --git a/kernel/driver.cc b/kernel/driver.cc
index 1fe61b499..c5e31d718 100644
--- a/kernel/driver.cc
+++ b/kernel/driver.cc
@@ -25,6 +25,10 @@
# include <readline/history.h>
#endif
+#ifdef YOSYS_ENABLE_EDITLINE
+# include <editline/readline.h>
+#endif
+
#include <stdio.h>
#include <string.h>
#include <limits.h>
@@ -119,27 +123,33 @@ const char *prompt()
#else /* EMSCRIPTEN */
-#ifdef YOSYS_ENABLE_READLINE
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
int yosys_history_offset = 0;
std::string yosys_history_file;
#endif
void yosys_atexit()
{
-#ifdef YOSYS_ENABLE_READLINE
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
if (!yosys_history_file.empty()) {
+#if defined(YOSYS_ENABLE_READLINE)
if (yosys_history_offset > 0) {
history_truncate_file(yosys_history_file.c_str(), 100);
append_history(where_history() - yosys_history_offset, yosys_history_file.c_str());
} else
write_history(yosys_history_file.c_str());
+#else
+ write_history(yosys_history_file.c_str());
+#endif
}
clear_history();
+#if defined(YOSYS_ENABLE_READLINE)
HIST_ENTRY **hist_list = history_list();
if (hist_list != NULL)
free(hist_list);
#endif
+#endif
}
int main(int argc, char **argv)
@@ -159,7 +169,7 @@ int main(int argc, char **argv)
bool mode_v = false;
bool mode_q = false;
-#ifdef YOSYS_ENABLE_READLINE
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
if (getenv("HOME") != NULL) {
yosys_history_file = stringf("%s/.yosys_history", getenv("HOME"));
read_history(yosys_history_file.c_str());
diff --git a/kernel/yosys.cc b/kernel/yosys.cc
index e5b22eba7..34665a0ad 100644
--- a/kernel/yosys.cc
+++ b/kernel/yosys.cc
@@ -25,6 +25,10 @@
# include <readline/history.h>
#endif
+#ifdef YOSYS_ENABLE_EDITLINE
+# include <editline/readline.h>
+#endif
+
#ifdef YOSYS_ENABLE_PLUGINS
# include <dlfcn.h>
#endif
@@ -938,7 +942,7 @@ void run_backend(std::string filename, std::string command, RTLIL::Design *desig
Backend::backend_call(design, NULL, filename, command);
}
-#ifdef YOSYS_ENABLE_READLINE
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
static char *readline_cmd_generator(const char *text, int state)
{
static std::map<std::string, Pass*>::iterator it;
@@ -1025,14 +1029,14 @@ void shell(RTLIL::Design *design)
recursion_counter++;
log_cmd_error_throw = true;
-#ifdef YOSYS_ENABLE_READLINE
- rl_readline_name = "yosys";
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
+ rl_readline_name = (char*)"yosys";
rl_attempted_completion_function = readline_completion;
- rl_basic_word_break_characters = " \t\n";
+ rl_basic_word_break_characters = (char*)" \t\n";
#endif
char *command = NULL;
-#ifdef YOSYS_ENABLE_READLINE
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
while ((command = readline(create_prompt(design, recursion_counter))) != NULL)
{
#else
@@ -1046,7 +1050,7 @@ void shell(RTLIL::Design *design)
#endif
if (command[strspn(command, " \t\r\n")] == 0)
continue;
-#ifdef YOSYS_ENABLE_READLINE
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
add_history(command);
#endif
@@ -1114,7 +1118,7 @@ struct ShellPass : public Pass {
}
} ShellPass;
-#ifdef YOSYS_ENABLE_READLINE
+#if defined(YOSYS_ENABLE_READLINE) || defined(YOSYS_ENABLE_EDITLINE)
struct HistoryPass : public Pass {
HistoryPass() : Pass("history", "show last interactive commands") { }
virtual void help() {
@@ -1128,8 +1132,13 @@ struct HistoryPass : public Pass {
}
virtual void execute(std::vector<std::string> args, RTLIL::Design *design) {
extra_args(args, 1, design, false);
+#ifdef YOSYS_ENABLE_READLINE
for(HIST_ENTRY **list = history_list(); *list != NULL; list++)
log("%s\n", (*list)->line);
+#else
+ for (int i = where_history(); history_get(i); i++)
+ log("%s\n", history_get(i)->line);
+#endif
}
} HistoryPass;
#endif
diff --git a/passes/cmds/Makefile.inc b/passes/cmds/Makefile.inc
index 9e3934e16..44a83b2b9 100644
--- a/passes/cmds/Makefile.inc
+++ b/passes/cmds/Makefile.inc
@@ -28,4 +28,5 @@ OBJS += passes/cmds/edgetypes.o
OBJS += passes/cmds/chformal.o
OBJS += passes/cmds/chtype.o
OBJS += passes/cmds/blackbox.o
+OBJS += passes/cmds/ltp.o
diff --git a/passes/cmds/ltp.cc b/passes/cmds/ltp.cc
new file mode 100644
index 000000000..42dc794ec
--- /dev/null
+++ b/passes/cmds/ltp.cc
@@ -0,0 +1,185 @@
+/*
+ * yosys -- Yosys Open SYnthesis Suite
+ *
+ * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ *
+ * Permission to use, copy, modify, and/or distribute this software for any
+ * purpose with or without fee is hereby granted, provided that the above
+ * copyright notice and this permission notice appear in all copies.
+ *
+ * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
+ * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
+ * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR
+ * ANY SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
+ * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
+ * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF
+ * OR IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
+ *
+ */
+
+#include "kernel/yosys.h"
+#include "kernel/celltypes.h"
+#include "kernel/sigtools.h"
+
+USING_YOSYS_NAMESPACE
+PRIVATE_NAMESPACE_BEGIN
+
+struct LtpWorker
+{
+ RTLIL::Design *design;
+ RTLIL::Module *module;
+ SigMap sigmap;
+
+ dict<SigBit, tuple<int, SigBit, Cell*>> bits;
+ dict<SigBit, dict<SigBit, Cell*>> bit2bits;
+ dict<SigBit, tuple<SigBit, Cell*>> bit2ff;
+
+ int maxlvl;
+ SigBit maxbit;
+ pool<SigBit> busy;
+
+ LtpWorker(RTLIL::Module *module, bool noff) : design(module->design), module(module), sigmap(module)
+ {
+ CellTypes ff_celltypes;
+
+ if (noff) {
+ ff_celltypes.setup_internals_mem();
+ ff_celltypes.setup_stdcells_mem();
+ }
+
+ for (auto wire : module->selected_wires())
+ for (auto bit : sigmap(wire))
+ bits[bit] = tuple<int, SigBit, Cell*>(-1, State::Sx, nullptr);
+
+ for (auto cell : module->selected_cells())
+ {
+ pool<SigBit> src_bits, dst_bits;
+
+ for (auto &conn : cell->connections())
+ for (auto bit : sigmap(conn.second)) {
+ if (cell->input(conn.first))
+ src_bits.insert(bit);
+ if (cell->output(conn.first))
+ dst_bits.insert(bit);
+ }
+
+ if (noff && ff_celltypes.cell_known(cell->type)) {
+ for (auto s : src_bits)
+ for (auto d : dst_bits) {
+ bit2ff[s] = tuple<SigBit, Cell*>(d, cell);
+ break;
+ }
+ continue;
+ }
+
+ for (auto s : src_bits)
+ for (auto d : dst_bits)
+ bit2bits[s][d] = cell;
+ }
+
+ maxlvl = -1;
+ maxbit = State::Sx;
+ }
+
+ void runner(SigBit bit, int level, SigBit from, Cell *via)
+ {
+ auto &bitinfo = bits.at(bit);
+
+ if (get<0>(bitinfo) >= level)
+ return;
+
+ if (busy.count(bit) > 0) {
+ log_warning("Detected loop at %s in %s\n", log_signal(bit), log_id(module));
+ return;
+ }
+
+ busy.insert(bit);
+ get<0>(bitinfo) = level;
+ get<1>(bitinfo) = from;
+ get<2>(bitinfo) = via;
+
+ if (level > maxlvl) {
+ maxlvl = level;
+ maxbit = bit;
+ }
+
+ if (bit2bits.count(bit)) {
+ for (auto &it : bit2bits.at(bit))
+ runner(it.first, level+1, bit, it.second);
+ }
+
+ busy.erase(bit);
+ }
+
+ void printpath(SigBit bit)
+ {
+ auto &bitinfo = bits.at(bit);
+ if (get<2>(bitinfo)) {
+ printpath(get<1>(bitinfo));
+ log("%5d: %s (via %s)\n", get<0>(bitinfo), log_signal(bit), log_id(get<2>(bitinfo)));
+ } else {
+ log("%5d: %s\n", get<0>(bitinfo), log_signal(bit));
+ }
+ }
+
+ void run()
+ {
+ for (auto &it : bits)
+ if (get<0>(it.second) < 0)
+ runner(it.first, 0, State::Sx, nullptr);
+
+ log("\n");
+ log("Longest topological path in %s (length=%d):\n", log_id(module), maxlvl);
+
+ if (maxlvl >= 0)
+ printpath(maxbit);
+
+ if (bit2ff.count(maxbit))
+ log("%5s: %s (via %s)\n", "ff", log_signal(get<0>(bit2ff.at(maxbit))), log_id(get<1>(bit2ff.at(maxbit))));
+ }
+};
+
+struct LtpPass : public Pass {
+ LtpPass() : Pass("ltp", "print longest topological path") { }
+ virtual void help()
+ {
+ // |---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|---v---|
+ log("\n");
+ log(" ltp [options] [selection]\n");
+ log("\n");
+ log("This command prints the longest topological path in the design. (Only considers\n");
+ log("paths within a single module, so the design must be flattened.)\n");
+ log("\n");
+ log(" -noff\n");
+ log(" automatically exclude FF cell types\n");
+ log("\n");
+ }
+ virtual void execute(std::vector<std::string> args, RTLIL::Design *design)
+ {
+ bool noff = false;
+
+ log_header(design, "Executing LTP pass (find longest path).\n");
+
+ size_t argidx;
+ for (argidx = 1; argidx < args.size(); argidx++) {
+ if (args[argidx] == "-noff") {
+ noff = true;
+ continue;
+ }
+ break;
+ }
+
+ extra_args(args, argidx, design);
+
+ for (Module *module : design->selected_modules())
+ {
+ if (module->has_processes_warn())
+ continue;
+
+ LtpWorker worker(module, noff);
+ worker.run();
+ }
+ }
+} LtpPass;
+
+PRIVATE_NAMESPACE_END
diff --git a/passes/cmds/show.cc b/passes/cmds/show.cc
index 3a3939a81..02624cf30 100644
--- a/passes/cmds/show.cc
+++ b/passes/cmds/show.cc
@@ -30,6 +30,10 @@
# include <readline/readline.h>
#endif
+#ifdef YOSYS_ENABLE_EDITLINE
+# include <editline/readline.h>
+#endif
+
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN
diff --git a/passes/opt/opt_clean.cc b/passes/opt/opt_clean.cc
index fb1851868..2d2ffa9a1 100644
--- a/passes/opt/opt_clean.cc
+++ b/passes/opt/opt_clean.cc
@@ -392,7 +392,7 @@ bool rmunused_module_init(RTLIL::Module *module, bool purge_mode, bool verbose)
}
if (verbose)
- log(" removing redundent init attribute on %s.\n", log_id(wire));
+ log(" removing redundant init attribute on %s.\n", log_id(wire));
wire->attributes.erase("\\init");
did_something = true;
diff --git a/passes/opt/opt_rmdff.cc b/passes/opt/opt_rmdff.cc
index 02f3e93f5..edec42c4d 100644
--- a/passes/opt/opt_rmdff.cc
+++ b/passes/opt/opt_rmdff.cc
@@ -430,6 +430,8 @@ struct OptRmdffPass : public Pass {
assign_map.set(module);
dff_init_map.set(module);
+ mux_drivers.clear();
+ init_attributes.clear();
for (auto wire : module->wires())
{
@@ -534,6 +536,7 @@ struct OptRmdffPass : public Pass {
assign_map.clear();
mux_drivers.clear();
+ init_attributes.clear();
if (total_count || total_initdrv)
design->scratchpad_set_bool("opt.did_something", true);
diff --git a/passes/techmap/abc.cc b/passes/techmap/abc.cc
index 3d943e682..be86f642a 100644
--- a/passes/techmap/abc.cc
+++ b/passes/techmap/abc.cc
@@ -111,6 +111,7 @@ bool recover_init;
bool clk_polarity, en_polarity;
RTLIL::SigSpec clk_sig, en_sig;
+dict<int, std::string> pi_map, po_map;
int map_signal(RTLIL::SigBit bit, gate_type_t gate_type = G(NONE), int in1 = -1, int in2 = -1, int in3 = -1, int in4 = -1)
{
@@ -601,6 +602,14 @@ struct abc_output_filter
void next_line(const std::string &line)
{
+ int pi, po;
+ if (sscanf(line.c_str(), "Start-point = pi%d. End-point = po%d.", &pi, &po) == 2) {
+ log("ABC: Start-point = pi%d (%s). End-point = po%d (%s).\n",
+ pi, pi_map.count(pi) ? pi_map.at(pi).c_str() : "???",
+ po, po_map.count(po) ? po_map.at(po).c_str() : "???");
+ return;
+ }
+
for (char ch : line)
next_char(ch);
}
@@ -616,6 +625,8 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
signal_map.clear();
signal_list.clear();
+ pi_map.clear();
+ po_map.clear();
recover_init = false;
if (clk_str != "$")
@@ -768,7 +779,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
if (!si.is_port || si.type != G(NONE))
continue;
fprintf(f, " n%d", si.id);
- count_input++;
+ pi_map[count_input++] = log_signal(si.bit);
}
if (count_input == 0)
fprintf(f, " dummy_input\n");
@@ -780,7 +791,7 @@ void abc_module(RTLIL::Design *design, RTLIL::Module *current_module, std::strin
if (!si.is_port || si.type == G(NONE))
continue;
fprintf(f, " n%d", si.id);
- count_output++;
+ po_map[count_output++] = log_signal(si.bit);
}
fprintf(f, "\n");
@@ -1392,6 +1403,8 @@ struct AbcPass : public Pass {
signal_list.clear();
signal_map.clear();
signal_init.clear();
+ pi_map.clear();
+ po_map.clear();
#ifdef ABCEXTERNAL
std::string exe_file = ABCEXTERNAL;
@@ -1819,6 +1832,8 @@ struct AbcPass : public Pass {
signal_list.clear();
signal_map.clear();
signal_init.clear();
+ pi_map.clear();
+ po_map.clear();
log_pop();
}
diff --git a/tests/sva/runtest.sh b/tests/sva/runtest.sh
index 35c95a3e0..4c8e16542 100644
--- a/tests/sva/runtest.sh
+++ b/tests/sva/runtest.sh
@@ -29,7 +29,7 @@ generate_sby() {
fi
if [ -f $prefix.vhd ]; then
- echo "verific -vhdpsl $prefix.vhd"
+ echo "verific -vhdl $prefix.vhd"
fi
cat <<- EOT
diff --git a/tests/sva/vhdlpsl00.vhd b/tests/sva/vhdlpsl00.vhd
deleted file mode 100644
index 6d765d5a9..000000000
--- a/tests/sva/vhdlpsl00.vhd
+++ /dev/null
@@ -1,34 +0,0 @@
-library ieee;
-use ieee.std_logic_1164.all;
-use ieee.std_logic_unsigned.all;
-use ieee.numeric_std.all;
-
-entity top is
- port (
- clk : in std_logic;
- rst : in std_logic;
- up : in std_logic;
- down : in std_logic;
- cnt : buffer std_logic_vector(7 downto 0)
- );
-end entity;
-
-architecture rtl of top is
-begin
- process (clk) begin
- if rising_edge(clk) then
- if rst = '1' then
- cnt <= std_logic_vector(to_unsigned(0, 8));
- elsif up = '1' then
- cnt <= cnt + std_logic_vector(to_unsigned(1, 8));
- elsif down = '1' then
- cnt <= cnt - std_logic_vector(to_unsigned(1, 8));
- end if;
- end if;
- end process;
-
- -- PSL default clock is (rising_edge(clk));
- -- PSL assume always ( down -> not up );
- -- PSL assert always ( up |=> (cnt = prev(cnt) + std_logic_vector(to_unsigned(1, 8))) ) abort rst = '1';
- -- PSL assert always ( down |=> (cnt = prev(cnt) - std_logic_vector(to_unsigned(1, 8))) ) abort rst = '1';
-end architecture;
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-07 19:57:35 +0000