Function Program Counter At

The Program Counter At Time function is the value of the program counter (PC) at time t

Format:

the PC at computer id and time t

Input:

Output:

Details:

The PC points to the next instruction that will be executed by the computer. For example, if the PC is set to 0, then instruction #0 is the next instruction that will execute. The PC value is located in the bottom table of the simulator. Try clicking Next a few times to see how the PC changes.

The PC starts at 0, then changes to 1, then to 2. What happens after that? The PC is set to 0 again, because that is what the JUMP instruction does to the PC. This shows that the PC does not always increment by 1.

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)
• if interrupt at computer: c index: 0 time: t = 1, then the PC at computer c and time (t + 1) = 1 (link)
• if interrupt at computer: c index: 1 time: t = 1, then the PC at computer c and time (t + 1) = 2 (link)
• if interrupt at computer: x index: 2 time: t = 1, then the PC at computer x and time (t + 1) = 3 (link)

Comments

Please log in to add comments