Function Is Add-Immediate Instruction

The Is Add-Immediate Instruction function determines whether there is an add-immediate (ADDI) instruction at instruction #i with source src, immediate imm, and destination dst. If there is such an instruction, then the output is true. Otherwise, the output is false.

Format:

instruction #i is addi dst=dst src=src imm=imm

Input:

number i - instruction number
number dst - destination memory cell
number src - source memory cell (left operand)
number imm - constant value (right operand)

Output:

boolean - true if there is a matching instruction, else false

Details:

The ADDI instruction tells the computer to add a number stored in memory with a constant value. Using the Is Add-Immediate Instruction function, we can make claims about the computer's state. Consider the following simulator:
Instructions
Memory Cells
Program Counter Time
0 0
LW Computer Simulator

We can make the following claim:

instruction #2 is an ADDI instruction with src: 1 imm: 5 and dst: 2

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:

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


Comments

Please log in to add comments