Function instruction #i is load dst=dst addr=addr imm=imm

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

Format:

instruction #i is load dst=dst addr=addr imm=imm

Input:

Output:

Conditional properties that reference this function:

• if the following are true:
  • instruction #i is load dst=dst addr=addr imm=imm
  • the PC at time t = i

  then value of cell dst at time (t + 1) = value of cell ((value of cell addr at time t) + imm) at time t

  (link)
• if the following are true:
  • instruction #i is load dst=dst addr=addr imm=imm
  • the PC at time t = i
  • not (other = dst)

  then value of cell other at time (t + 1) = value of cell other at time t

  (link)
• if the following are true:
  • instruction #x is load dst=s addr=d imm=imm
  • the PC at time t = x

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

  (link)

Comments

Please log in to add comments