
SystemC Transactional Models 629
The expression of this property requires the memorization of the address transferred to
the DMA, to be able to check that this address is actually used when the memory is read.
In the property below,
req src addr is the variable that memorizes this value:
// Modeling layer:
int req_src_addr;
// Each time an address is transferred into the source register, it is stored
// into req_src_addr:
if (initiator_port.write_CALL() && initiator_port.write_CALL.p1 == 0x4000+pv_dma::SRC_ADDR)
req_src_addr = initiator_port.write_CALL.p2;
// Assertion:
assert always ((initiator_port.write_CALL() &&
initiator_port.write_CALL.p1 == 0x4000+pv_dma::SRC_ADDR) ...