// After reset deasserted and one write, FIFO is no longer empty
 // -------------------------------------------------------------------
 fifo_not_empty_after_write: assert property (
     @(posedge clock) disable iff (reset)
     (f_empty && wr_en && !f_full) |=> (!f_empty)
 );

//Counter
always@(posedge clock)
begin
        if (reset)
        begin
                counter <= {(AWIDTH){1'b0}};
        end
        else
        begin
                if (rd_en && !f_empty && !wr_en)
                begin
                        counter <= w_counter;
                end
                else if (wr_en && !f_full && !rd_en)
                begin
                        counter <= w_counter;
                end
        end
end

 assign w_counter = (rd_en && !f_empty && !wr_en)? counter - 4'd1: (wr_en && !f_full && !rd_en)? counter + 4'd1: w_counter ;

// -------------------------------------------------------------------
// APB protocol: PENABLE must follow PSELx
// -------------------------------------------------------------------

penable_requires_pselx: assert property (
	@(posedge PCLK) disable iff (!PRESETn)
	PENABLE |-> PSELx
);

 paddr_stable_during_enable: assert property (
	  @(posedge PCLK) disable iff (!PRESETn)
	  (PSELx && PENABLE) |-> $stable(PADDR)
  );