Clifford Wolf [Fri, 14 Oct 2016 16:20:36 +0000 (18:20 +0200)]
Avoid using strcasecmp()
Clifford Wolf [Fri, 14 Oct 2016 15:18:18 +0000 (17:18 +0200)]
Fixed version string for out-of-tree builds
Clifford Wolf [Fri, 14 Oct 2016 13:39:33 +0000 (15:39 +0200)]
Added notes about some formal features to README
Clifford Wolf [Fri, 14 Oct 2016 13:24:03 +0000 (15:24 +0200)]
Added $anyseq cell type
Clifford Wolf [Fri, 14 Oct 2016 12:55:07 +0000 (14:55 +0200)]
Added clk2fflogic
Clifford Wolf [Fri, 14 Oct 2016 11:02:36 +0000 (13:02 +0200)]
Added opt_rmdff support for $ff cells
Clifford Wolf [Fri, 14 Oct 2016 10:33:56 +0000 (12:33 +0200)]
Added $global_clock verilog syntax support for creating $ff cells
Clifford Wolf [Fri, 14 Oct 2016 08:36:37 +0000 (10:36 +0200)]
Added MEMID handling to "flatten" pass
Clifford Wolf [Fri, 14 Oct 2016 07:36:40 +0000 (09:36 +0200)]
Merge branch 'master' of github.com:cliffordwolf/yosys
Clifford Wolf [Fri, 14 Oct 2016 07:36:31 +0000 (09:36 +0200)]
Merge pull request #246 from set-soft/abc_external_ovr
Allow to overwrite ABCEXTERNAL from the environment.
Clifford Wolf [Fri, 14 Oct 2016 07:35:18 +0000 (09:35 +0200)]
Added YOSYS_VER_STR make variable
Salvador E. Tropea [Thu, 13 Oct 2016 20:57:09 +0000 (17:57 -0300)]
Ugh! extra patches got here, reverting
Salvador E. Tropea [Thu, 13 Oct 2016 20:51:14 +0000 (17:51 -0300)]
Allow to overwrite ABCEXTERNAL from the environment.
In this way Debian scripts can define it as berkeley-abc from the shell.
Salvador E. Tropea [Thu, 13 Oct 2016 20:38:42 +0000 (17:38 -0300)]
Modified test target name (to test-all)
As this target depends on external tools, and packagers run "make test",
I think the name should be less generic.
Salvador E. Tropea [Thu, 13 Oct 2016 20:34:15 +0000 (17:34 -0300)]
Added a new configuration variable GIT_REV_WHERE
It determines from where we get the gits SHA1 value. By default is HEAD,
suitable for Clifford, but for Debian we can define it as upstream/master
Clifford Wolf [Wed, 12 Oct 2016 10:05:19 +0000 (12:05 +0200)]
Added "zinit" pass
Clifford Wolf [Tue, 11 Oct 2016 23:18:39 +0000 (01:18 +0200)]
Added $ff and $_FF_ cell types
Clifford Wolf [Tue, 11 Oct 2016 10:12:32 +0000 (12:12 +0200)]
Fixed "make test" for git head of iverilog
Clifford Wolf [Tue, 11 Oct 2016 10:12:09 +0000 (12:12 +0200)]
define PATH_MAX if not defined by limits.h
Clifford Wolf [Tue, 11 Oct 2016 01:58:27 +0000 (03:58 +0200)]
Merge branch 'master' of github.com:cliffordwolf/yosys
Clifford Wolf [Sat, 8 Oct 2016 10:25:34 +0000 (12:25 +0200)]
Added smtc support for top-level state with [], [N:] syntax
Clifford Wolf [Mon, 3 Oct 2016 22:54:44 +0000 (00:54 +0200)]
Bugfix in yosys-smtbmc --noincr
Clifford Wolf [Mon, 3 Oct 2016 18:43:38 +0000 (20:43 +0200)]
yosys-smtbmc: ABC is a QF_BV solver
Clifford Wolf [Mon, 3 Oct 2016 18:30:38 +0000 (20:30 +0200)]
Added "yosys-smtbmc --noincr"
Clifford Wolf [Sun, 2 Oct 2016 20:08:53 +0000 (22:08 +0200)]
Update ABV to hg rev
eb6eca6807cc
Clifford Wolf [Sun, 2 Oct 2016 20:08:30 +0000 (22:08 +0200)]
yosys-smtbmc: added smtc [...] support for cells
Clifford Wolf [Sat, 1 Oct 2016 11:54:21 +0000 (13:54 +0200)]
Added "yosys-smtbmc -s abc"
Clifford Wolf [Sat, 1 Oct 2016 10:23:24 +0000 (12:23 +0200)]
Updated ABV to hg rev
6b74de13c57f
Clifford Wolf [Fri, 30 Sep 2016 15:02:52 +0000 (17:02 +0200)]
Added "prep -nokeepdc"
Clifford Wolf [Fri, 30 Sep 2016 15:02:38 +0000 (17:02 +0200)]
Added "opt_rmdff -keepdc"
Clifford Wolf [Fri, 30 Sep 2016 08:56:36 +0000 (10:56 +0200)]
Updated ABV to hg rev
2bc57cc30593
Clifford Wolf [Sat, 24 Sep 2016 18:40:22 +0000 (20:40 +0200)]
Minor improvements in yosys-smtbmc
Clifford Wolf [Fri, 23 Sep 2016 11:53:23 +0000 (13:53 +0200)]
Added liberty parser support for types within cell decls
Clifford Wolf [Fri, 23 Sep 2016 11:42:08 +0000 (13:42 +0200)]
Merge branch 'master' of https://github.com/brouhaha/yosys
Eric Smith [Thu, 15 Sep 2016 08:00:29 +0000 (02:00 -0600)]
Add optional SEED=n command line option to Makefile, and -S n command line option to test scripts, for deterministic regression tests.
Clifford Wolf [Tue, 20 Sep 2016 07:29:56 +0000 (09:29 +0200)]
Added autotest.sh -I
Clifford Wolf [Mon, 19 Sep 2016 18:43:43 +0000 (20:43 +0200)]
Cosmetic fix in test_autotb.cc
Clifford Wolf [Mon, 19 Sep 2016 18:43:28 +0000 (20:43 +0200)]
Added yosys-smtbmc --noinfo and --dummy
Clifford Wolf [Mon, 19 Sep 2016 08:20:20 +0000 (10:20 +0200)]
Avoid creating very long strings in test_autotb
Clifford Wolf [Sun, 18 Sep 2016 23:30:07 +0000 (01:30 +0200)]
Added $past, $stable, $rose, $fell SVA functions
Clifford Wolf [Sun, 18 Sep 2016 18:48:09 +0000 (20:48 +0200)]
Improved handling of SMT2 logics in yosys-smtbmc
Clifford Wolf [Sun, 18 Sep 2016 16:48:59 +0000 (18:48 +0200)]
Added support for bus interfaces to "read_liberty -lib"
Clifford Wolf [Sat, 17 Sep 2016 22:50:02 +0000 (00:50 +0200)]
Merge branch 'master' of github.com:cliffordwolf/yosys
Clifford Wolf [Sat, 17 Sep 2016 22:48:36 +0000 (00:48 +0200)]
yosys-smtbmc: added -i support smtc files
Clifford Wolf [Wed, 14 Sep 2016 18:46:54 +0000 (20:46 +0200)]
Bugfix in techmap parameter handling
Clifford Wolf [Tue, 13 Sep 2016 11:23:06 +0000 (13:23 +0200)]
Work-around for boolector bug
Clifford Wolf [Tue, 13 Sep 2016 10:34:19 +0000 (12:34 +0200)]
Merge pull request #228 from Kmanfi/test
Fix for modules with big interfaces.
Kaj Tuomi [Tue, 13 Sep 2016 10:13:27 +0000 (13:13 +0300)]
Fix for modules with big interfaces.
Clifford Wolf [Sun, 11 Sep 2016 16:08:56 +0000 (18:08 +0200)]
Added missing :produce-models setting to smtio.py
Clifford Wolf [Sat, 10 Sep 2016 14:24:08 +0000 (16:24 +0200)]
Minor improvements to smtio.py vcd writer
Clifford Wolf [Sat, 10 Sep 2016 13:14:41 +0000 (15:14 +0200)]
fixed write_smt2 for (non-combinatorial) loops through hierarchical cells
Clifford Wolf [Thu, 8 Sep 2016 16:08:15 +0000 (18:08 +0200)]
smt2 mem init bugfix
Clifford Wolf [Thu, 8 Sep 2016 09:17:05 +0000 (11:17 +0200)]
Merge branch 'master' of github.com:cliffordwolf/yosys
Clifford Wolf [Thu, 8 Sep 2016 09:16:12 +0000 (11:16 +0200)]
yosys-smtbmc meminit support
Clifford Wolf [Thu, 8 Sep 2016 08:06:40 +0000 (10:06 +0200)]
Merge pull request #225 from Kmanfi/test
Typo fix.
Kaj Tuomi [Thu, 8 Sep 2016 07:57:16 +0000 (10:57 +0300)]
Typo fix.
Clifford Wolf [Wed, 7 Sep 2016 19:01:51 +0000 (21:01 +0200)]
Bugfix in "yosys-smtbmc --unroll"
Clifford Wolf [Wed, 7 Sep 2016 18:57:56 +0000 (20:57 +0200)]
Added "yosys-smtbmc --unroll"
Clifford Wolf [Wed, 7 Sep 2016 11:43:57 +0000 (13:43 +0200)]
Install celledges.h
Clifford Wolf [Wed, 7 Sep 2016 10:42:16 +0000 (12:42 +0200)]
Improvements in assertpmux
Clifford Wolf [Wed, 7 Sep 2016 09:08:54 +0000 (11:08 +0200)]
Updated ABC to hg
8e08604f8ad3
Clifford Wolf [Tue, 6 Sep 2016 22:28:01 +0000 (00:28 +0200)]
Added assertpmux
Clifford Wolf [Tue, 6 Sep 2016 15:43:24 +0000 (17:43 +0200)]
Added "tee +INT -INT"
Clifford Wolf [Tue, 6 Sep 2016 15:35:25 +0000 (17:35 +0200)]
Run log_flush() before solving in sat command
Clifford Wolf [Tue, 6 Sep 2016 15:35:06 +0000 (17:35 +0200)]
Bugfix in parsing of BLIF latch init values
Clifford Wolf [Tue, 6 Sep 2016 15:34:42 +0000 (17:34 +0200)]
Avoid creation of bogus initial blocks for assert/assume in always @*
Larry Doolittle [Tue, 6 Sep 2016 02:58:18 +0000 (19:58 -0700)]
Fix spelling and grammar in README
Clifford Wolf [Mon, 5 Sep 2016 23:40:31 +0000 (01:40 +0200)]
yosys-smtbmc: flush stdout after each log msg
Clifford Wolf [Sun, 4 Sep 2016 14:32:47 +0000 (16:32 +0200)]
Minor bugfix in write_smt2
Clifford Wolf [Sat, 3 Sep 2016 16:49:53 +0000 (18:49 +0200)]
Minor README updates
Clifford Wolf [Sat, 3 Sep 2016 12:26:00 +0000 (14:26 +0200)]
Added boolector support to yosys-smtbmc
Clifford Wolf [Fri, 2 Sep 2016 11:55:51 +0000 (13:55 +0200)]
Merge branch 'smtbmc-kmanfi'
Clifford Wolf [Fri, 2 Sep 2016 11:54:24 +0000 (13:54 +0200)]
Made examples/smtbmc/demo1.v more interesting
Clifford Wolf [Fri, 2 Sep 2016 11:46:56 +0000 (13:46 +0200)]
Don't re-create hex_dict for each value
Kaj Tuomi [Fri, 2 Sep 2016 10:09:09 +0000 (13:09 +0300)]
More PEP 8 fixes.
Kaj Tuomi [Fri, 2 Sep 2016 10:01:31 +0000 (13:01 +0300)]
Indentation and PEP 8 fixes. CamelCase and white space after semicolon.
Kaj Tuomi [Fri, 2 Sep 2016 09:50:23 +0000 (12:50 +0300)]
Use dict lookup instead of many ifs.
Kaj Tuomi [Fri, 2 Sep 2016 08:12:30 +0000 (11:12 +0300)]
Fix: Unresolved reference.
Kaj Tuomi [Fri, 2 Sep 2016 08:02:19 +0000 (11:02 +0300)]
Some syntax fixes. Generator and comma separated list modifications.
Clifford Wolf [Tue, 30 Aug 2016 21:57:24 +0000 (23:57 +0200)]
Added "prep -nomem"
Clifford Wolf [Tue, 30 Aug 2016 17:27:42 +0000 (19:27 +0200)]
Added $anyconst support to yosys-smtbmc
Clifford Wolf [Tue, 30 Aug 2016 17:09:56 +0000 (19:09 +0200)]
Removed $aconst cell type
Clifford Wolf [Tue, 30 Aug 2016 12:49:47 +0000 (14:49 +0200)]
Fixed memory bug in write_smt2
Clifford Wolf [Tue, 30 Aug 2016 10:40:09 +0000 (12:40 +0200)]
Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem"
Clifford Wolf [Tue, 30 Aug 2016 09:26:10 +0000 (11:26 +0200)]
Added $anyconst support to smt2 back-end
Clifford Wolf [Mon, 29 Aug 2016 23:34:04 +0000 (01:34 +0200)]
Improved init spec handling in opt_rmdff, modernized the code a bit
Clifford Wolf [Mon, 29 Aug 2016 20:41:45 +0000 (22:41 +0200)]
Added "yosys-smtbmc --dump-all"
Clifford Wolf [Mon, 29 Aug 2016 12:53:32 +0000 (14:53 +0200)]
More yosys-smtbmc bugfixes
Clifford Wolf [Mon, 29 Aug 2016 11:53:12 +0000 (13:53 +0200)]
Various fixes and improvements in yosys-smtbmc
Clifford Wolf [Sun, 28 Aug 2016 19:35:33 +0000 (21:35 +0200)]
Removed $predict again
Clifford Wolf [Sun, 28 Aug 2016 10:34:36 +0000 (12:34 +0200)]
Improved "show" help message
Clifford Wolf [Sat, 27 Aug 2016 20:04:15 +0000 (22:04 +0200)]
Some changes to yosys-smtbmc cmd line options, add --final-only
Clifford Wolf [Sat, 27 Aug 2016 15:06:22 +0000 (17:06 +0200)]
Fixed handling of transparent bram rd ports on ROMs
Clifford Wolf [Sat, 27 Aug 2016 12:30:36 +0000 (14:30 +0200)]
Added smtc "final" statement
Clifford Wolf [Fri, 26 Aug 2016 21:36:15 +0000 (23:36 +0200)]
Merge branch 'master' of github.com:cliffordwolf/yosys
Clifford Wolf [Fri, 26 Aug 2016 21:36:05 +0000 (23:36 +0200)]
Merge pull request #215 from frznchckn/to_upstream
Add some useful flexibility to build process
Clifford Wolf [Fri, 26 Aug 2016 21:35:27 +0000 (23:35 +0200)]
Added read_verilog -norestrict -assume-asserts
Russell L Friesenhahn [Fri, 26 Aug 2016 16:15:36 +0000 (11:15 -0500)]
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
Russell L Friesenhahn [Wed, 17 Aug 2016 03:07:36 +0000 (22:07 -0500)]
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
Clifford Wolf [Fri, 26 Aug 2016 15:33:02 +0000 (17:33 +0200)]
Various fixes and improvements in smt2 back-end