AHB assertions

property ahb_incr16_htrans_p;

   @(posedge clk) disable iff ( HTRANS == BUSY || HBURST != INCR16)

(HTRANS == NONSEQ) |=> (HTRANS |=> SEQ ) |=> (HTRANS == SEQ)[*14]

endproperty  

property ahb_incr4_htrans_p;
   @(posedge clk) disable iff ( HTRANS == BUSY || HBURST != INCR4)

(HTRANS == NONSEQ) |=> (HTRANS |=> SEQ ) |=> (HTRANS == SEQ)[*2]

endproperty  

// To check AHB incrementing bursts crossing 1KB boundary 
property ahb_1kb_boundary_p;
   @(posedge clk) disable iff (~rst_n)

(HTRANS == SEQ) |=> (HADDR[10:0] != 11'h400);

endproperty  

// To check AHB incrementing address during incrementing bursts 
property ahb_incr_addr_p;
   @(posedge clk) disable iff (~rst_n)

(HTRANS == SEQ) && (HBURST inside {INCR, INCR4, INCR8, INCR16}) && ($past(HTRANS,1) !=1)

 && ($past(HREADY, 1)) |-> (HADDR == ($past(HADDR, 1) + 2**HSIZE));

endproperty  

// To check AHB OKEY for IDLE transfers  
property ahb_idle_okey_p;
   @(posedge clk) disable iff (~rst_n)

(HTRANS == IDLE) && (HRESP == OKEY) |=> (HRESP == OKEY);

endproperty  

// To check AHB 2cycle ERROR response   
property ahb_error_response_p;
   @(posedge clk) disable iff (~rst_n)

$fell(HREADY) && (HRESP == ERROR) |=> (HRESP == ERROR)

endproperty  

// To check stable HADDR HWRITE HWDATA  until HREADY    
property ahb_htrans_wait_for_hready_p(HTRANS, HREADY);
   @(posedge clk) 
 (!HREADY) |=> $stable(HADDR && HWRITE && HWDATA );

endproperty  

// To check stable HTRANS until HREADY    
property ahb_htrans_wait_for_hready_p(HTRANS, HREADY);
   @(posedge clk) 
 HTRANS inside { NONSEQ, SEQ} && !HREADY |=> $stable(HTRANS) throughout HREADY [->1];

endproperty