yosys.git
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

8 years agoRelax test to see if yosys dir is a git repository in Makefile
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

8 years agoAllow redefining of the ABC repository URL
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

8 years agoVarious fixes and improvements in smt2 back-end
Clifford Wolf [Fri, 26 Aug 2016 15:33:02 +0000 (17:33 +0200)]
Various fixes and improvements in smt2 back-end

8 years agoImproved verilog parser errors
Clifford Wolf [Thu, 25 Aug 2016 09:44:25 +0000 (11:44 +0200)]
Improved verilog parser errors

8 years agoMore yosys-smtbmc smtc features
Clifford Wolf [Wed, 24 Aug 2016 21:18:29 +0000 (23:18 +0200)]
More yosys-smtbmc smtc features

8 years agoyosys-smtbmc --smtc -g
Clifford Wolf [Wed, 24 Aug 2016 20:09:50 +0000 (22:09 +0200)]
yosys-smtbmc --smtc -g

8 years agoAdded SV "restrict" keyword
Clifford Wolf [Wed, 24 Aug 2016 13:30:08 +0000 (15:30 +0200)]
Added SV "restrict" keyword

8 years agoMinor yosys-smtbmc bugfix
Clifford Wolf [Mon, 22 Aug 2016 15:45:01 +0000 (17:45 +0200)]
Minor yosys-smtbmc bugfix

8 years agoAdded "yosys-smtbmc --constr"
Clifford Wolf [Mon, 22 Aug 2016 15:27:43 +0000 (17:27 +0200)]
Added "yosys-smtbmc --constr"

8 years agoAdded "yosys-smtbmc --dump-constr"
Clifford Wolf [Mon, 22 Aug 2016 14:48:46 +0000 (16:48 +0200)]
Added "yosys-smtbmc --dump-constr"

8 years agoAdded glob support to all front-ends
Clifford Wolf [Mon, 22 Aug 2016 13:05:57 +0000 (15:05 +0200)]
Added glob support to all front-ends

8 years agoFixed bug with memories that do not have a down-to-zero data width
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

8 years agoFixed bug in memory_share for memory ports with different ABITS
Clifford Wolf [Mon, 22 Aug 2016 12:26:33 +0000 (14:26 +0200)]
Fixed bug in memory_share for memory ports with different ABITS

8 years agoyosys-smtbmc: improved --dump-vlogtb handling of memories
Clifford Wolf [Sun, 21 Aug 2016 13:56:22 +0000 (15:56 +0200)]
yosys-smtbmc: improved --dump-vlogtb handling of memories

8 years agoAdded another mem2reg test case
Clifford Wolf [Sun, 21 Aug 2016 11:45:46 +0000 (13:45 +0200)]
Added another mem2reg test case

8 years agoAnother bugfix in mem2reg code
Clifford Wolf [Sun, 21 Aug 2016 11:23:58 +0000 (13:23 +0200)]
Another bugfix in mem2reg code

8 years agoMinor improvements to AstNode::dumpAst() and AstNode::dumpVlog()
Clifford Wolf [Sun, 21 Aug 2016 11:18:09 +0000 (13:18 +0200)]
Minor improvements to AstNode::dumpAst() and AstNode::dumpVlog()

8 years agoAdded examples/smtbmc/demo2.v
Clifford Wolf [Sat, 20 Aug 2016 16:44:27 +0000 (18:44 +0200)]
Added examples/smtbmc/demo2.v

8 years agoAdded "yosys-smtbmc --dump-vlogtb"
Clifford Wolf [Sat, 20 Aug 2016 16:43:39 +0000 (18:43 +0200)]
Added "yosys-smtbmc --dump-vlogtb"

8 years agoAdded support for memories to smtio.py
Clifford Wolf [Sat, 20 Aug 2016 16:42:32 +0000 (18:42 +0200)]
Added support for memories to smtio.py

8 years agoDeprecated "write_smt2 -regs" (by default on now), and some other smt2 back-end impro...
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

8 years agoAdded "yosys-smtbmc -g"
Clifford Wolf [Sat, 20 Aug 2016 14:32:50 +0000 (16:32 +0200)]
Added "yosys-smtbmc -g"

8 years agoAdded smtbmc longopt support
Clifford Wolf [Sat, 20 Aug 2016 14:07:59 +0000 (16:07 +0200)]
Added smtbmc longopt support

8 years agoFixed finish_addr handling in $readmemh/$readmemb
Clifford Wolf [Sat, 20 Aug 2016 11:47:46 +0000 (13:47 +0200)]
Fixed finish_addr handling in $readmemh/$readmemb

8 years agoBugfix in partial mem write handling in verilog back-end
Clifford Wolf [Sat, 20 Aug 2016 11:06:06 +0000 (13:06 +0200)]
Bugfix in partial mem write handling in verilog back-end

8 years agoAdded "wreduce -memx"
Clifford Wolf [Sat, 20 Aug 2016 10:52:50 +0000 (12:52 +0200)]
Added "wreduce -memx"

8 years agoAdded memory_memx pass, "memory -memx", and "prep -memx"
Clifford Wolf [Fri, 19 Aug 2016 17:48:26 +0000 (19:48 +0200)]
Added memory_memx pass, "memory -memx", and "prep -memx"

8 years agoOptimize memory address port width in wreduce and memory_collect, not verilog front-end
Clifford Wolf [Fri, 19 Aug 2016 16:38:25 +0000 (18:38 +0200)]
Optimize memory address port width in wreduce and memory_collect, not verilog front-end

8 years agoAdded missing support for mem read enable ports to verilog back-end
Clifford Wolf [Thu, 18 Aug 2016 19:47:02 +0000 (21:47 +0200)]
Added missing support for mem read enable ports to verilog back-end

8 years agoBugfix in test_autotb
Clifford Wolf [Thu, 18 Aug 2016 11:43:12 +0000 (13:43 +0200)]
Bugfix in test_autotb

8 years agoImproved smtbmc vcd generation performance
Clifford Wolf [Thu, 18 Aug 2016 09:17:45 +0000 (11:17 +0200)]
Improved smtbmc vcd generation performance

8 years agoAdded printing of code loc of failed asserts to yosys-smtbmc
Clifford Wolf [Wed, 17 Aug 2016 18:10:02 +0000 (20:10 +0200)]
Added printing of code loc of failed asserts to yosys-smtbmc

8 years agoFixed default build config
Clifford Wolf [Tue, 16 Aug 2016 20:44:38 +0000 (22:44 +0200)]
Fixed default build config

8 years agoMerge pull request #203 from cr1901/master
Clifford Wolf [Tue, 16 Aug 2016 20:41:53 +0000 (22:41 +0200)]
Merge pull request #203 from cr1901/master

Add MSYS2-compatible build.