Skip to content
Permalink

Comparing changes

Choose two branches to see what’s changed or to start a new pull request. If you need to, you can also or learn more about diff comparisons.

Open a pull request

Create a new pull request by comparing changes across two branches. If you need to, you can also . Learn more about diff comparisons here.
base repository: azonenberg/yosys
Failed to load repositories. Confirm that selected base ref is valid, then try again.
Loading
base: 0d7e71f7abd4
Choose a base ref
...
head repository: azonenberg/yosys
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: 203b521a781c
Choose a head ref

Commits on Jan 31, 2017

  1. use Homebrew only if installed

    stv0g committed Jan 31, 2017
    Copy the full SHA
    44b47b5 View commit details

Commits on Feb 7, 2017

  1. Copy the full SHA
    19f3627 View commit details
  2. Copy the full SHA
    7e08e37 View commit details
  3. Copy the full SHA
    b8d5319 View commit details

Commits on Feb 9, 2017

  1. Copy the full SHA
    2ca8d48 View commit details
  2. Copy the full SHA
    8480620 View commit details
  3. Copy the full SHA
    e6cc67b View commit details
  4. Copy the full SHA
    94c76f8 View commit details
  5. Remove space after backslash

    stv0g committed Feb 9, 2017
    Copy the full SHA
    a3f19f0 View commit details

Commits on Feb 10, 2017

  1. Copy the full SHA
    9eca367 View commit details
  2. Use pkg-config for linking tcl-tk

    Both MacPorts and Homebrew have a pkg-config file for TCL. So lets use it.
    stv0g committed Feb 10, 2017
    Copy the full SHA
    422ffd5 View commit details
  3. Fix issue YosysHQ#306, "Bug in opt -full"

    Add check for whether the high bit in the constant expression is greater
    than the width of the variable, and optimizes that to a constant 1 or
    0
    C-Elegans committed Feb 10, 2017
    Copy the full SHA
    94b2720 View commit details

Commits on Feb 11, 2017

  1. Merge pull request YosysHQ#308 from C-Elegans/opt_compare_fix_pr

    Fix issue YosysHQ#306, "Bug in opt -full"
    cliffordwolf authored Feb 11, 2017
    Copy the full SHA
    9c1a7be View commit details
  2. Copy the full SHA
    a5bfeb9 View commit details
  3. Copy the full SHA
    a88e019 View commit details
  4. Copy the full SHA
    a1a82d6 View commit details
  5. Copy the full SHA
    a431f4e View commit details
  6. Copy the full SHA
    6d4e867 View commit details
  7. Copy the full SHA
    95dae6d View commit details
  8. Add log_wire() API

    cliffordwolf committed Feb 11, 2017
    Copy the full SHA
    63dfdb5 View commit details
  9. Copy the full SHA
    eb7b18e View commit details
  10. Copy the full SHA
    0b7aac6 View commit details
  11. Copy the full SHA
    fa4a7ef View commit details
  12. Copy the full SHA
    c449f4b View commit details
  13. Copy the full SHA
    cdb6ceb View commit details
  14. Copy the full SHA
    203b521 View commit details
Showing with 273 additions and 58 deletions.
  1. +30 −21 Makefile
  2. +22 −6 README.md
  3. +137 −8 frontends/verific/verific.cc
  4. +11 −9 frontends/verilog/verilog_lexer.l
  5. +13 −2 frontends/verilog/verilog_parser.y
  6. +7 −0 kernel/log.cc
  7. +1 −0 kernel/log.h
  8. +43 −9 passes/opt/opt_expr.cc
  9. +6 −2 passes/opt/opt_merge.cc
  10. +3 −1 passes/opt/opt_rmdff.cc
51 changes: 30 additions & 21 deletions Makefile
Original file line number Diff line number Diff line change
@@ -53,27 +53,35 @@ all: top-all
YOSYS_SRC := $(dir $(firstword $(MAKEFILE_LIST)))
VPATH := $(YOSYS_SRC)

CXXFLAGS += -Wall -Wextra -ggdb -I. -I"$(YOSYS_SRC)" -MD -D_YOSYS_ -fPIC -I$(PREFIX)/include
LDFLAGS += -L$(LIBDIR)
LDLIBS = -lstdc++ -lm
CXXFLAGS := $(CXXFLAGS) -Wall -Wextra -ggdb -I. -I"$(YOSYS_SRC)" -MD -D_YOSYS_ -fPIC -I$(PREFIX)/include
LDFLAGS := $(LDFLAGS) -L$(LIBDIR)
LDLIBS := $(LDLIBS) -lstdc++ -lm

PKG_CONFIG = pkg-config
SED = sed
BISON = bison
PKG_CONFIG ?= pkg-config
SED ?= sed
BISON ?= bison

ifeq (Darwin,$(findstring Darwin,$(shell uname)))
# add macports/homebrew include and library path to search directories, don't use '-rdynamic' and '-lrt':
CXXFLAGS += -I/opt/local/include -I/usr/local/opt/readline/include
LDFLAGS += -L/opt/local/lib -L/usr/local/opt/readline/lib
# add homebrew's libffi include and library path
CXXFLAGS += $(shell PKG_CONFIG_PATH=$$(brew list libffi | grep pkgconfig | xargs dirname) pkg-config --silence-errors --cflags libffi)
LDFLAGS += $(shell PKG_CONFIG_PATH=$$(brew list libffi | grep pkgconfig | xargs dirname) pkg-config --silence-errors --libs libffi)
# use bison installed by homebrew if available
BISON = $(shell (brew list bison | grep -m1 "bin/bison") || echo bison)
SED = sed
# homebrew search paths
ifneq ($(shell which brew),)
BREW_PREFIX := $(shell brew --prefix)/opt
CXXFLAGS += -I$(BREW_PREFIX)/readline/include
LDFLAGS += -L$(BREW_PREFIX)/readline/lib
PKG_CONFIG_PATH := $(BREW_PREFIX)/libffi/lib/pkgconfig:$(PKG_CONFIG_PATH)
PKG_CONFIG_PATH := $(BREW_PREFIX)/tcl-tk/lib/pkgconfig:$(PKG_CONFIG_PATH)
export PATH := $(BREW_PREFIX)/bison/bin:$(BREW_PREFIX)/gettext/bin:$(BREW_PREFIX)/flex/bin:$(PATH)

# macports search paths
else ifneq ($(shell which port),)
PORT_PREFIX := $(patsubst %/bin/port,%,$(shell which port))
CXXFLAGS += -I$(PORT_PREFIX)/include
LDFLAGS += -L$(PORT_PREFIX)/lib
PKG_CONFIG_PATH := $(PORT_PREFIX)/lib/pkgconfig:$(PKG_CONFIG_PATH)
export PATH := $(PORT_PREFIX)/bin:$(PATH)
endif
else
LDFLAGS += -rdynamic
LDLIBS += -lrt
LDFLAGS += -rdynamic
LDLIBS += -lrt
endif

YOSYS_VER := 0.7+$(shell cd $(YOSYS_SRC) && test -e .git && { git log --author=clifford@clifford.at --oneline 61f6811.. | wc -l; })
@@ -210,15 +218,16 @@ endif
endif

ifeq ($(ENABLE_PLUGINS),1)
CXXFLAGS += -DYOSYS_ENABLE_PLUGINS $(shell $(PKG_CONFIG) --silence-errors --cflags libffi)
LDLIBS += $(shell $(PKG_CONFIG) --silence-errors --libs libffi || echo -lffi) -ldl
CXXFLAGS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --cflags libffi) -DYOSYS_ENABLE_PLUGINS
LDLIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs libffi || echo -lffi) -ldl
endif

ifeq ($(ENABLE_TCL),1)
TCL_VERSION ?= tcl$(shell bash -c "tclsh <(echo 'puts [info tclversion]')")
TCL_INCLUDE ?= /usr/include/$(TCL_VERSION)
CXXFLAGS += -I$(TCL_INCLUDE) -DYOSYS_ENABLE_TCL
LDLIBS += -l$(TCL_VERSION)

CXXFLAGS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --cflags tcl || echo -I$(TCL_INCLUDE)) -DYOSYS_ENABLE_TCL
LDLIBS += $(shell PKG_CONFIG_PATH=$(PKG_CONFIG_PATH) $(PKG_CONFIG) --silence-errors --libs tcl || echo -l$(TCL_VERSION))
endif

ifeq ($(ENABLE_GPROF),1)
28 changes: 22 additions & 6 deletions README.md
Original file line number Diff line number Diff line change
@@ -40,21 +40,28 @@ Web Site
More information and documentation can be found on the Yosys web site:
http://www.clifford.at/yosys/


Getting Started
===============
Setup
======

You need a C++ compiler with C++11 support (up-to-date CLANG or GCC is
recommended) and some standard tools such as GNU Flex, GNU Bison, and GNU Make.
TCL, readline and libffi are optional (see ``ENABLE_*`` settings in Makefile).
Xdot (graphviz) is used by the ``show`` command in yosys to display schematics.

For example on Ubuntu Linux 16.04 LTS the following commands will install all
prerequisites for building yosys:

$ sudo apt-get install build-essential clang bison flex \
libreadline-dev gawk tcl-dev libffi-dev git mercurial \
graphviz xdot pkg-config python3

Similarily, on Mac OS X MacPorts or Homebrew can be used to install dependencies:

$ brew install bison flex gawk libffi \
git mercurial graphviz pkg-config python3
$ sudo port install bison flex readline gawk libffi \
git mercurial graphviz pkgconfig python36

There are also pre-compiled Yosys binary packages for Ubuntu and Win32 as well
as a source distribution for Visual Studio. Visit the Yosys download page for
more information: http://www.clifford.at/yosys/download.html
@@ -80,6 +87,9 @@ To build Yosys simply type 'make' in this directory.
Note that this also downloads, builds and installs ABC (using yosys-abc
as executable name).

Getting Started
===============

Yosys can be used with the interactive command shell, with
synthesis scripts or with command line arguments. Let's perform
a simple synthesis job using the interactive command shell:
@@ -379,10 +389,13 @@ Non-standard or SystemVerilog features for formal verification
to 0 otherwise.

- The system task ``$anyconst`` evaluates to any constant value. This is
equivalent to declaring a reg as ``const rand``.
equivalent to declaring a reg as ``rand const``, but also works outside
of checkers. (Yosys also supports ``rand const`` outside checkers.)

- The system task ``$anyseq`` evaluates to any value, possibly a different
value in each cycle. This is equivalent to declaring a reg as ``rand``.
value in each cycle. This is equivalent to declaring a reg as ``rand``,
but also works outside of checkers. (Yosys also supports ``rand``
variables outside checkers.)

- The SystemVerilog tasks ``$past``, ``$stable``, ``$rose`` and ``$fell`` are
supported in any clocked block.
@@ -407,7 +420,10 @@ from SystemVerilog:
- The keywords ``always_comb``, ``always_ff`` and ``always_latch``, ``logic``
and ``bit`` are supported.

- Declaring free variables with ``rand`` and ``const rand`` is supported.
- Declaring free variables with ``rand`` and ``rand const`` is supported.

- Checkers without a port list that do not need to be instantiated (but instead
behave like a named block) are supported.

- SystemVerilog packages are supported. Once a SystemVerilog file is read
into a design with ``read_verilog``, all its packages are available to
145 changes: 137 additions & 8 deletions frontends/verific/verific.cc
Original file line number Diff line number Diff line change
@@ -57,18 +57,24 @@ PRIVATE_NAMESPACE_BEGIN

void msg_func(msg_type_t msg_type, const char *message_id, linefile_type linefile, const char *msg, va_list args)
{
log("VERIFIC-%s [%s] ",
string message = stringf("VERIFIC-%s [%s] ",
msg_type == VERIFIC_NONE ? "NONE" :
msg_type == VERIFIC_ERROR ? "ERROR" :
msg_type == VERIFIC_WARNING ? "WARNING" :
msg_type == VERIFIC_IGNORE ? "IGNORE" :
msg_type == VERIFIC_INFO ? "INFO" :
msg_type == VERIFIC_COMMENT ? "COMMENT" :
msg_type == VERIFIC_PROGRAM_ERROR ? "PROGRAM_ERROR" : "UNKNOWN", message_id);

if (linefile)
log("%s:%d: ", LineFile::GetFileName(linefile), LineFile::GetLineNo(linefile));
logv(msg, args);
log("\n");
message += stringf("%s:%d: ", LineFile::GetFileName(linefile), LineFile::GetLineNo(linefile));

message += vstringf(msg, args);

if (msg_type == VERIFIC_ERROR || msg_type == VERIFIC_WARNING || msg_type == VERIFIC_PROGRAM_ERROR)
log_warning("%s\n", message.c_str());
else
log("%s\n", message.c_str());
}

struct VerificImporter
@@ -617,6 +623,10 @@ struct VerificImporter

module->fixup_ports();

dict<Net*, char, hash_ptr_ops> init_nets;
pool<Net*, hash_ptr_ops> anyconst_nets;
pool<Net*, hash_ptr_ops> anyseq_nets;

FOREACH_NET_OF_NETLIST(nl, mi, net)
{
if (net->IsRamNet())
@@ -643,9 +653,59 @@ struct VerificImporter

memory->width = bits_in_word;
memory->size = number_of_bits / bits_in_word;

const char *ascii_initdata = net->GetWideInitialValue();
if (ascii_initdata) {
while (*ascii_initdata != 0 && *ascii_initdata != '\'')
ascii_initdata++;
if (*ascii_initdata == '\'')
ascii_initdata++;
if (*ascii_initdata != 0) {
log_assert(*ascii_initdata == 'b');
ascii_initdata++;
}
for (int word_idx = 0; word_idx < memory->size; word_idx++) {
Const initval = Const(State::Sx, memory->width);
bool initval_valid = false;
for (int bit_idx = memory->width-1; bit_idx >= 0; bit_idx--) {
if (*ascii_initdata == 0)
break;
if (*ascii_initdata == '0' || *ascii_initdata == '1') {
initval[bit_idx] = (*ascii_initdata == '0') ? State::S0 : State::S1;
initval_valid = true;
}
ascii_initdata++;
}
if (initval_valid) {
RTLIL::Cell *cell = module->addCell(NEW_ID, "$meminit");
cell->parameters["\\WORDS"] = 1;
if (net->GetOrigTypeRange()->LeftRangeBound() < net->GetOrigTypeRange()->RightRangeBound())
cell->setPort("\\ADDR", word_idx);
else
cell->setPort("\\ADDR", memory->size - word_idx - 1);
cell->setPort("\\DATA", initval);
cell->parameters["\\MEMID"] = RTLIL::Const(memory->name.str());
cell->parameters["\\ABITS"] = 32;
cell->parameters["\\WIDTH"] = memory->width;
cell->parameters["\\PRIORITY"] = RTLIL::Const(autoidx-1);
}
}
}
continue;
}

if (net->GetInitialValue())
init_nets[net] = net->GetInitialValue();

const char *rand_const_attr = net->GetAttValue(" rand_const");
const char *rand_attr = net->GetAttValue(" rand");

if (rand_const_attr != nullptr && !strcmp(rand_const_attr, "1"))
anyconst_nets.insert(net);

else if (rand_attr != nullptr && !strcmp(rand_attr, "1"))
anyseq_nets.insert(net);

if (net_map.count(net)) {
// log(" skipping net %s.\n", net->Name());
continue;
@@ -683,25 +743,94 @@ struct VerificImporter
wire->start_offset = min(netbus->LeftIndex(), netbus->RightIndex());
import_attributes(wire->attributes, netbus);

for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1) {
if (netbus->ElementAtIndex(i)) {
RTLIL::Const initval = Const(State::Sx, GetSize(wire));
bool initval_valid = false;

for (int i = netbus->LeftIndex();; i += netbus->IsUp() ? +1 : -1)
{
if (netbus->ElementAtIndex(i))
{
int bitidx = i - wire->start_offset;
net = netbus->ElementAtIndex(i);
RTLIL::SigBit bit(wire, i - wire->start_offset);
RTLIL::SigBit bit(wire, bitidx);

if (init_nets.count(net)) {
if (init_nets.at(net) == '0')
initval.bits.at(bitidx) = State::S0;
if (init_nets.at(net) == '1')
initval.bits.at(bitidx) = State::S1;
initval_valid = true;
init_nets.erase(net);
}

if (net_map.count(net) == 0)
net_map[net] = bit;
else
module->connect(bit, net_map.at(net));
}

if (i == netbus->RightIndex())
break;
}

if (initval_valid)
wire->attributes["\\init"] = initval;
}
else
{
// log(" skipping netbus %s.\n", netbus->Name());
}

SigSpec anyconst_sig;
SigSpec anyseq_sig;

for (int i = netbus->RightIndex();; i += netbus->IsUp() ? -1 : +1) {
net = netbus->ElementAtIndex(i);
if (net != nullptr && anyconst_nets.count(net)) {
anyconst_sig.append(net_map.at(net));
anyconst_nets.erase(net);
}
if (net != nullptr && anyseq_nets.count(net)) {
anyseq_sig.append(net_map.at(net));
anyseq_nets.erase(net);
}
if (i == netbus->LeftIndex())
break;
}

if (GetSize(anyconst_sig))
module->connect(anyconst_sig, module->Anyconst(NEW_ID, GetSize(anyconst_sig)));

if (GetSize(anyseq_sig))
module->connect(anyseq_sig, module->Anyseq(NEW_ID, GetSize(anyseq_sig)));
}

for (auto it : init_nets)
{
Const initval;
SigBit bit = net_map.at(it.first);
log_assert(bit.wire);

if (bit.wire->attributes.count("\\init"))
initval = bit.wire->attributes.at("\\init");

while (GetSize(initval) < GetSize(bit.wire))
initval.bits.push_back(State::Sx);

if (it.second == '0')
initval.bits.at(bit.offset) = State::S0;
if (it.second == '1')
initval.bits.at(bit.offset) = State::S1;

bit.wire->attributes["\\init"] = initval;
}

for (auto net : anyconst_nets)
module->connect(net_map.at(net), module->Anyconst(NEW_ID));

for (auto net : anyseq_nets)
module->connect(net_map.at(net), module->Anyseq(NEW_ID));

FOREACH_INSTANCE_OF_NETLIST(nl, mi, inst)
{
if (inst->Type() == PRIM_SVA_POSEDGE) {
@@ -733,7 +862,7 @@ struct VerificImporter

SigBit outsig = net_map.at(out);
log_assert(outsig.wire && GetSize(outsig.wire) == 1);
outsig.wire->attributes["\\init"] == Const(0, 1);
outsig.wire->attributes["\\init"] = Const(1, 1);

module->addDff(NEW_ID, net_map.at(clk), net_map.at(in2), net_map.at(out));
continue;
20 changes: 11 additions & 9 deletions frontends/verilog/verilog_lexer.l
Original file line number Diff line number Diff line change
@@ -175,15 +175,17 @@ YOSYS_NAMESPACE_END
"always_ff" { SV_KEYWORD(TOK_ALWAYS); }
"always_latch" { SV_KEYWORD(TOK_ALWAYS); }

"assert" { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); }
"assume" { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); }
"cover" { if (formal_mode) return TOK_COVER; SV_KEYWORD(TOK_COVER); }
"restrict" { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); }
"property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); }
"rand" { if (formal_mode) return TOK_RAND; SV_KEYWORD(TOK_RAND); }
"const" { if (formal_mode) return TOK_CONST; SV_KEYWORD(TOK_CONST); }
"logic" { SV_KEYWORD(TOK_REG); }
"bit" { SV_KEYWORD(TOK_REG); }
"assert" { if (formal_mode) return TOK_ASSERT; SV_KEYWORD(TOK_ASSERT); }
"assume" { if (formal_mode) return TOK_ASSUME; SV_KEYWORD(TOK_ASSUME); }
"cover" { if (formal_mode) return TOK_COVER; SV_KEYWORD(TOK_COVER); }
"restrict" { if (formal_mode) return TOK_RESTRICT; SV_KEYWORD(TOK_RESTRICT); }
"property" { if (formal_mode) return TOK_PROPERTY; SV_KEYWORD(TOK_PROPERTY); }
"rand" { if (formal_mode) return TOK_RAND; SV_KEYWORD(TOK_RAND); }
"const" { if (formal_mode) return TOK_CONST; SV_KEYWORD(TOK_CONST); }
"checker" { if (formal_mode) return TOK_CHECKER; SV_KEYWORD(TOK_CHECKER); }
"endchecker" { if (formal_mode) return TOK_ENDCHECKER; SV_KEYWORD(TOK_ENDCHECKER); }
"logic" { SV_KEYWORD(TOK_REG); }
"bit" { SV_KEYWORD(TOK_REG); }

"input" { return TOK_INPUT; }
"output" { return TOK_OUTPUT; }
Loading