riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
4,249 Commits 75 Branches 48 Tags 61 MiB
Commit Graph

80 Commits

Author SHA1 Message Date
Clifford Wolf 0b9bb852c6 Add yosys-smtbmc support for btor witness 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-12-10 03:43:07 +01:00
Clifford Wolf 47a5dfdaa4 Add "yosys-smtbmc --btorwit" skeleton 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-12-08 06:59:27 +01:00
Clifford Wolf d0acea4f2e Add proper error message for when smtbmc "append" fails 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-11-04 14:41:28 +01:00
Clifford Wolf cedbc35f4b Imporove yosys-smtbmc error handling, Improve VCD output 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-05 12:17:22 +01:00
Clifford Wolf 3ced2cca6e Fix smtbmc smtc/aiw parser for wire names containing [] 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-03 14:15:49 +01:00
Clifford Wolf 675dd5347a Small fixes and improvements in $allconst/$allseq handling 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-26 11:58:44 +01:00
Clifford Wolf b13e6bd375 Add smtbmc support for exist-forall problems 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-23 19:33:30 +01:00
Clifford Wolf 17583b6a21 Add support for mockup clock signals in yosys-smtbmc vcd output 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-20 17:45:22 +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 da91b31bb2 Fixed "yosys-smtbmc -g" handling of no solution 2017-11-27 19:43:36 +01:00
Clifford Wolf dd46d76394 Fix a bug in yosys-smtbmc in ROM handling 2017-10-25 13:05:14 +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 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 3e0948e16f Remove unneeded delays in smtbmc vlogtb 2017-07-03 15:37: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 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 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 7af9727f78 Add "write_smt2 -stbv" 2017-02-24 18:24:53 +01: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 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 81bb952e5d Handle "always 1" like "always -1" in .smtc files 2017-01-02 20:08:03 +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 f257ccf22e Added "yosys-smtbmc --append" 2016-11-22 21:21:13 +01:00
Clifford Wolf 281a977b39 Ignore L_pi nets in "yosys-smtbmc --cex" 2016-10-18 10:54:53 +02:00
Clifford Wolf 0bcc617a4f Added "yosys-smtbmc --cex <filename>" 2016-10-17 14:57:28 +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 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 97b449fe55 yosys-smtbmc: flush stdout after each log msg 2016-09-06 01:40:31 +02:00
Clifford Wolf fa5565b606 Added boolector support to yosys-smtbmc 2016-09-03 14:26:00 +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 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