mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-11-04 05:19:11 +00:00 
			
		
		
		
	Add todo for more features to verificsva.cc
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
		
							parent
							
								
									7cf9d88028
								
							
						
					
					
						commit
						462e9f7bd4
					
				
					 1 changed files with 45 additions and 8 deletions
				
			
		| 
						 | 
					@ -21,14 +21,51 @@
 | 
				
			||||||
// Currently supported SVA sequence and property syntax:
 | 
					// Currently supported SVA sequence and property syntax:
 | 
				
			||||||
// http://symbiyosys.readthedocs.io/en/latest/verific.html
 | 
					// http://symbiyosys.readthedocs.io/en/latest/verific.html
 | 
				
			||||||
//
 | 
					//
 | 
				
			||||||
// Todos:
 | 
					// Next gen property syntax:
 | 
				
			||||||
//   property and property
 | 
					//   basic_property
 | 
				
			||||||
//   sequence |-> always sequence
 | 
					//   [antecedent_condition] property
 | 
				
			||||||
//   sequence |-> eventually sequence
 | 
					//   [antecedent_condition] always.. property
 | 
				
			||||||
//   sequence implies sequence
 | 
					//   [antecedent_condition] eventually.. basic_property
 | 
				
			||||||
//   sequence iff sequence
 | 
					//   [antecedent_condition] property until.. expression
 | 
				
			||||||
//   accept_on (expr) prop
 | 
					//   [antecedent_condition] basic_property until.. basic_property
 | 
				
			||||||
//   reject_on (expr) prop
 | 
					//
 | 
				
			||||||
 | 
					// antecedent_condition:
 | 
				
			||||||
 | 
					//   sequence |->
 | 
				
			||||||
 | 
					//   sequence |=>
 | 
				
			||||||
 | 
					//
 | 
				
			||||||
 | 
					// basic_property:
 | 
				
			||||||
 | 
					//   sequence
 | 
				
			||||||
 | 
					//   sequence #-# basic_property
 | 
				
			||||||
 | 
					//   sequence #=# basic_property
 | 
				
			||||||
 | 
					//   basic_property or basic_property       (cover only)
 | 
				
			||||||
 | 
					//   basic_property and basic_property      (assert/assume only)
 | 
				
			||||||
 | 
					//   basic_property implies basic_property
 | 
				
			||||||
 | 
					//   basic_property iff basic_property
 | 
				
			||||||
 | 
					//
 | 
				
			||||||
 | 
					// sequence:
 | 
				
			||||||
 | 
					//   expression
 | 
				
			||||||
 | 
					//   sequence ##N sequence
 | 
				
			||||||
 | 
					//   sequence ##[*] sequence
 | 
				
			||||||
 | 
					//   sequence ##[+] sequence
 | 
				
			||||||
 | 
					//   sequence ##[N:M] sequence
 | 
				
			||||||
 | 
					//   sequence ##[N:$] sequence
 | 
				
			||||||
 | 
					//   sequence [*]
 | 
				
			||||||
 | 
					//   sequence [+]
 | 
				
			||||||
 | 
					//   sequence [*N]
 | 
				
			||||||
 | 
					//   sequence [*N:M]
 | 
				
			||||||
 | 
					//   sequence [*N:$]
 | 
				
			||||||
 | 
					//   sequence or sequence
 | 
				
			||||||
 | 
					//   sequence and sequence
 | 
				
			||||||
 | 
					//   expression throughout sequence
 | 
				
			||||||
 | 
					//   sequence intersect sequence
 | 
				
			||||||
 | 
					//   sequence within sequence
 | 
				
			||||||
 | 
					//   first_match( sequence )
 | 
				
			||||||
 | 
					//   expression [=N]
 | 
				
			||||||
 | 
					//   expression [=N:M]
 | 
				
			||||||
 | 
					//   expression [=N:$]
 | 
				
			||||||
 | 
					//   expression [->N]
 | 
				
			||||||
 | 
					//   expression [->N:M]
 | 
				
			||||||
 | 
					//   expression [->N:$]
 | 
				
			||||||
 | 
					
 | 
				
			||||||
 | 
					
 | 
				
			||||||
#include "kernel/yosys.h"
 | 
					#include "kernel/yosys.h"
 | 
				
			||||||
| 
						 | 
					
 | 
				
			||||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue