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
|
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 |