Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								0acea3548b 
								
							 
						 
						
							
							
								
								Set stack size to at least 128 MB (large stack needed for parsing huge expressions)  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-27 15:04:10 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								5e49ee5c2d 
								
							 
						 
						
							
							
								
								Fix tests/simple/specify.v  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-27 14:34:00 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Udi Finkelstein 
								
							 
						 
						
							
							
							
							
								
							
							
								6378e2cd46 
								
							 
						 
						
							
							
								
								First draft of Verilog parser support for specify blocks and parameters.  
							
							... 
							
							
							
							The only functionality of this code at the moment is to accept correct specify syntax and ignore it.
No part of the specify block is added to the AST 
							
						 
						
							2018-03-27 14:34:00 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								f3eaa0ffa5 
								
							 
						 
						
							
							
								
								Merge pull request  #515  from edcote/patch-1  
							
							... 
							
							
							
							Rename rename to renames 
							
						 
						
							2018-03-27 14:14:51 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								ee3c12d6d9 
								
							 
						 
						
							
							
								
								Chenged "extensions_map" to "extensions_list" in hierarchy.cc  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-27 14:12:57 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								c652774ca2 
								
							 
						 
						
							
							
								
								Merge pull request  #518  from xerpi/master  
							
							... 
							
							
							
							passes/hierarchy: Reduce code duplication in expand_module 
							
						 
						
							2018-03-27 14:10:39 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Sergi Granell 
								
							 
						 
						
							
							
							
							
								
							
							
								f93f8aaa11 
								
							 
						 
						
							
							
								
								passes/hierarchy: Reduce code duplication in expand_module  
							
							... 
							
							
							
							This also makes it easier to add new file extensions support.
Signed-off-by: Sergi Granell <xerpi.g.12@gmail.com> 
							
						 
						
							2018-03-27 09:35:20 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								77bd645c35 
								
							 
						 
						
							
							
								
								Add $mem support to SMT2 clock tagging  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-27 02:11:20 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								6f681c4f82 
								
							 
						 
						
							
							
								
								Fix build for new ABC location on github, also update ABC to a2d59be  
							
							
							
						 
						
							2018-03-27 00:39:01 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								491c352da7 
								
							 
						 
						
							
							
								
								Add .sv support to "hierarchy -libdir"  
							
							
							
						 
						
							2018-03-26 21:19:00 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								315d5e32bf 
								
							 
						 
						
							
							
								
								Fix handling of unclocked immediate assertions in Verific front-end  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-26 13:04:10 +02:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Edmond Cote 
								
							 
						 
						
							
							
								
								
							
							
							
								
							
							
								64ea55056a 
								
							 
						 
						
							
							
								
								Rename rename to renames  
							
							... 
							
							
							
							Create TCL alias for rename command.  Using renames.  Following the same convention as proc -> procs. 
							
						 
						
							2018-03-20 15:50:50 -07:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								3f00702475 
								
							 
						 
						
							
							
								
								Improve yosys-smtbmc log output and error handling  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-17 18:06:17 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									Clifford Wolf 
								
							 
						 
						
							
							
							
							
								
							
							
								4d4e3a8ca6 
								
							 
						 
						
							
							
								
								Improve handling of invalid check-sat result in smtio.py  
							
							... 
							
							
							
							Signed-off-by: Clifford Wolf <clifford@clifford.at> 
							
						 
						
							2018-03-17 12:17:53 +01:00 
							
								 
							
						 
					 
				
					
						
							
								
								
									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