Design and verification of SystemC transaction-level models