mirror of
				https://github.com/YosysHQ/yosys
				synced 2025-11-03 21:09:12 +00:00 
			
		
		
		
	Add support for SVA sequence concatenation ranges via verific
Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
		
							parent
							
								
									9d963cd29c
								
							
						
					
					
						commit
						5c6247dfa6
					
				
					 3 changed files with 144 additions and 16 deletions
				
			
		| 
						 | 
				
			
			@ -35,6 +35,7 @@ generate_sby() {
 | 
			
		|||
	cat <<- EOT
 | 
			
		||||
		verific -import -extnets -all top
 | 
			
		||||
		prep -top top
 | 
			
		||||
		chformal -early -assume
 | 
			
		||||
 | 
			
		||||
		[files]
 | 
			
		||||
	EOT
 | 
			
		||||
| 
						 | 
				
			
			
 | 
			
		|||
							
								
								
									
										19
									
								
								tests/sva/sva_range.sv
									
										
									
									
									
										Normal file
									
								
							
							
						
						
									
										19
									
								
								tests/sva/sva_range.sv
									
										
									
									
									
										Normal file
									
								
							| 
						 | 
				
			
			@ -0,0 +1,19 @@
 | 
			
		|||
module top (
 | 
			
		||||
	input clk,
 | 
			
		||||
	input a, b, c, d
 | 
			
		||||
);
 | 
			
		||||
	default clocking @(posedge clk); endclocking
 | 
			
		||||
 | 
			
		||||
	assert property (
 | 
			
		||||
		a ##[*] b |=> c until ##[*] d
 | 
			
		||||
	);
 | 
			
		||||
 | 
			
		||||
`ifndef FAIL
 | 
			
		||||
	assume property (
 | 
			
		||||
		b |=> ##5 d
 | 
			
		||||
	);
 | 
			
		||||
	assume property (
 | 
			
		||||
		b || (c && !d) |=> c
 | 
			
		||||
	);
 | 
			
		||||
`endif
 | 
			
		||||
endmodule
 | 
			
		||||
		Loading…
	
	Add table
		Add a link
		
	
		Reference in a new issue