Simple APB transaction descriptions
We can accurately and unambiguously define transactions using PSL Regular Expressions:

Read transaction

( (PADDR==addr_arg) && !PWRITE && PSEL && !PENABLE)  ;
         ( (PADDR==addr_arg) && !PWRITE && PSEL && PENABLE && (PRDATA == data_arg) )


Write transaction

( (PADDR==addr_arg) && PWRITE && PSEL && !PENABLE && (PWDATA == data_arg) )  ;
         ( (PADDR==addr_arg) && PWRITE && PSEL && PENABLE && (PWDATA == data_arg) )
Leveraging the Formal Protocol definition....
Copyright 2009 Structured Design Verification Ltd.