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

3961 Commits

Author SHA1 Message Date
Clifford Wolf e7862d4f64 Update todo for more features to verificsva.cc 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-16 15:48:48 +01:00
Clifford Wolf 38596ce68f Update todo for more features to verificsva.cc 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-16 12:16:52 +01:00
Clifford Wolf 462e9f7bd4 Add todo for more features to verificsva.cc 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-16 12:15:36 +01:00
Clifford Wolf 7cf9d88028 Improve import of memories via Verific 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-15 18:20:37 +01:00
Clifford Wolf bf402a806a Fix handling of SV compilation units in Verific front-end 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-14 20:22:11 +01:00
Clifford Wolf 08225f49a4 Add "expose -input" 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-12 13:52:52 +01:00
Clifford Wolf 83ffb23739 Add "setundef -undef" 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-12 13:52:35 +01:00
Udi Finkelstein 2b9c75f8e3 This PR should be the base for discussion, do not merge it yet! 
It correctly detects reg/wire mix and incorrect use on blocking,nonblocking assignments within blocks and assign statements.

What it DOES'T do:
Detect registers connected to output ports of instances.

Where it FAILS:
memorty nonblocking assignments causes spurious (I assume??) errors on yosys-generated "_ADDR", "_DATA", "EN" signals.

You can test it with tests/simple/reg_wire_error.v (look inside for the comments to enable/disable specific lines)
 2018-03-11 23:09:34 +02:00
Larry Doolittle efaef82f75 Squelch trailing whitespace, including meta-whitespace 2018-03-11 16:03:41 +01:00
Larry Doolittle 82fecc98c0 Harmonize uses of _WIN32 macro 2018-03-11 16:01:30 +01:00
Clifford Wolf 307c16a309 Fix SVA handling of NON_CONSECUTIVE_REPEAT and GOTO_REPEAT 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-10 16:24:01 +01:00
Clifford Wolf ce37b6d730 Fix variable name typo in verificsva.cc 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-10 14:33:42 +01:00
Clifford Wolf da216937b1 Add support for trivial SVA sequences and properties 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-10 14:32:01 +01:00
Clifford Wolf a74f805ba0 Fix handling of src attributes in flatten 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-10 13:55:30 +01:00
Clifford Wolf 3545c0fffb Remove debug prints from yosys-smtbmc VCD writer 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-08 16:24:35 +01:00
Clifford Wolf a15208f301 Use Verific hier_tree component for elaboration 
Signed-off-by: Clifford Wolf <clifford@clifford.at>
 2018-03-08 13:26:33 +01:00
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