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
Clifford Wolf [Thu, 25 Aug 2016 09:44:25 +0000 (11:44 +0200)]
Improved verilog parser errors
Clifford Wolf [Wed, 24 Aug 2016 21:18:29 +0000 (23:18 +0200)]
More yosys-smtbmc smtc features
Clifford Wolf [Wed, 24 Aug 2016 20:09:50 +0000 (22:09 +0200)]
yosys-smtbmc --smtc -g
Clifford Wolf [Wed, 24 Aug 2016 13:30:08 +0000 (15:30 +0200)]
Added SV "restrict" keyword
Clifford Wolf [Mon, 22 Aug 2016 15:45:01 +0000 (17:45 +0200)]
Minor yosys-smtbmc bugfix
Clifford Wolf [Mon, 22 Aug 2016 15:27:43 +0000 (17:27 +0200)]
Added "yosys-smtbmc --constr"
Clifford Wolf [Mon, 22 Aug 2016 14:48:46 +0000 (16:48 +0200)]
Added "yosys-smtbmc --dump-constr"
Clifford Wolf [Mon, 22 Aug 2016 13:05:57 +0000 (15:05 +0200)]
Added glob support to all front-ends
Clifford Wolf [Mon, 22 Aug 2016 12:27:46 +0000 (14:27 +0200)]
Fixed bug with memories that do not have a down-to-zero data width
Clifford Wolf [Mon, 22 Aug 2016 12:26:33 +0000 (14:26 +0200)]
Fixed bug in memory_share for memory ports with different ABITS
Clifford Wolf [Sun, 21 Aug 2016 13:56:22 +0000 (15:56 +0200)]
yosys-smtbmc: improved --dump-vlogtb handling of memories
Clifford Wolf [Sun, 21 Aug 2016 11:45:46 +0000 (13:45 +0200)]
Added another mem2reg test case
Clifford Wolf [Sun, 21 Aug 2016 11:23:58 +0000 (13:23 +0200)]
Another bugfix in mem2reg code
Clifford Wolf [Sun, 21 Aug 2016 11:18:09 +0000 (13:18 +0200)]
Minor improvements to AstNode::dumpAst() and AstNode::dumpVlog()
Clifford Wolf [Sat, 20 Aug 2016 16:44:27 +0000 (18:44 +0200)]
Added examples/smtbmc/demo2.v
Clifford Wolf [Sat, 20 Aug 2016 16:43:39 +0000 (18:43 +0200)]
Added "yosys-smtbmc --dump-vlogtb"
Clifford Wolf [Sat, 20 Aug 2016 16:42:32 +0000 (18:42 +0200)]
Added support for memories to smtio.py
Clifford Wolf [Sat, 20 Aug 2016 16:41:57 +0000 (18:41 +0200)]
Deprecated "write_smt2 -regs" (by default on now), and some other smt2 back-end improvements
Clifford Wolf [Sat, 20 Aug 2016 14:32:50 +0000 (16:32 +0200)]
Added "yosys-smtbmc -g"