-------------------------- MODULE CPU ----------------------------------------
EXTENDS Sequences, TLC
CONSTANTS REGS, \* the set of CPU registers (e.g. {r1, r2})
ADDRS, \* the set of memory addresses (e.g. {a1, a2})
DATA \* the set of primitive data values (e.g. {d1, d2})
\* Zero data value (other than ADDRS or DATA)
Zero == CHOOSE val : val \notin ADDRS \cup DATA
\* TLC symmetry optimisations
Perms ==
Permutations(REGS) \cup Permutations(ADDRS) \cup Permutations(DATA)
VARIABLES regs, \* CPU registers
mem, \* memory (virtual)
exception, \* exception status
cmd \* last executed command (debug)
cpu_vars == << regs, mem, exception >>
(* A memory location can store ADDRS or DATA or Zero *)
VALUES == ADDRS \cup DATA \cup {Zero}
CPUTypeOK ==
/\ regs \in [REGS -> VALUES]
/\ mem \in [ADDRS -> VALUES]
/\ exception \in BOOLEAN
(* Registers and memory are initialised to Zero *)
CPUInit ==
/\ regs = [r \in REGS |-> Zero]
/\ mem = [a \in ADDRS |-> Zero]
/\ exception = FALSE
/\ cmd = << >>
(* Executable CPU instructions *)
(* Move an immediate value to a register *)
MOVI(reg, imm) ==
/\ regs' = [regs EXCEPT ![reg] = imm]
/\ UNCHANGED << mem, exception >>
(* Move the value of a register to another *)
MOV(regt, regm) ==
/\ regs' = [regs EXCEPT ![regt] = regs[regm]]
/\ UNCHANGED << mem, exception >>
(* Load a value from memory at the address specified by regm into
regt. If the access is not permitted (invalid pointer), set the
exception state *)
LDR(regt, regm) ==
/\ LET pointer == regs[regm]
IN IF pointer \in ADDRS
THEN /\ regs' = [regs EXCEPT ![regt] = mem[pointer]]
/\ UNCHANGED exception
ELSE /\ exception' = TRUE
/\ UNCHANGED regs
/\ UNCHANGED mem
(* Store the value in regt to memory at the address specified by
regm. If the access is not permitted (invalid pointer), set the
exception state *)
STR(regt, regm) ==
/\ LET pointer == regs[regm]
IN IF pointer \in ADDRS
THEN /\ mem' = [mem EXCEPT ![pointer] = regs[regt]]
/\ UNCHANGED exception
ELSE /\ exception' = TRUE
/\ UNCHANGED mem
/\ UNCHANGED regs
(* Execute an instruction in the form << "name", arg1, arg2 >> *)
CPUExec(inst) ==
/\ CASE inst[1] = "movi" -> MOVI(inst[2], inst[3])
[] inst[1] = "mov" -> MOV(inst[2], inst[3])
[] inst[1] = "ldr" -> LDR(inst[2], inst[3])
[] inst[1] = "str" -> STR(inst[2], inst[3])
[] OTHER -> Assert(FALSE, << "Unknown instruction", inst[1] >>)
/\ cmd' = inst
------------------------------------------------------------------------------
CPUNext ==
\/ \E reg \in REGS, imm \in VALUES : CPUExec(<< "movi", reg, imm >>)
\/ \E regt, regm \in REGS : CPUExec(<< "mov", regt, regm >>)
\/ \E regt, regm \in REGS : CPUExec(<< "ldr", regt, regm >>)
\/ \E regt, regm \in REGS : CPUExec(<< "str", regt, regm >>)
CPUSpec == CPUInit /\ [][CPUNext]_<< cpu_vars, cmd >>
THEOREM CPUSpec => []CPUTypeOK
==============================================================================
\* CPU.cfg
CONSTANTS REGS = {r1, r2}
ADDRS = {a1, a2}
DATA = "" d2}
Zero = Zero
SYMMETRY Perms
VIEW cpu_vars
SPECIFICATION CPUSpec
INVARIANTS CPUTypeOK