blob: c3c1f743aee0da099a2ab82bd99e99fb025ecb01 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
|
\section{Components}
Our chip consists of the following static components:
\begin{itemize}
\item An ALU: $\ALUOp \times \Word8 \times \Word8 \to \Word8$.
\item The program memory $\prog$: $\Prog \eqdef \Word4^{256}$.
\end{itemize}
And these volatile components:
\begin{itemize}
\item A memory $\mem$: $\Mem \eqdef \Word8^{256}$. Individual words or cells
are addressed with one word. We write $\mem.n$ for the cell in $\mem$ at
address $n$. We write $\update{\mem}{n\mapsto k}$ for the memory $\mem'$
with
$$
\mem'.i = \begin{cases}
k & \text{if $i=n$,}\\
\mem.i & \text{otherwise.}
\end{cases}
$$
\item The accumulators $\acc1$ and $\acc2$ are located at address $0$ and
$1$ of the memory, respectively.
\item The program counter $\pc$ is located at address $2$ of the memory.
\end{itemize}
A state $\st$ can be seen as a tuple $(\prog,\mem)$. We define the set of all
states $\State \eqdef \Word4^{256} \times \Word8^{256}$. An instruction is a
function $\Mem\to\Mem$. The instruction cycle is a function $\State\to\State$.
|
