APB write cycle assertion

SystemVerilog
,
6

In reply to rag123:

  • I made a mistake in $stable(paddr && pwdata) because they are vectors, and you do to want to AND the vectors and then check for stability. Should be
    $stable(paddr) && $stable(pwdata).
  • If you look at the timing, addr@T2 == addr@T3, i.e., thus stable
    The $stable is tested at T3, the cycle after the rose in the antecedent.
    I see 2 clocks in the stabibilty, one at the $rose (at t2) and other in the next cycle at T3.

ap: assert property( 
           @(posedge pclk) now_waite_write ##0  
              $rose (pwrite && psel) |->  ##1   // 1 $rose is at T2 
              $stable(paddr) && $stable(pwdata) ##0    / 2 at T3
              // addr@T2 == addr@T3, i.e., thus stable 
              $rose (penable && pready) ##1                  // 3  at $rose at T3
              pwrite && !psel && !penable);                  // 4  at T4