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)); endpr...