riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
3,888 Commits 76 Branches 48 Tags 62 MiB
Commit Graph

462 Commits

Author SHA1 Message Date
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