APB write cycle assertion

SystemVerilog
,
8

In reply to rag123:

  • First of all, I am NOT a fan of multiple sequence declarations unless each sequence is complex and serves a specific function, or if I need an endpoint.
  • I am also NOT a fan of multiple implication operators because of vacuity.
 sq1 |=> sq2 |=> sq3
// If sq2 is not a match, the property is vacuous
  • Your sequence s1: sequenceA |-> sequenceB IS NOT A sequence, it is a PROPERTY. It cannot be declared in a sequence declaration
  • Use a compiler/simulator to test your code
    See https://www.edaplayground.com/
  • SPECS says “PSELx, also goes LOW unless the transfer is to be followed immediately by another transfer to the same peripheral”. That is not handled here.
// in ( pwrite && !psel && !penable), there is a need to
// detect another xfr to another peripheral for the !psel

// My take 
ap_ahb_write_with_without_wait: assert property( 
   $rose (pwrite && psel) |-> !penable ##1  
       $rose (penable) ##0 
       $stable ((paddr) && $stable (pwdata)) until_with pready ##1
       pwrite && !psel && !penable // !psel is questionable here 
 );