Function JAL instruction with jump to: jump_to

the jump-and-link (jal) instruction saves the value of the program counter + 1 to the return register and sets the PC to jump_to

Format:

JAL instruction with jump to: jump_to

Input:

Output:

Conditional properties that reference this function:

• if the following are true:
  • the instruction at computer c and index i = JAL instruction with jump to: jump_to
  • the PC at computer c and time t = i

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

  (link)
• if the following are true:
  • the instruction at computer c and index i = JAL instruction with jump to: jump_to
  • the PC at computer c and time t = i
  • not (x = 2)

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

  (link)
• if the following are true:
  • the instruction at computer c and index i = JAL instruction with jump to: jump_to
  • the PC at computer c and time t = i

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

  (link)

Comments

Please log in to add comments