| 
				
				
				
				 | 
			
			 | 
			@@ -0,0 +1,35 @@ | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			module ass(); | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
  | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			//wvalid id high and wready is low then wdata,wid,wstb should be stable | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
  | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			property p1(); | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
  | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    @(posedge clk) | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			   disable iff(rst) | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			   (wvalid & !wready) |-> ($stable(wdata) && $stable(wid) && $stable(wstrb)); | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
  | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			endproperty | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
  | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
  | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			assert property (p1) | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    $display("PASS"); | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 else | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
				 $diplay("FAIL"); | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
  | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 //In write transaction when burst type is wrap then len must have 2,4,8 or 16 | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
  | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			property p1(); | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
  | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    @(posedge clk) | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			   disable iff(rst) | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			   (awvalid & awburst==2'b01) |-> ((awlen==8'b00000010)||(awlen==8`b00000100)||(awlen==8'b00001000)||(awlen==8`b00010000)); | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
  | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			endproperty | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
  | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
  | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			assert property (p1) | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			    $display("PASS"); | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 else | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
				 $diplay("FAIL"); | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			
  | 
		
		
	
		
			
			 | 
			 | 
			
			 | 
			 endmodule |