yosys-smtbmc: added smtc [...] support for cells

Added "yosys-smtbmc -s abc"

Updated ABV to hg rev 6b74de13c57f

Added "prep -nokeepdc"

Added "opt_rmdff -keepdc"

Updated ABV to hg rev 2bc57cc30593

Minor improvements in yosys-smtbmc

Added liberty parser support for types within cell decls

Merge branch 'master' of https://github.com/brouhaha/yosys

Add optional SEED=n command line option to Makefile, and -S n command line option to test scripts, for deterministic regression tests.

Added autotest.sh -I

Cosmetic fix in test_autotb.cc

Added yosys-smtbmc --noinfo and --dummy

Avoid creating very long strings in test_autotb

Added $past, $stable, $rose, $fell SVA functions

Improved handling of SMT2 logics in yosys-smtbmc

Added support for bus interfaces to "read_liberty -lib"

Merge branch 'master' of github.com:cliffordwolf/yosys

yosys-smtbmc: added -i support smtc files

Bugfix in techmap parameter handling

Work-around for boolector bug

Merge pull request #228 from Kmanfi/test

Fix for modules with big interfaces.

Fix for modules with big interfaces.

Added missing :produce-models setting to smtio.py

Minor improvements to smtio.py vcd writer

fixed write_smt2 for (non-combinatorial) loops through hierarchical cells

smt2 mem init bugfix

Merge branch 'master' of github.com:cliffordwolf/yosys

yosys-smtbmc meminit support

Merge pull request #225 from Kmanfi/test

Typo fix.

Typo fix.

Bugfix in "yosys-smtbmc --unroll"

Added "yosys-smtbmc --unroll"

Install celledges.h

Improvements in assertpmux

Updated ABC to hg 8e08604f8ad3

Added assertpmux

Added "tee +INT -INT"

Run log_flush() before solving in sat command

Bugfix in parsing of BLIF latch init values

Avoid creation of bogus initial blocks for assert/assume in always @*

Fix spelling and grammar in README

yosys-smtbmc: flush stdout after each log msg

Minor bugfix in write_smt2

Minor README updates

Added boolector support to yosys-smtbmc

Merge branch 'smtbmc-kmanfi'

Made examples/smtbmc/demo1.v more interesting

Don't re-create hex_dict for each value

More PEP 8 fixes.

Indentation and PEP 8 fixes. CamelCase and white space after semicolon.

Use dict lookup instead of many ifs.

Fix: Unresolved reference.

Some syntax fixes. Generator and comma separated list modifications.

Added "prep -nomem"

Added $anyconst support to yosys-smtbmc

Removed $aconst cell type

Fixed memory bug in write_smt2

Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem"

Added $anyconst support to smt2 back-end

Improved init spec handling in opt_rmdff, modernized the code a bit

Added "yosys-smtbmc --dump-all"

More yosys-smtbmc bugfixes

Various fixes and improvements in yosys-smtbmc

Removed $predict again

Improved "show" help message

Some changes to yosys-smtbmc cmd line options, add --final-only

Fixed handling of transparent bram rd ports on ROMs

Added smtc "final" statement

Merge branch 'master' of github.com:cliffordwolf/yosys

Merge pull request #215 from frznchckn/to_upstream

Add some useful flexibility to build process

Added read_verilog -norestrict -assume-asserts

Relax test to see if yosys dir is a git repository in Makefile

This prevents the test from failing in the case that yosys is a
submodule of a repository since for a submodule the .git is actually a
file containing the location of the submodule's .git directory

Allow redefining of the ABC repository URL

For persons or organizations that prefer to keep their own mirrors of
repositories, users may now specify the URL of the ABC Mercurial
repository that yosys clones during build.

The URL may be set in the Makefile directly, on the
command-line, or in the environment

Various fixes and improvements in smt2 back-end

Improved verilog parser errors

More yosys-smtbmc smtc features

yosys-smtbmc --smtc -g

Added SV "restrict" keyword

Minor yosys-smtbmc bugfix

Added "yosys-smtbmc --constr"

Added "yosys-smtbmc --dump-constr"

Added glob support to all front-ends

Fixed bug with memories that do not have a down-to-zero data width

Fixed bug in memory_share for memory ports with different ABITS

yosys-smtbmc: improved --dump-vlogtb handling of memories

Added another mem2reg test case

Another bugfix in mem2reg code

Minor improvements to AstNode::dumpAst() and AstNode::dumpVlog()

Added examples/smtbmc/demo2.v

Added "yosys-smtbmc --dump-vlogtb"

Added support for memories to smtio.py

Deprecated "write_smt2 -regs" (by default on now), and some other smt2 back-end improvements

Added "yosys-smtbmc -g"

Added smtbmc longopt support

Fixed finish_addr handling in $readmemh/$readmemb

Bugfix in partial mem write handling in verilog back-end

Added "wreduce -memx"

Added memory_memx pass, "memory -memx", and "prep -memx"

Optimize memory address port width in wreduce and memory_collect, not verilog front-end