riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity
3,995 Commits 92 Branches 49 Tags 39 MiB
Commit Graph

3995 Commits

Author SHA1 Message Date
Clifford Wolf 8b604004da Check results of (check-sat) in yosys-smtbmc 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-07 22:54:19 +01:00
Clifford Wolf a4bbfd2d15 Fix Verific handling of "assert property (..);" in always block 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-07 20:06:02 +01:00
Clifford Wolf 92d5f4db6f Add "verific -import -V" 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-07 19:40:34 +01:00
Clifford Wolf 252627fc54 Set Verific db_preserve_user_nets flag 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-07 18:08:03 +01:00
Clifford Wolf 6991c132b5 Add Xilinx RAM64X1D and RAM128X1D simulation models 2018-03-07 17:31:48 +01:00
Clifford Wolf 73c01dca65 Add "memory_nordff" pass 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-06 23:31:51 +01:00
Clifford Wolf dcc4a18d5a Update comment about supported SVA in verificsva.cc 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-06 15:47:33 +01:00
Clifford Wolf 03b49654b1 Add SVA NON_CONSECUTIVE_REPEAT and GOTO_REPEAT support 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-06 15:39:46 +01:00
Clifford Wolf 7bb83ae9f2 Add SVA first_match() support 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-06 15:06:35 +01:00
Clifford Wolf 78f2cca2d9 Add SVA within support 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-06 14:41:27 +01:00
Clifford Wolf 5555292ce2 Add support for SVA sequence intersect 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-06 14:26:57 +01:00
Clifford Wolf d86e875f0f Add get_fsm_accept_reject for parsing SVA properties 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-06 11:50:38 +01:00
Clifford Wolf 588ce0e34a Simplified SVA "until" handling 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-06 01:51:42 +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 61a9e2eeb3 Fix connwrappers help message 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 22:54:34 +01:00
Clifford Wolf e5534a080e Improve handling of warning messages 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 22:35:59 +01:00
Clifford Wolf 2935e8ea41 Update copyright header 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 21:31:10 +01:00
Clifford Wolf 8b7602e660 Improve SMT2 encoding of $reduce_{and,or,bool} 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 21:22:20 +01:00
Clifford Wolf 45a6fce92c Fix a hangup in yosys-smtbmc error handling 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 21:13:30 +01:00
Clifford Wolf 480e8e676a Add proper SVA seq.triggered support 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 19:29:26 +01:00
Clifford Wolf 27dd500d31 Add "synth -noshare" 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 17:13:45 +01:00
Clifford Wolf 8dcf3d0c76 Add Verific SVA support for "seq and seq" expressions 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 15:08:21 +01:00
Clifford Wolf 9ab2498c55 Refactor Verific SVA importer property parser 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 14:29:48 +01:00
Clifford Wolf 261cf706f4 Add VerificClocking class and refactor Verific DFF handling 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-04 13:48:53 +01:00
Clifford Wolf ae4e204c76 Improved error handling in yosys-smtbmc 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-03 20:00:07 +01:00
Clifford Wolf 707ddb77bc Add SVA support for sequence OR 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-03 16:34:28 +01:00
Clifford Wolf a44e1edaa3 Terminate running SMT solver when smtbmc is terminated 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-03 14:50:40 +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 cabc3c59e0 Fix handling of SVA "until seq.triggered" properties 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-02 18:17:10 +01:00
Clifford Wolf ab791e61b3 Update SVA cheat sheet in verificsva.cc 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-02 16:05:56 +01:00
Clifford Wolf 4e5f1f59d6 Fix in Verific SVA importer handling of until_with 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-01 19:37:36 +01:00
Clifford Wolf 90ae426078 Mangle names with square brackets in VCD files to work around issues in gtkwave 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-01 14:15:27 +01:00
Clifford Wolf 9a2a8cd97b Fixes and improvements in Verific SVA importer 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-01 11:40:43 +01:00
Clifford Wolf 3c49e3c5b3 Add $rose/$fell support to Verific bindings 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-01 10:12:15 +01:00
Clifford Wolf 3df0d04a7b Merge branch 'verificsva-ng' 2018-02-28 15:32:53 +01:00
Clifford Wolf 5ac3ee858a Add support for PRIM_SVA_UNTIL to new SVA importer 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-28 15:32:17 +01:00
Clifford Wolf 8a1d6ccf0c Add DFSM generator to verific SVA importer 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-28 15:05:33 +01:00
Clifford Wolf 15902d495f Continue refactoring of Verific SVA importer code 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-28 11:45:04 +01:00
Clifford Wolf 25e33d7ab8 Major redesign of Verific SVA importer 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-27 20:33:15 +01:00
Clifford Wolf 6f26695d9b Add -lz for verific builds 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-27 12:15:42 +01:00
Clifford Wolf b6fbeb0969 Add handling of verific OPER_REDUCE_NOR 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-26 15:26:01 +01:00
Clifford Wolf 2aeb4d4e12 Add handling of verific OPER_SELECTOR and OPER_WIDE_SELECTOR 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-26 15:20:27 +01:00
Clifford Wolf 9cd9f5fc78 Add handling of verific OPER_NTO1MUX and OPER_WIDE_NTO1MUX 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-26 15:02:03 +01:00
Clifford Wolf d1cb5150aa Add "SVA syntax cheat sheet" comment to verificsva.cc 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-26 14:31:58 +01:00
Clifford Wolf d31584c649 Add $dlatchsr support to clk2fflogic 2018-02-26 12:20:28 +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 fba499b866 Fix opt_rmdff handling of $dlatchsr 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-26 11:46:05 +01:00
Clifford Wolf 0d636964b8 Merge branch 'forall' 2018-02-23 19:37:00 +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 eb67a7532b Add $allconst and $allseq cell types 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-02-23 13:14:47 +01:00