Clifford Wolf
|
c9672e2e2e
|
Fix handling of zero-length cell connections in SMT2 back-end
Signed-off-by: Clifford Wolf <clifford@clifford.at>
|
2018-02-08 19:12:12 +01:00 |
Clifford Wolf
|
e4f0218907
|
Fixed gcc 7.2 "statement will never be executed" warning
|
2018-02-03 14:31:47 +01:00 |
Clifford Wolf
|
e97f10b142
|
Fix smtio.py for large SMT2 S-expressions
|
2018-01-29 12:34:28 +01:00 |
Clifford Wolf
|
54aeca0983
|
Move user-provided smt2 info stmts to the top of the yosys-smtbmc smt2 output
|
2018-01-18 14:25:22 +01:00 |
Clifford Wolf
|
9804ebedbf
|
Add "no driver for signal bit" error msg to btor back-end
|
2017-12-24 17:30:36 +01:00 |
Clifford Wolf
|
292984896b
|
Simple fix BTOR memory encoding
|
2017-12-17 18:57:54 +01:00 |
Clifford Wolf
|
bbdcc1f9d4
|
Improve BTOR memory encoding
|
2017-12-17 18:55:17 +01:00 |
Clifford Wolf
|
30f23281ed
|
Add array support to btor back-end
|
2017-12-15 02:19:06 +01:00 |
Clifford Wolf
|
ad901671c5
|
Add $anyconst/$anyseq support to btor back-end
|
2017-12-15 00:40:24 +01:00 |
Clifford Wolf
|
162c29bd6b
|
Merge branch 'master' into btor-ng
|
2017-12-14 03:13:47 +01:00 |
Clifford Wolf
|
9419de3e37
|
Add yosys-smtbmc VCD writer support for memories with async writes
|
2017-12-14 03:06:00 +01:00 |
Clifford Wolf
|
a48ec49017
|
Merge branch 'master' into btor-ng
|
2017-12-14 02:17:01 +01:00 |
Clifford Wolf
|
2625da6440
|
Add smt2 back-end support for async write memories
|
2017-12-14 02:07:10 +01:00 |
Clifford Wolf
|
546de7fa4f
|
Add "write_btor -s" mode
|
2017-12-13 00:15:44 +01:00 |
Clifford Wolf
|
0881bbf2e7
|
Add state initval handling to btor back-end
|
2017-12-12 23:44:08 +01:00 |
Clifford Wolf
|
f697282246
|
Add btor back-end support for 'x' constants
|
2017-12-12 21:48:55 +01:00 |
Clifford Wolf
|
82d1fd77de
|
Add btor $shift/$shiftx support
|
2017-12-11 14:24:19 +01:00 |
Clifford Wolf
|
cc119b5232
|
Fix btor back-end shift handling
|
2017-12-10 08:40:11 +01:00 |
Clifford Wolf
|
133a0f4978
|
Add support for $pmux in btor back-end
|
2017-12-10 08:11:08 +01:00 |
Clifford Wolf
|
83cf736309
|
Add support for more cell types to btor back-end
|
2017-12-10 07:16:47 +01:00 |
Clifford Wolf
|
63343aeaaa
|
Fix btor concat
|
2017-12-09 05:58:14 +01:00 |
Clifford Wolf
|
da91b31bb2
|
Fixed "yosys-smtbmc -g" handling of no solution
|
2017-11-27 19:43:36 +01:00 |
Clifford Wolf
|
b981e5aa69
|
Fixed "yosys-smtbmc -g" handling of no solution
|
2017-11-27 17:42:32 +01:00 |
Clifford Wolf
|
e3a51b3e87
|
Bugfixes in new BTOR back-end
|
2017-11-24 18:13:41 +01:00 |
Clifford Wolf
|
60d1129506
|
Progress in new BTOR back-end
|
2017-11-23 23:44:39 +01:00 |
Clifford Wolf
|
b3d6b277ea
|
Progress in new BTOR back-end
|
2017-11-23 18:50:10 +01:00 |
Clifford Wolf
|
cc2495d48d
|
Progress in new BTOR back-end
|
2017-11-23 18:14:53 +01:00 |
Clifford Wolf
|
e41dcaa759
|
Progress with new BTOR backend
|
2017-11-23 08:28:29 +01:00 |
Clifford Wolf
|
6ee305553a
|
Add skeleton for new BTOR back-end
|
2017-11-23 06:38:57 +01:00 |
Clifford Wolf
|
eceacdb9a3
|
Remove old BTOR back-end
|
2017-11-23 04:28:51 +01:00 |
Clifford Wolf
|
455c1c9d97
|
Fix SMT2 handling of initstate in sub-modules
|
2017-10-29 13:21:20 +01:00 |
Clifford Wolf
|
1170508264
|
Improve smtio performance by using reader thread, not writer thread
|
2017-10-26 01:01:55 +02:00 |
Clifford Wolf
|
f513494f5f
|
Use separate writer thread for talking to SMT solver to avoid read/write deadlock
|
2017-10-25 19:59:56 +02:00 |
Clifford Wolf
|
76326c163a
|
Improve p_* functions in smtio.py
|
2017-10-25 15:45:32 +02:00 |
Clifford Wolf
|
c672c321e3
|
Capsulate smt-solver read/write in separate functions
|
2017-10-25 13:37:11 +02:00 |
Clifford Wolf
|
dd46d76394
|
Fix a bug in yosys-smtbmc in ROM handling
|
2017-10-25 13:05:14 +02:00 |
Clifford Wolf
|
adf1754729
|
Add $shiftx support to verilog front-end
|
2017-10-07 13:40:54 +02:00 |
Clifford Wolf
|
65f91e5120
|
Rename "write_verilog -nobasenradix" to "write_verilog -decimal"
|
2017-10-03 17:31:21 +02:00 |
dh73
|
e480847753
|
Fixed wrong declaration in Verilog backend
|
2017-10-01 11:11:32 -05:00 |
dh73
|
cbaba62401
|
Adding Cyclone IV (E, GX), Arria 10, Cyclone V and LPM functions (ALTPLL and M9K); M9K is not finished yet. Achronix Speedster also in this commit. Both Arria10 and Speedster-i are still experimental due complexity, but you can experiment around those devices right now
|
2017-10-01 11:04:17 -05:00 |
Clifford Wolf
|
c2d737457a
|
Fix bug in write_smt2 (export logic driving hierarchical cells before exporting regs)
|
2017-08-25 11:44:48 +02:00 |
Clifford Wolf
|
48b2b376d0
|
Add "yosys-smtbmc --smtc-init --smtc-top --noinit"
|
2017-08-04 17:09:08 +02:00 |
Clifford Wolf
|
3a8f6f0f51
|
Add verilator support to testbenches generated by yosys-smtbmc
|
2017-07-21 14:33:29 +02:00 |
Clifford Wolf
|
10c7709e68
|
Generate FSM-style testbenches in smtbmc
|
2017-07-12 15:57:04 +02:00 |
Clifford Wolf
|
4a8c131fa7
|
Fix the fixed handling of x-bits in EDIF back-end
|
2017-07-11 17:45:29 +02:00 |
Clifford Wolf
|
479be3cec7
|
Fix handling of x-bits in EDIF back-end
|
2017-07-11 17:38:19 +02:00 |
Clifford Wolf
|
9557fd2a36
|
Add attributes and parameter support to JSON front-end
|
2017-07-10 13:17:38 +02:00 |
Clifford Wolf
|
3c693b6561
|
Change s/asserts/assertions/ in yosys-smtbmc log messages
|
2017-07-07 11:52:25 +02:00 |
Clifford Wolf
|
8f7404f82c
|
Add "yosys-smtbmc --presat"
|
2017-07-07 02:47:30 +02:00 |
Clifford Wolf
|
5442554e6f
|
Fix generation of multiple outputs for same AIG node in write_aiger
|
2017-07-05 14:23:54 +02:00 |
Clifford Wolf
|
37af6294bd
|
Add write_table command
|
2017-07-05 12:13:53 +02:00 |
Clifford Wolf
|
3e0948e16f
|
Remove unneeded delays in smtbmc vlogtb
|
2017-07-03 15:37:17 +02:00 |
Clifford Wolf
|
287831dca3
|
Include output ports with constant driver in AIGER output
|
2017-07-03 14:53:17 +02:00 |
Clifford Wolf
|
ea805af6f5
|
Add "yosys-smtbmc --vlogtb-top"
|
2017-07-01 18:19:23 +02:00 |
Clifford Wolf
|
7d2fb6e2fc
|
Fix smtbmc vlogtb bug in $anyseq handling
|
2017-07-01 02:13:32 +02:00 |
Clifford Wolf
|
8f8baccfde
|
Fix generation of vlogtb output in yosys-smtbmc for "rand reg" and "rand const reg"
|
2017-06-07 12:30:24 +02:00 |
Clifford Wolf
|
c365e33fd7
|
Fix AIGER back-end for multiple symbols per input/latch/output/property
|
2017-05-30 19:09:11 +02:00 |
Clifford Wolf
|
9ed4c9d710
|
Improve write_aiger handling of unconnected nets and constants
|
2017-05-28 11:31:35 +02:00 |
Clifford Wolf
|
d9201b85f3
|
Change default smt2 solver to yices (Yices 2 has switched its license to GPL)
|
2017-05-27 11:56:01 +02:00 |
Clifford Wolf
|
2122ae69b3
|
Add workaround for CBMC bug to SimpleC back-end
|
2017-05-17 21:07:54 +02:00 |
Clifford Wolf
|
05cdd58c8d
|
Add $_ANDNOT_ and $_ORNOT_ gates
|
2017-05-17 09:08:29 +02:00 |
Clifford Wolf
|
9f4fbc5e74
|
Add <modname>_init() function generator to simpleC back-end
|
2017-05-16 19:34:07 +02:00 |
Clifford Wolf
|
35be567605
|
Improve simplec back-end
|
2017-05-16 08:50:23 +02:00 |
Clifford Wolf
|
8d3c706459
|
Improve simplec back-end
|
2017-05-15 13:21:59 +02:00 |
Clifford Wolf
|
9c397ea78b
|
Improve simplec back-end
|
2017-05-14 13:14:49 +02:00 |
Clifford Wolf
|
628daab277
|
Improve simplec back-end
|
2017-05-13 18:47:31 +02:00 |
Clifford Wolf
|
ef7594ce3d
|
Improve simplec back-end
|
2017-05-12 22:39:16 +02:00 |
Clifford Wolf
|
7931e1ebb4
|
Added support for more gate types to simplec back-end
|
2017-05-12 17:42:31 +02:00 |
Clifford Wolf
|
bd4ed19887
|
Add first draft of simple C back-end
|
2017-05-12 14:13:33 +02:00 |
Clifford Wolf
|
1a4b7c6bfa
|
Fix boolector support in yosys-smtbmc
|
2017-05-08 14:33:22 +02:00 |
Clifford Wolf
|
106e44f406
|
Add "write_smt2 -stdt" mode
|
2017-03-20 12:00:35 +01:00 |
Clifford Wolf
|
0ac72e759d
|
Add generation of logic cells to EDIF back-end runtest.py
|
2017-03-19 14:57:40 +01:00 |
Clifford Wolf
|
850f8299a9
|
Fix EDIF: portRef member 0 is always the MSB bit
|
2017-03-19 14:53:28 +01:00 |
Clifford Wolf
|
1390e9a0a7
|
Add simple EDIF test case generator and checker
|
2017-03-18 15:00:03 +01:00 |
Clifford Wolf
|
c855353986
|
Improve smt2 encodings of assert/assume/cover, better wire_smt2 help msg
|
2017-03-04 23:41:54 +01:00 |
Clifford Wolf
|
a6ca28276e
|
Add write_aiger $anyseq support
|
2017-03-02 16:39:48 +01:00 |
Clifford Wolf
|
fbd52ec6dd
|
Use hex addresses in smtbmc vcd mem traces
|
2017-02-28 13:54:50 +01:00 |
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 |
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 |
Clifford Wolf
|
372d672c2a
|
Minor bugfix in write_smt2
|
2016-09-04 16:32:47 +02:00 |
Clifford Wolf
|
fa5565b606
|
Added boolector support to yosys-smtbmc
|
2016-09-03 14:26:00 +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
|
aa25a4cec6
|
Added $anyconst support to yosys-smtbmc
|
2016-08-30 19:27:42 +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
|
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
|
f56dba8e20
|
Some changes to yosys-smtbmc cmd line options, add --final-only
|
2016-08-27 22:04:15 +02:00 |
Clifford Wolf
|
adcda6817e
|
Added smtc "final" statement
|
2016-08-27 14:30:36 +02:00 |
Clifford Wolf
|
17233b11e1
|
Various fixes and improvements in smt2 back-end
|
2016-08-26 17:33:02 +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
|
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
|
7a33b9892a
|
yosys-smtbmc: improved --dump-vlogtb handling of memories
|
2016-08-21 15:56:22 +02:00 |
Clifford Wolf
|
f7578b0239
|
Added "yosys-smtbmc --dump-vlogtb"
|
2016-08-20 18:43:39 +02:00 |
Clifford Wolf
|
ed785194de
|
Added support for memories to smtio.py
|
2016-08-20 18:42:32 +02:00 |
Clifford Wolf
|
c325bae792
|
Deprecated "write_smt2 -regs" (by default on now), and some other smt2 back-end improvements
|
2016-08-20 18:41:57 +02:00 |
Clifford Wolf
|
28271e43c9
|
Added "yosys-smtbmc -g"
|
2016-08-20 16:32:50 +02:00 |
Clifford Wolf
|
a889acb897
|
Added smtbmc longopt support
|
2016-08-20 16:07:59 +02:00 |
Clifford Wolf
|
75bf7416f0
|
Bugfix in partial mem write handling in verilog back-end
|
2016-08-20 13:06:06 +02:00 |
Clifford Wolf
|
9b8e06bee1
|
Added missing support for mem read enable ports to verilog back-end
|
2016-08-18 21:47:02 +02:00 |
Clifford Wolf
|
de8ee412c3
|
Improved smtbmc vcd generation performance
|
2016-08-18 11:17:45 +02:00 |
Clifford Wolf
|
dfcd30ea86
|
Added printing of code loc of failed asserts to yosys-smtbmc
|
2016-08-17 20:10:02 +02:00 |
Clifford Wolf
|
f0a8713fea
|
Fixed upto handling in verilog back-end
|
2016-08-15 08:26:20 +02:00 |
Clifford Wolf
|
21e1bac084
|
Merge branch 'master' of github.com:cliffordwolf/yosys
|
2016-07-30 12:50:39 +02:00 |
Clifford Wolf
|
5fe13a16ea
|
Added "write_verilog -defparam"
|
2016-07-30 12:46:06 +02:00 |
Clifford Wolf
|
7fa61cba1b
|
Added "write_verilog -nodec -nostr"
|
2016-07-30 12:38:40 +02:00 |
Clifford Wolf
|
da56a5bbc6
|
Added $initstate support to smtbmc flow
|
2016-07-27 16:11:37 +02:00 |
whitequark
|
546233f0e1
|
write_json: also write module attributes.
|
2016-07-12 06:32:04 +00:00 |
Clifford Wolf
|
c71785d65e
|
Yosys-smtbmc: Support for hierarchical VCD dumping
|
2016-07-11 12:49:33 +02:00 |
Clifford Wolf
|
0153ad85d9
|
Moved smt2 yosys info parsing from smtbmc.py to smtio.py
|
2016-07-11 11:49:05 +02:00 |
Clifford Wolf
|
771c5fe000
|
Support for hierarchical designs in smt2 back-end
|
2016-07-10 18:11:25 +02:00 |
Clifford Wolf
|
27b5347a87
|
Restored blif "-true - .." behavior, use "-true + .." for eddiehung-vtr behavior
|
2016-07-08 11:51:04 +02:00 |
Clifford Wolf
|
72149aba2e
|
In BLIF, a .names without entries already always outputs 0
|
2016-07-08 11:41:26 +02:00 |
Clifford Wolf
|
f6b7cf23d6
|
Merge branch 'yosys-0.5-vtr' of https://github.com/eddiehung/yosys into eddiehung-vtr
|
2016-07-08 11:32:36 +02:00 |
Clifford Wolf
|
5ffad4e073
|
Added $sop support to BLIF back-end
|
2016-06-18 12:28:49 +02:00 |
Clifford Wolf
|
f3983a0940
|
Also escape "=" in spice output
|
2016-05-20 16:43:13 +02:00 |
Clifford Wolf
|
d10dfccabb
|
Added "write_blif -noalias"
|
2016-05-06 15:05:53 +02:00 |