Function a LOAD instruction with dst: dst addr: addr and imm: imm

the load instruction copies the value stored in address (value at addr + imm) to address dst

Format:

a LOAD instruction with dst: dst addr: addr and imm: imm

Input:

Output:

Conditional properties that reference this function:

• if the following are true:

  • the instruction at computer c and index i = a LOAD instruction with dst: dst addr: addr and imm: imm
  • the PC at computer c and time t = i

  then byte at ID: c, cell #dst at time (t + 1) = byte at ID: c, cell #((byte at ID: c, cell #addr at time t) + imm) at time t

  (link)

• if the following are true:

  • the instruction at computer c and index i = a LOAD instruction with dst: dst addr: addr and imm: imm
  • the PC at computer c and time t = i
  • not (other = dst)

  then byte at ID: c, cell #other at time (t + 1) = byte at ID: c, cell #other at time t

  (link)

• if the following are true:

  • the instruction at computer c and index x = a LOAD instruction with dst: s addr: d and imm: imm
  • the PC at computer c and time t = x

  then the PC at computer c and time (t + 1) = x + 1

  (link)

Comments

Please log in to add comments