Clifford Wolf
|
2203562268
|
Add smtbmc support for memory vcd dumping
|
2017-02-26 21:26:32 +01:00 |
Clifford Wolf
|
80ecd7a26f
|
Fix extra newline bug in write_smt2
|
2017-02-26 14:41:27 +01:00 |
Clifford Wolf
|
6e152f7aa1
|
Fix bug in smtio unroll code
|
2017-02-26 14:39:07 +01:00 |
Clifford Wolf
|
66a1617b69
|
Fix assert checking in "yosys-smtbmc -c --append"
|
2017-02-26 11:06:26 +01:00 |
Clifford Wolf
|
fd1cc0c73d
|
Improve (and fix for stbv mode) SMT2 memory API
|
2017-02-26 10:58:34 +01:00 |
Clifford Wolf
|
38bf458037
|
Add support for "yosys-smtbmc -c --append"
|
2017-02-25 23:41:40 +01:00 |
Clifford Wolf
|
c7d1286728
|
Improve "write_edif" help message
|
2017-02-25 16:35:53 +01:00 |
Clifford Wolf
|
dfddf391f9
|
Move EdifNames out of double-private namespace
|
2017-02-25 16:29:27 +01:00 |
Clifford Wolf
|
8c61ecdd6e
|
Clean up edif code, swap bit indexing of "upto" ports
|
2017-02-25 16:28:34 +01:00 |
Clifford Wolf
|
b76c89a5dd
|
Merge branch 'master' of https://github.com/klammerj/yosys into klammerj-master
|
2017-02-25 15:59:02 +01:00 |
Clifford Wolf
|
dac0842d61
|
Add $live and $fair support to AIGER back-end.
|
2017-02-25 13:07:15 +01:00 |
Clifford Wolf
|
7af9727f78
|
Add "write_smt2 -stbv"
|
2017-02-24 18:24:53 +01:00 |
Clifford Wolf
|
a9c3acf5a2
|
Add SMT2 statebv mode (inactive for now)
|
2017-02-24 14:04:52 +01:00 |
Johann Klammer
|
6d7a77dbf6
|
Did as you requested, /but/...
Now the nets are wired in reverse again because the netlister still uses zero-based indices.
|
2017-02-24 13:18:49 +01:00 |
Johann Klammer
|
06df86aae3
|
add options for edif flavors
*to force renames on wide ports
*to choose array delimiters
*to choose up or downwards indices
|
2017-02-23 19:42:37 +01:00 |
Clifford Wolf
|
242c5f01de
|
Add "yosys-smtbmc -S <opt>"
|
2017-02-19 22:51:29 +01:00 |
Clifford Wolf
|
4e80ce97a8
|
Add warning about x/z bits left unconnected in EDIF output
|
2017-02-14 12:49:35 +01:00 |
Adam Izraelevitz
|
794cec0016
|
More progress on Firrtl backend.
Chisel -> Firrtl -> Verilog -> Firrtl -> Verilog is successful for a
simple rocket-chip design.
|
2017-02-13 11:17:53 -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
|
18ea65ef04
|
Add "yosys-smtbmc --aig <aim_filename>:<aiw_filename>" support
|
2017-01-30 11:38:43 +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
|
b7cfb7dbd2
|
Fix $initstate handling bug in yosys-smtbmc
|
2017-01-11 14:14:12 +01:00 |
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 |