APB write cycle assertion

SystemVerilog
,
7

In reply to ben@SystemVerilog.us:

Thanks a lot Ben :) I also tried with Wait states. can you let me know if this is correct?



sequence s1;
    $rose (pwrite && psel) |-> ##1 (pwrite && psel) until with pready;
  endsequence
  
  sequence s2;
    $stable ((paddr) && $stable (pwdata)) until with pready;
  endsequence
  
  sequence s3;
    $rose (penable) ##1 penable until with pready
  endsequence
  

property p2;
    @(posedge pclk)    
    s1 |=> s2 |=> s3 ##1 pwrite && !psel && !penable
  endproperty

assert property (p2);