mirrors/yosys
3
0
Fork 0
mirror of https://github.com/YosysHQ/yosys synced 2025-04-08 02:15:20 +00:00
Code Activity

Merge https://github.com/cliffordwolf/yosys

Browse source
This commit is contained in:
dh73 2017-11-08 20:24:01 -06:00
parent 1fc061d90c 9ae25039fb
commit cf8cc50bf5
25 changed files with 605 additions and 466 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
.travis.yml
View file

@ -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

13
COPYING Normal file
View file

@ -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.

19
Makefile
View file

@ -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)

2
README.md
View file

@ -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

3
backends/smt2/smt2.cc
View file

@ -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);

3
backends/smt2/smtbmc.py
View file

@ -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)):

79
backends/smt2/smtio.py
View file

@ -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:

2
examples/osu035/Makefile
View file

@ -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:

2
examples/osu035/example.constr Normal file
View file

@ -0,0 +1,2 @@
set_driving_cell INVX1
set_load 0.015

2
examples/osu035/example.ys
View file

@ -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

21
frontends/ast/simplify.cc
View file

@ -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--;

7
frontends/verific/README
View file

@ -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
========================================================

441
frontends/verific/verific.cc
View file

@ -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,46 +1244,11 @@ VerificClockEdge::VerificClockEdge(VerificImporter *importer, Instance *inst)
clock_sig = importer->net_map_at(clock_net);
return;
}
// VHDL-flavored PSL clock
if (inst->Type() == PRIM_AND)
{
Net *w1 = inst->GetInput1();
Net *w2 = inst->GetInput2();
clock_net = verific_follow_inv_pslprev(w1);
if (clock_net == w2) {
clock_sig = importer->net_map_at(clock_net);
posedge = true;
return;
}
clock_net = verific_follow_inv_pslprev(w2);
if (clock_net == w1) {
clock_sig = importer->net_map_at(clock_net);
posedge = true;
return;
}
clock_net = verific_follow_pslprev(w1);
if (clock_net == verific_follow_inv(w2)) {
clock_sig = importer->net_map_at(clock_net);
posedge = false;
return;
}
clock_net = verific_follow_pslprev(w2);
if (clock_net == verific_follow_inv(w1)) {
clock_sig = importer->net_map_at(clock_net);
posedge = false;
return;
}
log_abort();
}
}
struct VerificSvaImporter
// ==================================================================
struct VerificSvaPP
{
VerificImporter *importer;
Module *module;
@ -1359,11 +1256,6 @@ struct VerificSvaImporter
Netlist *netlist;
Instance *root;
SigBit clock = State::Sx;
bool clock_posedge = false;
SigBit disable_iff = State::S0;
bool mode_assert = false;
bool mode_assume = false;
bool mode_cover = false;
@ -1381,8 +1273,128 @@ 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)
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;
}
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;
}
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());
}
}
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;
Module *module;
Netlist *netlist;
Instance *root;
SigBit clock = State::Sx;
bool clock_posedge = false;
SigBit disable_iff = State::S0;
bool mode_assert = false;
bool mode_assume = false;
bool mode_cover = false;
bool eventually = false;
Instance *net_to_ast_driver(Net *n)
{
if (n == nullptr)
return nullptr;
if (n->IsMultipleDriven())
return nullptr;
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)
@ -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();
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();
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();
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;
}

1
frontends/vhdl2verilog/Makefile.inc
View file

@ -1 +0,0 @@
OBJS += frontends/vhdl2verilog/vhdl2verilog.o

183
frontends/vhdl2verilog/vhdl2verilog.cc
View file

@ -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

16
kernel/driver.cc
View file

@ -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());

23
kernel/yosys.cc
View file

@ -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

1
passes/cmds/Makefile.inc
View file

@ -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

185
passes/cmds/ltp.cc Normal file
View file

@ -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

4
passes/cmds/show.cc
View file

@ -30,6 +30,10 @@
# include <readline/readline.h>
#endif
#ifdef YOSYS_ENABLE_EDITLINE
# include <editline/readline.h>
#endif
USING_YOSYS_NAMESPACE
PRIVATE_NAMESPACE_BEGIN

2
passes/opt/opt_clean.cc
View file

@ -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;

3
passes/opt/opt_rmdff.cc
View file

@ -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);

19
passes/techmap/abc.cc
View file

@ -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();
}

2
tests/sva/runtest.sh
View file

@ -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

34
tests/sva/vhdlpsl00.vhd
View file

@ -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;