Function Instruction At

The Instruction At function is the instruction at index i

Format:

the instruction at computer id and index i

Input:

Output:

Conditional properties that reference this function:

• if the following are true:
  • the instruction at computer c and index i = an ADDI instruction with src: src imm: imm and dst: dst
  • 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 #src at time t) + imm

  (link)
• if the following are true:
  • the instruction at computer c and index i = an ADDI instruction with src: src imm: imm and dst: dst
  • 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 i = subtract immediate instruction with dst: dst src: src and immediate: 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 #src at time t) - imm

  (link)
• if the following are true:
  • the instruction at computer c and index i = subtract immediate instruction with dst: dst src: src and immediate: 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 i = an add instruction with dst: d src1: s1 and src2: s2
  • the PC at computer c and time t = i

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

  (link)
• if the following are true:
  • the instruction at computer c and index i = an add instruction with dst: d src1: s1 and src2: s2
  • the PC at computer c and time t = i
  • not (other = d)

  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 i = a STORE instruction with src: src address: addr and immediate: imm
  • the PC at computer c and time t = i

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

  (link)
• if the following are true:
  • the instruction at computer c and index i = a STORE instruction with src: src address: addr and immediate: imm
  • the PC at computer c and time t = i
  • not (other = (byte at ID: c, cell #addr at time t) + imm)

  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 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 i = a BEQ instruction that compares l and r with immediate imm
  • the PC at computer c and time t = i

  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 = a BEQ instruction that compares left and right with immediate imm
  • the PC at computer c and time t = i
  • byte at ID: c, cell #left at time t = byte at ID: c, cell #right at time t

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

  (link)
• if the following are true:
  • the instruction at computer c and index i = a BEQ instruction that compares left and right with immediate imm
  • the PC at computer c and time t = i
  • not (byte at ID: c, cell #left at time t = byte at ID: c, cell #right at time t)

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

  (link)
• if the following are true:
  • the instruction at computer c and index i = a jump instruction with 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 = a jump instruction with to: jump_to
  • the PC at computer c and time t = i

  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 = jump register instruction with addr: addr
  • the PC at computer c and time t = i

  then the PC at computer c and time (t + 1) = byte at ID: c, cell #addr at time t

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

  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 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)
• if the following are true:
  • the instruction at computer c and index x = an ADDI instruction with src: d imm: imm and dst: s
  • the PC at computer c and time t = x

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

  (link)
• if the following are true:
  • the instruction at computer c and index x = an add instruction with dst: s src1: d and src2: imm
  • the PC at computer c and time t = x

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

  (link)
• if the following are true:
  • the instruction at computer c and index x = subtract immediate instruction with dst: s src: d and immediate: imm
  • the PC at computer c and time t = x

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

  (link)
• if the following are true:
  • the instruction at computer c and index x = a STORE instruction with src: s address: d and immediate: imm
  • the PC at computer c and time t = x

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

  (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