Function Program Counter At Time

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

Format:

the PC at 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:

  • instruction #i is addi dst=dst src=src imm=imm
  • the PC at time t = i

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

  (link)

• if the following are true:

  • instruction #i is addi dst=dst src=src 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:

  • subtract immediate instruction with dst: dst src: src and immediate: imm at i
  • the PC at time t = i

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

  (link)

• if the following are true:

  • subtract immediate instruction with dst: dst src: src and immediate: imm at i
  • 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 #i is add dst=d src1=s1 src2=s2
  • the PC at time t = i

  then value of cell d at time (t + 1) = (value of cell s1 at time t) + (value of cell s2 at time t)

  (link)

• if the following are true:

  • instruction #i is add dst=d src1=s1 src2=s2
  • the PC at time t = i
  • not (other = d)

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

  (link)

• if the following are true:

  • instruction #i is store src=src addr=addr imm=imm
  • the PC at time t = i

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

  (link)

• if the following are true:

  • instruction #i is store src=src addr=addr imm=imm
  • the PC at time t = i
  • not (other = (value of cell addr at time t) + imm)

  then value of cell other at time (t + 1) = value of cell other 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

  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 #i is beq left=l right=r imm=imm
  • the PC at time t = i

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

  (link)

• if the following are true:

  • instruction #i is beq left=left right=right imm=imm
  • the PC at time t = i
  • value of cell left at time t = value of cell right at time t

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

  (link)

• if the following are true:

  • instruction #i is beq left=left right=right imm=imm
  • the PC at time t = i
  • not (value of cell left at time t = value of cell right at time t)

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

  (link)

• if the following are true:

  • instruction #i is jump imm=jump_to
  • the PC at time t = i

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

  (link)

• if the following are true:

  • instruction #i is jump imm=jump_to
  • the PC at time t = i

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

  (link)

• if the following are true:

  • instruction #i is jumpr addr=addr
  • the PC at time t = i

  then the PC at time (t + 1) = value of cell addr at time t

  (link)

• if the following are true:

  • instruction #i is jumpr addr=addr
  • the PC at time t = i

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

  (link)

• if the following are true:

  • instruction #i is a JAL instruction with jump to: jump_to
  • the PC at time t = i

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

  (link)

• if the following are true:

  • instruction #i is a JAL instruction with jump to: jump_to
  • the PC at time t = i
  • not (x = 2)

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

  (link)

• if the following are true:

  • instruction #i is a JAL instruction with jump to: jump_to
  • the PC at time t = i

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

  (link)

• if the following are true:

  • instruction #x is addi dst=s src=d imm=imm
  • the PC at time t = x

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

  (link)

• if the following are true:

  • instruction #x is add dst=s src1=d src2=imm
  • the PC at time t = x

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

  (link)

• if the following are true:

  • subtract immediate instruction with dst: s src: d and immediate: imm at x
  • the PC at time t = x

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

  (link)

• if the following are true:

  • instruction #x is store src=s addr=d imm=imm
  • the PC at time t = x

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

  (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)

• if interrupt at index: 0 time: t = 1, then the PC at time (t + 1) = 1

  (link)

• if interrupt at index: 1 time: t = 1, then the PC at time (t + 1) = 2

  (link)

Comments

Please log in to add comments