Clifford Wolf
97583ab729
Avoid creation of bogus initial blocks for assert/assume in always @*
2016-09-06 17:34:42 +02:00
Larry Doolittle
dcb5a6ea8a
Fix spelling and grammar in README
2016-09-06 11:25:33 +02:00
Clifford Wolf
97b449fe55
yosys-smtbmc: flush stdout after each log msg
2016-09-06 01:40:31 +02:00
Clifford Wolf
372d672c2a
Minor bugfix in write_smt2
2016-09-04 16:32:47 +02:00
Clifford Wolf
19a3b3732c
Minor README updates
2016-09-03 18:49:53 +02:00
Clifford Wolf
fa5565b606
Added boolector support to yosys-smtbmc
2016-09-03 14:26:00 +02:00
Clifford Wolf
d2eba7631f
Merge branch 'smtbmc-kmanfi'
2016-09-02 13:55:51 +02:00
Clifford Wolf
068d5bc02f
Made examples/smtbmc/demo1.v more interesting
2016-09-02 13:54:24 +02:00
Clifford Wolf
948aac9e1e
Don't re-create hex_dict for each value
2016-09-02 13:46:56 +02:00
Kaj Tuomi
d88cd0ae7f
More PEP 8 fixes.
2016-09-02 13:09:09 +03:00
Kaj Tuomi
c4ba1965fd
Indentation and PEP 8 fixes. CamelCase and white space after semicolon.
2016-09-02 13:01:31 +03:00
Kaj Tuomi
2343dda946
Use dict lookup instead of many ifs.
2016-09-02 12:50:23 +03:00
Kaj Tuomi
279298c0b8
Fix: Unresolved reference.
2016-09-02 11:12:30 +03:00
Kaj Tuomi
74dd36ad55
Some syntax fixes. Generator and comma separated list modifications.
2016-09-02 11:02:19 +03:00
Clifford Wolf
2ee9bf10d0
Added "prep -nomem"
2016-08-30 23:57:24 +02:00
Clifford Wolf
aa25a4cec6
Added $anyconst support to yosys-smtbmc
2016-08-30 19:27:42 +02:00
Clifford Wolf
6f41e5277d
Removed $aconst cell type
2016-08-30 19:09:56 +02:00
Clifford Wolf
a8124c137e
Fixed memory bug in write_smt2
2016-08-30 14:49:47 +02:00
Clifford Wolf
b04a40d9fe
Made "write_smt2 -bv -mem" default, added "write_smt2 -nobv -nomem"
2016-08-30 12:40:09 +02:00
Clifford Wolf
39e4faa2e4
Added $anyconst support to smt2 back-end
2016-08-30 11:26:10 +02:00
Clifford Wolf
4ea7054b56
Improved init spec handling in opt_rmdff, modernized the code a bit
2016-08-30 01:34:04 +02:00
Clifford Wolf
c417421495
Added "yosys-smtbmc --dump-all"
2016-08-29 22:41:45 +02:00
Clifford Wolf
b226893461
More yosys-smtbmc bugfixes
2016-08-29 14:53:32 +02:00
Clifford Wolf
a2e2fc5980
Various fixes and improvements in yosys-smtbmc
2016-08-29 13:53:12 +02:00
Clifford Wolf
eae390ae17
Removed $predict again
2016-08-28 21:35:33 +02:00
Clifford Wolf
66582964bc
Improved "show" help message
2016-08-28 12:34:36 +02:00
Clifford Wolf
f56dba8e20
Some changes to yosys-smtbmc cmd line options, add --final-only
2016-08-27 22:04:15 +02:00
Clifford Wolf
23afeadb5e
Fixed handling of transparent bram rd ports on ROMs
2016-08-27 17:06:22 +02:00
Clifford Wolf
adcda6817e
Added smtc "final" statement
2016-08-27 14:30:36 +02:00
Clifford Wolf
7500b403de
Merge branch 'master' of github.com:cliffordwolf/yosys
2016-08-26 23:36:15 +02:00
Clifford Wolf
3356d3947b
Merge pull request #215 from frznchckn/to_upstream
...
Add some useful flexibility to build process
2016-08-26 23:36:05 +02:00
Clifford Wolf
1276c87a56
Added read_verilog -norestrict -assume-asserts
2016-08-26 23:35:27 +02:00
Russell L Friesenhahn
ee620c6a24
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
2016-08-26 11:15:36 -05:00
Russell L Friesenhahn
23f217b166
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
2016-08-26 11:14:24 -05:00
Clifford Wolf
17233b11e1
Various fixes and improvements in smt2 back-end
2016-08-26 17:33:02 +02:00
Clifford Wolf
4be4969bae
Improved verilog parser errors
2016-08-25 11:44:37 +02:00
Clifford Wolf
ad56ad44c3
More yosys-smtbmc smtc features
2016-08-24 23:18:29 +02:00
Clifford Wolf
ee3e7a0e45
yosys-smtbmc --smtc -g
2016-08-24 22:09:50 +02:00
Clifford Wolf
cd18235f30
Added SV "restrict" keyword
2016-08-24 15:30:08 +02:00
Clifford Wolf
6523023645
Minor yosys-smtbmc bugfix
2016-08-22 17:45:01 +02:00
Clifford Wolf
583ceee6eb
Added "yosys-smtbmc --constr"
2016-08-22 17:27:43 +02:00
Clifford Wolf
2bd30e2026
Added "yosys-smtbmc --dump-constr"
2016-08-22 16:48:46 +02:00
Clifford Wolf
f8a77abfac
Added glob support to all front-ends
2016-08-22 15:05:57 +02:00
Clifford Wolf
450f6f59b4
Fixed bug with memories that do not have a down-to-zero data width
2016-08-22 14:27:46 +02:00
Clifford Wolf
cad40fc874
Fixed bug in memory_share for memory ports with different ABITS
2016-08-22 14:26:33 +02:00
Clifford Wolf
7a33b9892a
yosys-smtbmc: improved --dump-vlogtb handling of memories
2016-08-21 15:56:22 +02:00
Clifford Wolf
cdd0b85e47
Added another mem2reg test case
2016-08-21 13:45:46 +02:00
Clifford Wolf
82a4a0230f
Another bugfix in mem2reg code
2016-08-21 13:23:58 +02:00
Clifford Wolf
dbdd8927e7
Minor improvements to AstNode::dumpAst() and AstNode::dumpVlog()
2016-08-21 13:18:09 +02:00
Clifford Wolf
a93fcec93f
Added examples/smtbmc/demo2.v
2016-08-20 18:44:27 +02:00