Clifford Wolf
1d1f56a361
Add PSL parser mode to verific front-end
2017-02-08 10:40:33 +01:00
Steffen Vogel
b8d531957d
Added notes for compilation on OS X
2017-02-07 11:16:56 -03:00
Steffen Vogel
7e08e37961
Fix compilation on OS X in order to support both MacPorts and Homebrew
2017-02-07 11:16:56 -03:00
Steffen Vogel
19f36271c2
Allow standard tools to be overwritten in make invocation
2017-02-07 11:09:15 -03:00
Clifford Wolf
7e0b776a79
Add "read_blif -wideports"
2017-02-06 14:48:03 +01:00
Clifford Wolf
aab58045a8
Fix undef propagation bug in $pmux SAT model
2017-02-05 22:43:33 +01:00
Clifford Wolf
19303f6392
Update ABC to hg rev a2fcd1cc61a6
2017-02-05 20:04:17 +01:00
Clifford Wolf
1064c8f61f
Merge pull request #304 from esden/gsed-darwin
...
Use gsed vs sed on Darwin.
2017-02-05 12:00:21 +01:00
Piotr Esden-Tempski
e3a12b57f5
Use -E sed parameter instead of -r.
...
BSD sed equivalent to -r parameter is -E and it is also supported in GNU
sed thus using -E results in support on both platforms.
2017-02-04 18:26:01 -08:00
Clifford Wolf
5541b42159
Add assert check in "yosys-smtbmc -c"
2017-02-04 21:22:17 +01:00
Clifford Wolf
adbecfee66
Improve yosys-smtbmc cover() support
2017-02-04 21:10:24 +01:00
Clifford Wolf
0c0784b6bf
Partially implement cover() support in yosys-smtbmc
2017-02-04 18:17:08 +01:00
Clifford Wolf
6abf79eb28
Further improve cover() support
2017-02-04 17:02:13 +01:00
Clifford Wolf
3928482a3c
Add $cover cell type and SVA cover() support
2017-02-04 14:14:26 +01:00
Clifford Wolf
911c44d164
Add assert/assume support to verific front-end
2017-02-04 13:36:00 +01:00
Clifford Wolf
249ddbc16c
Update ABC to hg rev fe96921e5d50
2017-02-01 11:15:37 +01:00
Clifford Wolf
8927e19b13
Update ABC scripts to use "&nf" instead of "map"
2017-02-01 11:15:20 +01:00
Clifford Wolf
c17aab2957
Merge branch 'C-Elegans-opt_compare_pr'
2017-01-31 16:21:23 +01:00
Clifford Wolf
ffbe8d41f3
Fix indenting and log messages in code merged from opt_compare_pr
2017-01-31 16:20:56 +01:00
Clifford Wolf
19a980277f
Merge branch 'opt_compare_pr' of https://github.com/C-Elegans/yosys into C-Elegans-opt_compare_pr
2017-01-31 15:54:41 +01:00
Steffen Vogel
44b47b57e3
use Homebrew only if installed
2017-01-31 10:06:06 -03:00
Clifford Wolf
7481ba4750
Improve opt_rmdff support for $dlatch cells
2017-01-31 10:15:04 +01:00
C-Elegans
a94c3694d7
Refactor and generalize the comparision optimization
...
Generalizes the optimization to:
a < C,
a >= C,
C > a,
C <= a
2017-01-30 17:52:16 -05:00
Clifford Wolf
18ea65ef04
Add "yosys-smtbmc --aig <aim_filename>:<aiw_filename>" support
2017-01-30 11:38:43 +01:00
Clifford Wolf
fe29869ec5
Add $ff and $_FF_ support to equiv_simple
2017-01-30 10:50:38 +01:00
Clifford Wolf
e54c355b41
Add "yosys-smtbmc --aig-noheader" and AIGER mem init support
2017-01-28 15:15:02 +01:00
Clifford Wolf
45e10c1c89
Be more conservative with merging large cells into FSMs
2017-01-26 09:19:28 +01:00
Clifford Wolf
49b8160488
Add warnings for quickly growing FSM table size in fsm_expand
2017-01-26 09:05:59 +01:00
Clifford Wolf
b0a430f601
Merge branch 'master' of github.com:cliffordwolf/yosys
2017-01-26 08:59:26 +01:00
Clifford Wolf
b54972c112
Fix RTLIL::Memory::start_offset initialization
2017-01-25 17:00:59 +01:00
C-Elegans
2fa0fd4a37
Do not use b.as_int() in calculation of bit set
2017-01-21 12:58:26 -05:00
Clifford Wolf
fea528280b
Add "enum" and "typedef" lexer support
2017-01-17 17:33:52 +01:00
C-Elegans
84f9cd0025
Optimize compares to powers of 2
...
Remove opt_compare and put comparison pass in opt_expr
assuming a [7:0] is unsigned
a >= (1<<x) becomes |a[7:x]
a < (1<<x) becomes !a[7:x]
Additionally:
a >= 0 becomes constant true,
a < 0 becomes constant false
delete opt_compare.cc
revert opt.cc to commit b7cfb7dbd
(remove opt_compare step)
2017-01-16 13:45:50 -05:00
Clifford Wolf
87fe8ab3f2
Merge pull request #293 from thoughtpolice/minor-cleanup
...
Delete some dead code in the Hierarchy pass
2017-01-16 10:25:25 +01:00
Austin Seipp
6781543244
passes/hierarchy: delete some dead code
...
Signed-off-by: Austin Seipp <aseipp@pobox.com>
2017-01-15 16:39:12 -06:00
C-Elegans
943389cdd5
Fix issue #269 , optimize signed compare with 0
...
add opt_compare pass and add it to opt
for a < 0:
if a is signed, replace with a[max_bit-1]
for a >= 0:
if a is signed, replace with ~a[max_bit-1]
2017-01-15 13:38:29 -05:00
Andrew Zonenberg
0c83a30f95
Merge https://github.com/cliffordwolf/yosys
2017-01-15 09:43:15 -08:00
Clifford Wolf
78f65f89ff
Fix bug in AstNode::mem2reg_as_needed_pass2()
2017-01-15 13:52:50 +01:00
Clifford Wolf
b7cfb7dbd2
Fix $initstate handling bug in yosys-smtbmc
2017-01-11 14:14:12 +01:00
Clifford Wolf
8953a55cd8
Update ABC to hg id f8cadfe3861f
2017-01-11 10:56:27 +01:00
Clifford Wolf
8012de40b9
Updated ABC to hg id 38b26a543f1d
2017-01-08 11:57:52 +01:00
Andrew Zonenberg
ac90de73be
Merge https://github.com/cliffordwolf/yosys
2017-01-05 06:05:58 -08:00
Clifford Wolf
2d32c6c4f6
Fixed handling of local memories in functions
2017-01-05 13:19:03 +01:00
Clifford Wolf
0cac95ea94
Added "check -initdrv"
2017-01-04 18:12:41 +01:00
Clifford Wolf
81a9ee2360
Added handling of local memories and error for local decls in unnamed blocks
2017-01-04 16:03:04 +01:00
Clifford Wolf
b9ad91b93e
Implicitly set "yosys-smtbmc --noprogress" on windows
2017-01-04 15:23:48 +01:00
Clifford Wolf
080004b19a
Fixed typo in tests/simple/arraycells.v
2017-01-04 12:39:01 +01:00
Clifford Wolf
ed812ea39c
Fixed "yosys-smtbmc --noprogress"
2017-01-04 12:03:04 +01:00
Clifford Wolf
dfb461fe52
Added Verilog $rtoi and $itor support
2017-01-03 17:40:58 +01:00
Clifford Wolf
81bb952e5d
Handle "always 1" like "always -1" in .smtc files
2017-01-02 20:08:03 +01:00