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: 0c83a30f950d
Choose a base ref
...
head repository: azonenberg/yosys
Failed to load repositories. Confirm that selected head ref is valid, then try again.
Loading
compare: 0d7e71f7abd4
Choose a head ref

Commits on Jan 15, 2017

  1. Fix issue YosysHQ#269, optimize signed compare with 0

    add opt_compare pass and add it to opt
    for a < 0:
        if a is signed, replace with a[max_bit-1]
    for a >= 0:
        if a is signed, replace with ~a[max_bit-1]
    C-Elegans committed Jan 15, 2017
    Copy the full SHA
    943389c View commit details
  2. passes/hierarchy: delete some dead code

    Signed-off-by: Austin Seipp <aseipp@pobox.com>
    thoughtpolice committed Jan 15, 2017
    Copy the full SHA
    6781543 View commit details

Commits on Jan 16, 2017

  1. Merge pull request YosysHQ#293 from thoughtpolice/minor-cleanup

    Delete some dead code in the Hierarchy pass
    cliffordwolf authored Jan 16, 2017
    Copy the full SHA
    87fe8ab View commit details
  2. Optimize compares to powers of 2

    Remove opt_compare and put comparison pass in opt_expr
    
    assuming a [7:0] is unsigned
    a >= (1<<x) becomes |a[7:x]
    a <  (1<<x) becomes !a[7:x]
    
    Additionally:
    a >= 0 becomes constant true,
    a < 0 becomes constant false
    
    delete opt_compare.cc
    revert opt.cc to commit b7cfb7d (remove opt_compare step)
    C-Elegans committed Jan 16, 2017
    Copy the full SHA
    84f9cd0 View commit details

Commits on Jan 17, 2017

  1. Copy the full SHA
    fea5282 View commit details

Commits on Jan 21, 2017

  1. Copy the full SHA
    2fa0fd4 View commit details

Commits on Jan 25, 2017

  1. Copy the full SHA
    b54972c View commit details

Commits on Jan 26, 2017

  1. Copy the full SHA
    b0a430f View commit details
  2. Copy the full SHA
    49b8160 View commit details
  3. Copy the full SHA
    45e10c1 View commit details

Commits on Jan 28, 2017

  1. Copy the full SHA
    e54c355 View commit details

Commits on Jan 30, 2017

  1. Copy the full SHA
    fe29869 View commit details
  2. Copy the full SHA
    18ea65e View commit details
  3. Refactor and generalize the comparision optimization

    Generalizes the optimization to:
    a < C,
    a >= C,
    C > a,
    C <= a
    C-Elegans committed Jan 30, 2017
    Copy the full SHA
    a94c369 View commit details

Commits on Jan 31, 2017

  1. Copy the full SHA
    7481ba4 View commit details
  2. Merge branch 'opt_compare_pr' of https://github.com/C-Elegans/yosys i…

    …nto C-Elegans-opt_compare_pr
    cliffordwolf committed Jan 31, 2017
    Copy the full SHA
    19a9802 View commit details
  3. Copy the full SHA
    ffbe8d4 View commit details
  4. Copy the full SHA
    c17aab2 View commit details

Commits on Feb 1, 2017

  1. Copy the full SHA
    8927e19 View commit details
  2. Copy the full SHA
    249ddbc View commit details

Commits on Feb 4, 2017

  1. Copy the full SHA
    911c44d View commit details
  2. Copy the full SHA
    3928482 View commit details
  3. Copy the full SHA
    6abf79e View commit details
  4. Copy the full SHA
    0c0784b View commit details
  5. Copy the full SHA
    adbecfe View commit details
  6. Copy the full SHA
    5541b42 View commit details

Commits on Feb 5, 2017

  1. Use -E sed parameter instead of -r.

    BSD sed equivalent to -r parameter is -E and it is also supported in GNU
    sed thus using -E results in support on both platforms.
    esden committed Feb 5, 2017
    Copy the full SHA
    e3a12b5 View commit details
  2. Merge pull request YosysHQ#304 from esden/gsed-darwin

    Use gsed vs sed on Darwin.
    cliffordwolf authored Feb 5, 2017
    Copy the full SHA
    1064c8f View commit details
  3. Copy the full SHA
    19303f6 View commit details
  4. Copy the full SHA
    aab5804 View commit details

Commits on Feb 6, 2017

  1. Copy the full SHA
    7e0b776 View commit details

Commits on Feb 8, 2017

  1. Copy the full SHA
    1d1f56a View commit details
  2. Copy the full SHA
    ef4a28e View commit details

Commits on Feb 9, 2017

  1. Copy the full SHA
    0d7e71f View commit details
2 changes: 1 addition & 1 deletion Makefile
Original file line number Diff line number Diff line change
@@ -86,7 +86,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 = f8cadfe3861f
ABCREV = a2fcd1cc61a6
ABCPULL = 1
ABCURL ?= https://bitbucket.org/alanmi/abc
ABCMKARGS = CC="$(CXX)" CXX="$(CXX)"
17 changes: 10 additions & 7 deletions README.md
Original file line number Diff line number Diff line change
@@ -46,7 +46,7 @@ Getting Started

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).
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:
@@ -372,16 +372,17 @@ Verilog Attributes and non-standard features
Non-standard or SystemVerilog features for formal verification
==============================================================

- Support for ``assert``, ``assume``, and ``restrict`` is enabled when
``read_verilog`` is called with ``-formal``.
- Support for ``assert``, ``assume``, ``restrict``, and ``cover'' is enabled
when ``read_verilog`` is called with ``-formal``.

- The system task ``$initstate`` evaluates to 1 in the initial state and
to 0 otherwise.

- The system task ``$anyconst`` evaluates to any constant value.
- The system task ``$anyconst`` evaluates to any constant value. This is
equivalent to declaring a reg as ``const rand``.

- The system task ``$anyseq`` evaluates to any value, possibly a different
value in each cycle.
value in each cycle. This is equivalent to declaring a reg as ``rand``.

- The SystemVerilog tasks ``$past``, ``$stable``, ``$rose`` and ``$fell`` are
supported in any clocked block.
@@ -400,12 +401,14 @@ from SystemVerilog:
form. In module context: ``assert property (<expression>);`` and within an
always block: ``assert(<expression>);``. It is transformed to a $assert cell.

- The ``assume`` and ``restrict`` statements from SystemVerilog are also
supported. The same limitations as with the ``assert`` statement apply.
- The ``assume``, ``restrict``, and ``cover`` statements from SystemVerilog are
also supported. The same limitations as with the ``assert`` statement apply.

- The keywords ``always_comb``, ``always_ff`` and ``always_latch``, ``logic``
and ``bit`` are supported.

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

- SystemVerilog packages are supported. Once a SystemVerilog file is read
into a design with ``read_verilog``, all its packages are available to
SystemVerilog files being read into the same design afterwards.
16 changes: 11 additions & 5 deletions backends/smt2/smt2.cc
Original file line number Diff line number Diff line change
@@ -662,19 +662,25 @@ struct Smt2Worker

if (verbose) log("=> export logic driving asserts\n");

vector<string> assert_list, assume_list;
vector<string> assert_list, assume_list, cover_list;
for (auto cell : module->cells())
if (cell->type.in("$assert", "$assume")) {
if (cell->type.in("$assert", "$assume", "$cover")) {
string name_a = get_bool(cell->getPort("\\A"));
string name_en = get_bool(cell->getPort("\\EN"));
decls.push_back(stringf("; yosys-smt2-%s %s#%d %s\n", cell->type.c_str() + 1, get_id(module), idcounter,
cell->attributes.count("\\src") ? cell->attributes.at("\\src").decode_string().c_str() : get_id(cell)));
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
if (cell->type == "$cover")
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (and %s %s)) ; %s\n",
get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
else
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) Bool (or %s (not %s))) ; %s\n",
get_id(module), idcounter, get_id(module), name_a.c_str(), name_en.c_str(), get_id(cell)));
if (cell->type == "$assert")
assert_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
else
else if (cell->type == "$assume")
assume_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
else if (cell->type == "$cover")
cover_list.push_back(stringf("(|%s#%d| state)", get_id(module), idcounter++));
}

for (int iter = 1; !registers.empty(); iter++)
Loading