yosys.git
8 years agocleanup in write_smt2 log messages (-bv and -mem are now default)
Clifford Wolf [Sun, 16 Oct 2016 21:02:51 +0000 (23:02 +0200)]
cleanup in write_smt2 log messages (-bv and -mem are now default)

8 years agoBuild fixes for VS 2015
Clifford Wolf [Sun, 16 Oct 2016 18:37:02 +0000 (20:37 +0200)]
Build fixes for VS 2015

8 years agoSome minor build fixes for Visual C
Clifford Wolf [Fri, 14 Oct 2016 16:34:44 +0000 (18:34 +0200)]
Some minor build fixes for Visual C

8 years agoAvoid using strcasecmp()
Clifford Wolf [Fri, 14 Oct 2016 16:20:36 +0000 (18:20 +0200)]
Avoid using strcasecmp()

8 years agoFixed version string for out-of-tree builds
Clifford Wolf [Fri, 14 Oct 2016 15:18:18 +0000 (17:18 +0200)]
Fixed version string for out-of-tree builds

8 years agoAdded notes about some formal features to README
Clifford Wolf [Fri, 14 Oct 2016 13:39:33 +0000 (15:39 +0200)]
Added notes about some formal features to README

8 years agoAdded $anyseq cell type
Clifford Wolf [Fri, 14 Oct 2016 13:24:03 +0000 (15:24 +0200)]
Added $anyseq cell type

8 years agoAdded clk2fflogic
Clifford Wolf [Fri, 14 Oct 2016 12:55:07 +0000 (14:55 +0200)]
Added clk2fflogic

8 years agoAdded opt_rmdff support for $ff cells
Clifford Wolf [Fri, 14 Oct 2016 11:02:36 +0000 (13:02 +0200)]
Added opt_rmdff support for $ff cells

8 years agoAdded $global_clock verilog syntax support for creating $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

8 years agoAdded MEMID handling to "flatten" pass
Clifford Wolf [Fri, 14 Oct 2016 08:36:37 +0000 (10:36 +0200)]
Added MEMID handling to "flatten" pass

8 years agoMerge branch 'master' of github.com:cliffordwolf/yosys
Clifford Wolf [Fri, 14 Oct 2016 07:36:40 +0000 (09:36 +0200)]
Merge branch 'master' of github.com:cliffordwolf/yosys

8 years agoMerge pull request #246 from set-soft/abc_external_ovr
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.

8 years agoAdded YOSYS_VER_STR make variable
Clifford Wolf [Fri, 14 Oct 2016 07:35:18 +0000 (09:35 +0200)]
Added YOSYS_VER_STR make variable

8 years agoUgh! extra patches got here, reverting
Salvador E. Tropea [Thu, 13 Oct 2016 20:57:09 +0000 (17:57 -0300)]
Ugh! extra patches got here, reverting

8 years agoAllow to overwrite ABCEXTERNAL from the environment.
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.

8 years agoModified test target name (to test-all)
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.

8 years agoAdded a new configuration variable GIT_REV_WHERE
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

8 years agoAdded "zinit" pass
Clifford Wolf [Wed, 12 Oct 2016 10:05:19 +0000 (12:05 +0200)]
Added "zinit" pass

8 years agoAdded $ff and $_FF_ cell types
Clifford Wolf [Tue, 11 Oct 2016 23:18:39 +0000 (01:18 +0200)]
Added $ff and $_FF_ cell types

8 years agoFixed "make test" for git head of iverilog
Clifford Wolf [Tue, 11 Oct 2016 10:12:32 +0000 (12:12 +0200)]
Fixed "make test" for git head of iverilog

8 years agodefine PATH_MAX if not defined by limits.h
Clifford Wolf [Tue, 11 Oct 2016 10:12:09 +0000 (12:12 +0200)]
define PATH_MAX if not defined by limits.h

8 years agoMerge branch 'master' of github.com:cliffordwolf/yosys
Clifford Wolf [Tue, 11 Oct 2016 01:58:27 +0000 (03:58 +0200)]
Merge branch 'master' of github.com:cliffordwolf/yosys

8 years agoAdded smtc support for top-level state with [], [N:] syntax
Clifford Wolf [Sat, 8 Oct 2016 10:25:34 +0000 (12:25 +0200)]
Added smtc support for top-level state with [], [N:] syntax

8 years agoBugfix in yosys-smtbmc --noincr
Clifford Wolf [Mon, 3 Oct 2016 22:54:44 +0000 (00:54 +0200)]
Bugfix in yosys-smtbmc --noincr

8 years agoyosys-smtbmc: ABC is a QF_BV solver
Clifford Wolf [Mon, 3 Oct 2016 18:43:38 +0000 (20:43 +0200)]
yosys-smtbmc: ABC is a QF_BV solver

8 years agoAdded "yosys-smtbmc --noincr"
Clifford Wolf [Mon, 3 Oct 2016 18:30:38 +0000 (20:30 +0200)]
Added "yosys-smtbmc --noincr"

8 years agoUpdate ABV to hg rev eb6eca6807cc
Clifford Wolf [Sun, 2 Oct 2016 20:08:53 +0000 (22:08 +0200)]
Update ABV to hg rev eb6eca6807cc

8 years agoyosys-smtbmc: added smtc [...] support for cells
Clifford Wolf [Sun, 2 Oct 2016 20:08:30 +0000 (22:08 +0200)]
yosys-smtbmc: added smtc [...] support for cells

8 years agoAdded "yosys-smtbmc -s abc"
Clifford Wolf [Sat, 1 Oct 2016 11:54:21 +0000 (13:54 +0200)]
Added "yosys-smtbmc -s abc"

8 years agoUpdated ABV to hg rev 6b74de13c57f
Clifford Wolf [Sat, 1 Oct 2016 10:23:24 +0000 (12:23 +0200)]
Updated ABV to hg rev 6b74de13c57f

8 years agoAdded "prep -nokeepdc"
Clifford Wolf [Fri, 30 Sep 2016 15:02:52 +0000 (17:02 +0200)]
Added "prep -nokeepdc"

8 years agoAdded "opt_rmdff -keepdc"
Clifford Wolf [Fri, 30 Sep 2016 15:02:38 +0000 (17:02 +0200)]
Added "opt_rmdff -keepdc"

8 years agoUpdated ABV to hg rev 2bc57cc30593
Clifford Wolf [Fri, 30 Sep 2016 08:56:36 +0000 (10:56 +0200)]
Updated ABV to hg rev 2bc57cc30593

8 years agoMinor improvements in yosys-smtbmc
Clifford Wolf [Sat, 24 Sep 2016 18:40:22 +0000 (20:40 +0200)]
Minor improvements in yosys-smtbmc

8 years agoAdded liberty parser support for types within cell decls
Clifford Wolf [Fri, 23 Sep 2016 11:53:23 +0000 (13:53 +0200)]
Added liberty parser support for types within cell decls

8 years agoMerge branch 'master' of https://github.com/brouhaha/yosys
Clifford Wolf [Fri, 23 Sep 2016 11:42:08 +0000 (13:42 +0200)]
Merge branch 'master' of https://github.com/brouhaha/yosys

8 years agoAdd optional SEED=n command line option to Makefile, and -S n command line option...
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.

8 years agoAdded autotest.sh -I
Clifford Wolf [Tue, 20 Sep 2016 07:29:56 +0000 (09:29 +0200)]
Added autotest.sh -I

8 years agoCosmetic fix in test_autotb.cc
Clifford Wolf [Mon, 19 Sep 2016 18:43:43 +0000 (20:43 +0200)]
Cosmetic fix in test_autotb.cc

8 years agoAdded yosys-smtbmc --noinfo and --dummy
Clifford Wolf [Mon, 19 Sep 2016 18:43:28 +0000 (20:43 +0200)]
Added yosys-smtbmc --noinfo and --dummy

8 years agoAvoid creating very long strings in test_autotb
Clifford Wolf [Mon, 19 Sep 2016 08:20:20 +0000 (10:20 +0200)]
Avoid creating very long strings in test_autotb

8 years agoAdded $past, $stable, $rose, $fell SVA functions
Clifford Wolf [Sun, 18 Sep 2016 23:30:07 +0000 (01:30 +0200)]
Added $past, $stable, $rose, $fell SVA functions

8 years agoImproved handling of SMT2 logics in yosys-smtbmc
Clifford Wolf [Sun, 18 Sep 2016 18:48:09 +0000 (20:48 +0200)]
Improved handling of SMT2 logics in yosys-smtbmc

8 years agoAdded support for bus interfaces to "read_liberty -lib"
Clifford Wolf [Sun, 18 Sep 2016 16:48:59 +0000 (18:48 +0200)]
Added support for bus interfaces to "read_liberty -lib"

8 years agoMerge branch 'master' of github.com:cliffordwolf/yosys
Clifford Wolf [Sat, 17 Sep 2016 22:50:02 +0000 (00:50 +0200)]
Merge branch 'master' of github.com:cliffordwolf/yosys

8 years agoyosys-smtbmc: added -i support smtc files
Clifford Wolf [Sat, 17 Sep 2016 22:48:36 +0000 (00:48 +0200)]
yosys-smtbmc: added -i support smtc files

8 years agoBugfix in techmap parameter handling
Clifford Wolf [Wed, 14 Sep 2016 18:46:54 +0000 (20:46 +0200)]
Bugfix in techmap parameter handling

8 years agoWork-around for boolector bug
Clifford Wolf [Tue, 13 Sep 2016 11:23:06 +0000 (13:23 +0200)]
Work-around for boolector bug

8 years agoMerge pull request #228 from Kmanfi/test
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.

8 years agoFix for modules with big interfaces.
Kaj Tuomi [Tue, 13 Sep 2016 10:13:27 +0000 (13:13 +0300)]
Fix for modules with big interfaces.

8 years agoAdded missing :produce-models setting to smtio.py
Clifford Wolf [Sun, 11 Sep 2016 16:08:56 +0000 (18:08 +0200)]
Added missing :produce-models setting to smtio.py

8 years agoMinor improvements to smtio.py vcd writer
Clifford Wolf [Sat, 10 Sep 2016 14:24:08 +0000 (16:24 +0200)]
Minor improvements to smtio.py vcd writer

8 years agofixed write_smt2 for (non-combinatorial) loops through hierarchical cells
Clifford Wolf [Sat, 10 Sep 2016 13:14:41 +0000 (15:14 +0200)]
fixed write_smt2 for (non-combinatorial) loops through hierarchical cells

8 years agosmt2 mem init bugfix
Clifford Wolf [Thu, 8 Sep 2016 16:08:15 +0000 (18:08 +0200)]
smt2 mem init bugfix

8 years agoMerge branch 'master' of github.com:cliffordwolf/yosys
Clifford Wolf [Thu, 8 Sep 2016 09:17:05 +0000 (11:17 +0200)]
Merge branch 'master' of github.com:cliffordwolf/yosys

8 years agoyosys-smtbmc meminit support
Clifford Wolf [Thu, 8 Sep 2016 09:16:12 +0000 (11:16 +0200)]
yosys-smtbmc meminit support

8 years agoMerge pull request #225 from Kmanfi/test
Clifford Wolf [Thu, 8 Sep 2016 08:06:40 +0000 (10:06 +0200)]
Merge pull request #225 from Kmanfi/test

Typo fix.

8 years agoTypo fix.
Kaj Tuomi [Thu, 8 Sep 2016 07:57:16 +0000 (10:57 +0300)]
Typo fix.

8 years agoBugfix in "yosys-smtbmc --unroll"
Clifford Wolf [Wed, 7 Sep 2016 19:01:51 +0000 (21:01 +0200)]
Bugfix in "yosys-smtbmc --unroll"

8 years agoAdded "yosys-smtbmc --unroll"
Clifford Wolf [Wed, 7 Sep 2016 18:57:56 +0000 (20:57 +0200)]
Added "yosys-smtbmc --unroll"

8 years agoInstall celledges.h
Clifford Wolf [Wed, 7 Sep 2016 11:43:57 +0000 (13:43 +0200)]
Install celledges.h

8 years agoImprovements in assertpmux
Clifford Wolf [Wed, 7 Sep 2016 10:42:16 +0000 (12:42 +0200)]
Improvements in assertpmux

8 years agoUpdated ABC to hg 8e08604f8ad3
Clifford Wolf [Wed, 7 Sep 2016 09:08:54 +0000 (11:08 +0200)]
Updated ABC to hg 8e08604f8ad3

8 years agoAdded assertpmux
Clifford Wolf [Tue, 6 Sep 2016 22:28:01 +0000 (00:28 +0200)]
Added assertpmux

8 years agoAdded "tee +INT -INT"
Clifford Wolf [Tue, 6 Sep 2016 15:43:24 +0000 (17:43 +0200)]
Added "tee +INT -INT"

8 years agoRun log_flush() before solving in sat command
Clifford Wolf [Tue, 6 Sep 2016 15:35:25 +0000 (17:35 +0200)]
Run log_flush() before solving in sat command

8 years agoBugfix in parsing of BLIF latch init values
Clifford Wolf [Tue, 6 Sep 2016 15:35:06 +0000 (17:35 +0200)]
Bugfix in parsing of BLIF latch init values

8 years agoAvoid creation of bogus initial blocks for assert/assume in always @*
Clifford Wolf [Tue, 6 Sep 2016 15:34:42 +0000 (17:34 +0200)]
Avoid creation of bogus initial blocks for assert/assume in always @*

8 years agoFix spelling and grammar in README
Larry Doolittle [Tue, 6 Sep 2016 02:58:18 +0000 (19:58 -0700)]
Fix spelling and grammar in README

8 years agoyosys-smtbmc: flush stdout after each log msg
Clifford Wolf [Mon, 5 Sep 2016 23:40:31 +0000 (01:40 +0200)]
yosys-smtbmc: flush stdout after each log msg

8 years agoMinor bugfix in write_smt2
Clifford Wolf [Sun, 4 Sep 2016 14:32:47 +0000 (16:32 +0200)]
Minor bugfix in write_smt2

8 years agoMinor README updates
Clifford Wolf [Sat, 3 Sep 2016 16:49:53 +0000 (18:49 +0200)]
Minor README updates

8 years agoAdded boolector support to yosys-smtbmc
Clifford Wolf [Sat, 3 Sep 2016 12:26:00 +0000 (14:26 +0200)]
Added boolector support to yosys-smtbmc

8 years agoMerge branch 'smtbmc-kmanfi'
Clifford Wolf [Fri, 2 Sep 2016 11:55:51 +0000 (13:55 +0200)]
Merge branch 'smtbmc-kmanfi'

8 years agoMade examples/smtbmc/demo1.v more interesting
Clifford Wolf [Fri, 2 Sep 2016 11:54:24 +0000 (13:54 +0200)]
Made examples/smtbmc/demo1.v more interesting

8 years agoDon't re-create hex_dict for each value
Clifford Wolf [Fri, 2 Sep 2016 11:46:56 +0000 (13:46 +0200)]
Don't re-create hex_dict for each value

8 years agoMore PEP 8 fixes.
Kaj Tuomi [Fri, 2 Sep 2016 10:09:09 +0000 (13:09 +0300)]
More PEP 8 fixes.

8 years agoIndentation and PEP 8 fixes. CamelCase and white space after semicolon.
Kaj Tuomi [Fri, 2 Sep 2016 10:01:31 +0000 (13:01 +0300)]
Indentation and PEP 8 fixes. CamelCase and white space after semicolon.

8 years agoUse dict lookup instead of many ifs.
Kaj Tuomi [Fri, 2 Sep 2016 09:50:23 +0000 (12:50 +0300)]
Use dict lookup instead of many ifs.

8 years agoFix: Unresolved reference.
Kaj Tuomi [Fri, 2 Sep 2016 08:12:30 +0000 (11:12 +0300)]
Fix: Unresolved reference.

8 years agoSome syntax fixes. Generator and comma separated list modifications.
Kaj Tuomi [Fri, 2 Sep 2016 08:02:19 +0000 (11:02 +0300)]
Some syntax fixes. Generator and comma separated list modifications.

8 years agoAdded "prep -nomem"
Clifford Wolf [Tue, 30 Aug 2016 21:57:24 +0000 (23:57 +0200)]
Added "prep -nomem"

8 years agoAdded $anyconst support to yosys-smtbmc
Clifford Wolf [Tue, 30 Aug 2016 17:27:42 +0000 (19:27 +0200)]
Added $anyconst support to yosys-smtbmc

8 years agoRemoved $aconst cell type
Clifford Wolf [Tue, 30 Aug 2016 17:09:56 +0000 (19:09 +0200)]
Removed $aconst cell type

8 years agoFixed memory bug in write_smt2
Clifford Wolf [Tue, 30 Aug 2016 12:49:47 +0000 (14:49 +0200)]
Fixed memory bug in write_smt2

8 years agoMade "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem"
Clifford Wolf [Tue, 30 Aug 2016 10:40:09 +0000 (12:40 +0200)]
Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem"

8 years agoAdded $anyconst support to smt2 back-end
Clifford Wolf [Tue, 30 Aug 2016 09:26:10 +0000 (11:26 +0200)]
Added $anyconst support to smt2 back-end

8 years agoImproved init spec handling in opt_rmdff, modernized the code a bit
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

8 years agoAdded "yosys-smtbmc --dump-all"
Clifford Wolf [Mon, 29 Aug 2016 20:41:45 +0000 (22:41 +0200)]
Added "yosys-smtbmc --dump-all"

8 years agoMore yosys-smtbmc bugfixes
Clifford Wolf [Mon, 29 Aug 2016 12:53:32 +0000 (14:53 +0200)]
More yosys-smtbmc bugfixes

8 years agoVarious fixes and improvements in yosys-smtbmc
Clifford Wolf [Mon, 29 Aug 2016 11:53:12 +0000 (13:53 +0200)]
Various fixes and improvements in yosys-smtbmc

8 years agoRemoved $predict again
Clifford Wolf [Sun, 28 Aug 2016 19:35:33 +0000 (21:35 +0200)]
Removed $predict again

8 years agoImproved "show" help message
Clifford Wolf [Sun, 28 Aug 2016 10:34:36 +0000 (12:34 +0200)]
Improved "show" help message

8 years agoSome changes to yosys-smtbmc cmd line options, add --final-only
Clifford Wolf [Sat, 27 Aug 2016 20:04:15 +0000 (22:04 +0200)]
Some changes to yosys-smtbmc cmd line options, add --final-only

8 years agoFixed handling of transparent bram rd ports on ROMs
Clifford Wolf [Sat, 27 Aug 2016 15:06:22 +0000 (17:06 +0200)]
Fixed handling of transparent bram rd ports on ROMs

8 years agoAdded smtc "final" statement
Clifford Wolf [Sat, 27 Aug 2016 12:30:36 +0000 (14:30 +0200)]
Added smtc "final" statement

8 years agoMerge branch 'master' of github.com:cliffordwolf/yosys
Clifford Wolf [Fri, 26 Aug 2016 21:36:15 +0000 (23:36 +0200)]
Merge branch 'master' of github.com:cliffordwolf/yosys

8 years agoMerge pull request #215 from frznchckn/to_upstream
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

8 years agoAdded read_verilog -norestrict -assume-asserts
Clifford Wolf [Fri, 26 Aug 2016 21:35:27 +0000 (23:35 +0200)]
Added read_verilog -norestrict -assume-asserts