Clifford Wolf
|
b9ad91b93e
|
Implicitly set "yosys-smtbmc --noprogress" on windows
|
2017-01-04 15:23:48 +01:00 |
Clifford Wolf
|
ed812ea39c
|
Fixed "yosys-smtbmc --noprogress"
|
2017-01-04 12:03:04 +01:00 |
Clifford Wolf
|
81bb952e5d
|
Handle "always 1" like "always -1" in .smtc files
|
2017-01-02 20:08:03 +01:00 |
Clifford Wolf
|
2198948398
|
Improved write_json help message
|
2016-12-29 12:13:29 +01:00 |
Clifford Wolf
|
a61c88f122
|
Added $anyconst support to AIGER back-end
|
2016-12-11 13:48:18 +01:00 |
Clifford Wolf
|
a44cc7a3d1
|
Added $assert/$assume support to AIGER back-end
|
2016-12-03 13:20:29 +01:00 |
Clifford Wolf
|
37760541bd
|
Improved yosys-smtbmc default -t/--assume-skipped for --cex and --aig
|
2016-12-03 12:37:20 +01:00 |
Clifford Wolf
|
88b9733253
|
Added "yosys-smtbmc --aig"
|
2016-12-01 13:16:57 +01:00 |
Clifford Wolf
|
52c243cf05
|
Added support for partially initialized regs to smt2 back-end
|
2016-12-01 12:00:00 +01:00 |
Clifford Wolf
|
5fa1fa1e6f
|
Added "write_aiger -zinit -symbols -vmap"
|
2016-12-01 11:04:36 +01:00 |
Clifford Wolf
|
c1f762ca56
|
Added "write_aiger" command
|
2016-11-30 21:30:24 +01:00 |
Clifford Wolf
|
df2e5aad6f
|
Bugfix in smt2 back-end for pure checker modules
|
2016-11-28 15:15:09 +01:00 |
Clifford Wolf
|
c17d98f55c
|
Removed shebang line from smtio.py, fixes #279
|
2016-11-27 12:11:04 +01:00 |
Clifford Wolf
|
5c2c78e2dd
|
Added wire start_offset and upto handling BLIF back-end
|
2016-11-23 13:54:33 +01:00 |
Clifford Wolf
|
f257ccf22e
|
Added "yosys-smtbmc --append"
|
2016-11-22 21:21:13 +01:00 |
Adam Izraelevitz
|
f77dc3bacc
|
Bugfix: include assign to write-mask
|
2016-11-18 11:49:26 -08:00 |
Clifford Wolf
|
e01382739d
|
More progress in FIRRTL back-end
|
2016-11-18 02:41:29 +01:00 |
Clifford Wolf
|
c051115e03
|
Progress in FIRRTL back-end
|
2016-11-18 00:32:35 +01:00 |
Clifford Wolf
|
57966a619f
|
Added first draft of FIRRTL back-end
|
2016-11-17 23:36:47 +01:00 |
Clifford Wolf
|
ce132cf652
|
Cleanups and fixed in write_verilog regarding reg init
|
2016-11-16 12:00:39 +01:00 |
Clifford Wolf
|
3db2ac4e00
|
Added hex constant support to write_verilog
|
2016-11-03 12:13:23 +01:00 |
Clifford Wolf
|
caa2fc62ef
|
Adde "write_verilog -renameprefix -v"
|
2016-11-01 11:30:27 +01:00 |
Clifford Wolf
|
aa72262330
|
Added avail params to ilang format, check module params in 'hierarchy -check'
|
2016-10-22 11:05:49 +02:00 |
Clifford Wolf
|
281a977b39
|
Ignore L_pi nets in "yosys-smtbmc --cex"
|
2016-10-18 10:54:53 +02:00 |
Clifford Wolf
|
9e980a2bb0
|
Use init value "2" for all uninitialized FFs in BLIF back-end
|
2016-10-18 10:54:04 +02:00 |
Clifford Wolf
|
0bcc617a4f
|
Added "yosys-smtbmc --cex <filename>"
|
2016-10-17 14:57:28 +02:00 |
Clifford Wolf
|
189fbd4cf8
|
cleanup in write_smt2 log messages (-bv and -mem are now default)
|
2016-10-16 23:02:51 +02:00 |
Clifford Wolf
|
bdc316db50
|
Added $anyseq cell type
|
2016-10-14 15:24:03 +02:00 |
Clifford Wolf
|
53655d173b
|
Added $global_clock verilog syntax support for creating $ff cells
|
2016-10-14 12:33:56 +02:00 |
Clifford Wolf
|
8ebba8a35f
|
Added $ff and $_FF_ cell types
|
2016-10-12 01:18:39 +02:00 |
Clifford Wolf
|
11130d581d
|
Merge branch 'master' of github.com:cliffordwolf/yosys
|
2016-10-11 03:58:27 +02:00 |
Clifford Wolf
|
5f6a838823
|
Added smtc support for top-level state with [], [N:] syntax
|
2016-10-08 12:25:34 +02:00 |
Clifford Wolf
|
5f7c5e685b
|
Bugfix in yosys-smtbmc --noincr
|
2016-10-04 00:54:44 +02:00 |
Clifford Wolf
|
1114ce9210
|
yosys-smtbmc: ABC is a QF_BV solver
|
2016-10-03 20:43:38 +02:00 |
Clifford Wolf
|
99b2093bc4
|
Added "yosys-smtbmc --noincr"
|
2016-10-03 20:30:38 +02:00 |
Clifford Wolf
|
9aec8a1672
|
yosys-smtbmc: added smtc [...] support for cells
|
2016-10-02 22:08:30 +02:00 |
Clifford Wolf
|
4eb0d6fc0e
|
Added "yosys-smtbmc -s abc"
|
2016-10-01 13:54:21 +02:00 |
Clifford Wolf
|
34e2fb594d
|
Minor improvements in yosys-smtbmc
|
2016-09-24 20:40:22 +02:00 |
Clifford Wolf
|
2e244c2d8e
|
Added yosys-smtbmc --noinfo and --dummy
|
2016-09-19 20:43:28 +02:00 |
Clifford Wolf
|
d009cdd6ee
|
Improved handling of SMT2 logics in yosys-smtbmc
|
2016-09-18 20:48:09 +02:00 |
Clifford Wolf
|
7bc88e8101
|
yosys-smtbmc: added -i support smtc files
|
2016-09-18 00:48:36 +02:00 |
Clifford Wolf
|
d39db41df8
|
Work-around for boolector bug
|
2016-09-13 13:23:06 +02:00 |
Clifford Wolf
|
6f416c1953
|
Added missing :produce-models setting to smtio.py
|
2016-09-11 18:17:22 +02:00 |
Clifford Wolf
|
5199aafca0
|
Minor improvements to smtio.py vcd writer
|
2016-09-10 16:24:08 +02:00 |
Clifford Wolf
|
b582f11074
|
fixed write_smt2 for (non-combinatorial) loops through hierarchical cells
|
2016-09-10 15:14:41 +02:00 |
Clifford Wolf
|
3ceba145d5
|
smt2 mem init bugfix
|
2016-09-08 18:08:15 +02:00 |
Clifford Wolf
|
14bfd3c5c1
|
yosys-smtbmc meminit support
|
2016-09-08 11:16:12 +02:00 |
Clifford Wolf
|
209a3d9ffc
|
Bugfix in "yosys-smtbmc --unroll"
|
2016-09-07 21:01:51 +02:00 |
Clifford Wolf
|
6770d6e0f8
|
Added "yosys-smtbmc --unroll"
|
2016-09-07 20:57:56 +02:00 |
Clifford Wolf
|
97b449fe55
|
yosys-smtbmc: flush stdout after each log msg
|
2016-09-06 01:40:31 +02:00 |