whitequark · Dec 29, 2018 · Dec 29, 2018 · Dec 30, 2018
diff --git a/doc/design.ods b/doc/design.ods
diff --git a/doc/images/logo-notext.svg b/doc/images/logo-notext.svg
diff --git a/doc/logo-parts.svg → doc/images/logo-parts.svg b/doc/logo-parts.svg → doc/images/logo-parts.svg
diff --git a/doc/logo.svg → doc/images/logo-text.svg b/doc/logo.svg → doc/images/logo-text.svg
diff --git a/doc/logo2blur.svg → doc/images/logo_toaru-blur.svg b/doc/logo2blur.svg → doc/images/logo_toaru-blur.svg
diff --git a/doc/logo2.svg → doc/images/logo_toaru.svg b/doc/logo2.svg → doc/images/logo_toaru.svg
diff --git a/doc/manual/.gitignore b/doc/manual/.gitignore
@@ -0,0 +1,5 @@
+*.aux
+*.log
+*.toc
+*.out
+*.cb*
diff --git a/doc/manual/build.sh b/doc/manual/build.sh
@@ -0,0 +1,5 @@
+#!/bin/sh -ex
+
+cd $(dirname $0)
+pdflatex -halt-on-error -interaction batchmode manual.tex
+pdflatex -halt-on-error -interaction batchmode manual.tex
diff --git a/doc/manual/insns/ADC.tex b/doc/manual/insns/ADC.tex
@@ -0,0 +1,17 @@
+\begin{instruction}{ADC}{Add Register with Carry}
+  \begin{encoding}
+    \mnemonic & \op{3}{000} & \op{2}{01} & \reg{d} & \reg{a} & \op{2}{01} & \reg{b} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, Rb}
+  \purpose{To add 16-bit integers in registers, with carry input.}
+  \restrictions{None.}
+  \begin{operation}\aluRR{opA + opB + C}\wb\flagZSCV\end{operation}
+  \begin{remarks}
+  A 32-bit addition with both operands in registers can be performed as follows:
+  \begin{alltt}
+  ; Perform (R1|R0) ← (R3|R2) + (R5|R4)
+  ADD  R0, R2, R4
+  ADC  R1, R3, R5
+  \end{alltt}
+  \end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/ADCI.tex b/doc/manual/insns/ADCI.tex
@@ -0,0 +1,21 @@
+\begin{instruction}{ADCI}{Add Immediate with Carry}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{001} & \op{2}{01} & \reg{d} & \reg{a} & \op{2}{01} & \imm{3} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{001} & \op{2}{01} & \reg{d} & \reg{a} & \op{2}{01} & \imm{3} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rd, Ra, imm}
+  \purpose{To add a constant to a 16-bit integer in a register, with carry input.}
+  \restrictions{None.}
+  \begin{operation}\aluRI{opA + opB + C}\wb\flagZSCV\end{operation}
+  \begin{remarks}
+  A 32-bit addition with a register and an immediate operand can be performed as follows:
+  \begin{alltt}
+  ; Perform (R1|R0) ← (R3|R2) + 0x40001
+  ADDI R0, R2, 1
+  ADCI R1, R3, 4
+  \end{alltt}
+  \end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/ADD.tex b/doc/manual/insns/ADD.tex
@@ -0,0 +1,9 @@
+\begin{instruction}{ADD}{Add Register}
+  \begin{encoding}
+    \mnemonic & \op{3}{000} & \op{2}{01} & \reg{d} & \reg{a} & \op{2}{00} & \reg{b} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, Rb}
+  \purpose{To add 16-bit integers in registers.}
+  \restrictions{None.}
+  \begin{operation}\aluRR{opA + opB}\wb\flagZSCV\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/ADDI.tex b/doc/manual/insns/ADDI.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{ADDI}{Add Immediate}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{001} & \op{2}{01} & \reg{d} & \reg{a} & \op{2}{00} & \imm{3} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{001} & \op{2}{01} & \reg{d} & \reg{a} & \op{2}{00} & \imm{3} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rd, Ra, imm}
+  \purpose{To add a constant to a 16-bit integer in a register.}
+  \restrictions{None.}
+  \begin{operation}\aluRI{opA + opB}\wb\flagZSCV\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/ADJW.1.tex b/doc/manual/insns/ADJW.1.tex
@@ -0,0 +1,16 @@
+\begin{instruction}{ADJW.1}{Adjust Window}
+  \begin{encoding}
+    \mnemonic & \op{3}{001} & \op{2}{11} & \bits{3}{000} & \bits{3}{000} & \op{2}{11} & \imm{3} \\
+  \end{encoding}
+  \assembly{ADJW size}
+  \purpose{To adjust the position of register window.}
+  \restrictions{None.}
+\begin{operation}
+\K{if} (has\_ext13)
+\K{then} imm ← ext13|imm3
+\K{else} imm ← sign\_extend(imm3)
+W ← W + imm
+\end{operation}
+  \begin{remarks}See also \insnref{LEAV}.\end{remarks}
+  \begin{notice}The exact encoding of this instruction is not final.\end{notice}
+\end{instruction}
diff --git a/doc/manual/insns/ADJW.2.tex b/doc/manual/insns/ADJW.2.tex
@@ -0,0 +1,18 @@
+\begin{instruction}{ADJW.2}{Adjust Window, Store Previous Address}
+  \begin{encoding}
+    \mnemonic & \op{3}{001} & \op{2}{11} & \reg{d} & \bits{3}{001} & \op{2}{11} & \imm{3} \\
+  \end{encoding}
+  \assembly{ADJW Rd, size}
+  \purpose{To adjust the position of register window and store the previous window position to a register.}
+  \restrictions{None.}
+\begin{operation}
+\K{if} (has\_ext13)
+\K{then} imm ← ext13|imm3
+\K{else} imm ← sign\_extend(imm3)
+tmp ← W
+W ← W + imm
+mem[W|Rd] ← tmp|000
+\end{operation}
+  \begin{remarks}See also \insnref{ENTR}.\end{remarks}
+  \begin{notice}The exact encoding of this instruction is not final.\end{notice}
+\end{instruction}
diff --git a/doc/manual/insns/AND.tex b/doc/manual/insns/AND.tex
@@ -0,0 +1,9 @@
+\begin{instruction}{AND}{Bitwise AND with Register}
+  \begin{encoding}
+    \mnemonic & \op{3}{000} & \op{2}{00} & \reg{d} & \reg{a} & \op{2}{00} & \reg{b} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, Rb}
+  \purpose{To perform bitwise AND between 16-bit integers in registers.}
+  \restrictions{None.}
+  \begin{operation}\aluRR{opA \K{and} opB}\wb\flagZS\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/ANDI.tex b/doc/manual/insns/ANDI.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{ANDI}{Bitwise AND with Immediate}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{001} & \op{2}{00} & \reg{d} & \reg{a} & \op{2}{00} & \imm{3} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{001} & \op{2}{00} & \reg{d} & \reg{a} & \op{2}{00} & \imm{3} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rd, Ra, imm}
+  \purpose{To perform bitwise AND between a constant and a 16-bit integer in a register.}
+  \restrictions{None.}
+  \begin{operation}\aluRI{opA \K{and} opB}\wb\flagZS\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/CMP.tex b/doc/manual/insns/CMP.tex
@@ -0,0 +1,10 @@
+\begin{instruction}{CMP}{Compare to Register}
+  \begin{encoding}
+    \mnemonic & \op{3}{000} & \op{2}{00} & \op{3}{000} & \reg{a} & \op{2}{11} & \reg{b} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, Rb}
+  \purpose{To compare 16-bit integers in registers.}
+  \restrictions{None.}
+  \begin{operation}\aluRR{opA - opB}\flagZSBV\end{operation}
+  \begin{remarks}This instruction is identical to \texttt{SUB}, with the exception that it discards the computed value.\end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/CMPI.tex b/doc/manual/insns/CMPI.tex
@@ -0,0 +1,14 @@
+\begin{instruction}{CMPI}{Compare to Immediate}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{001} & \op{2}{00} & \op{3}{000} & \reg{a} & \op{2}{11} & \imm{3} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{001} & \op{2}{00} & \op{3}{000} & \reg{a} & \op{2}{11} & \imm{3} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rd, Ra, imm}
+  \purpose{To compare a constant to a 16-bit integer in a register.}
+  \restrictions{None.}
+  \begin{operation}\aluRI{opA - opB}\flagZSBV\end{operation}
+  \begin{remarks}This instruction is identical to \texttt{SUBI}, with the exception that it discards the computed value.\end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/ENTR.tex b/doc/manual/insns/ENTR.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{ENTR}{Enter Frame}
+  \assembly{\mnemonic{} Rd, size}
+  \purpose{To set up a working area at an entry to a function.}
+  \restrictions{None.}
+  \begin{remarks}
+The assembler translates \texttt{\mnemonic} to
+\begin{alltt}
+  ADJW Rd, -size
+\end{alltt}
+
+See the description of \insnref{ADJW.2}. See also \insnref{LEAV}.
+  \end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/EXTI.tex b/doc/manual/insns/EXTI.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{EXTI}{Extend Immediate}
+  \begin{encoding}
+    \mnemonic & \op{3}{110} & \imm{13} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, Rb}
+  \purpose{To extend the range of immediate in the next executed instruction.}
+  \restrictions{None.}
+\begin{operation}
+ext13 ← imm13
+has_ext13 ← 1
+\end{operation}
+  \begin{remarks}This instruction is exclusively emitted by the assembler while translating other instructions. As it changes both the meaning of and the constraints placed on the immediate field in the following instruction, the assembler does not accept a mnemonic for \texttt{EXTI}.\end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/J.tex b/doc/manual/insns/J.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{J}{Jump}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1111} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1111} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To unconditionally transfer control.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}PC ← PC + 1 + off\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/JAL.tex b/doc/manual/insns/JAL.tex
@@ -0,0 +1,16 @@
+\begin{instruction}{JAL}{Jump And Link}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{100} & \op{2}{10} & \reg{d} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{100} & \op{2}{10} & \reg{d} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control to a subroutine.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}
+mem[W|Rd] ← PC + 1
+PC ← PC + 1 + off
+  \end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/JC.tex b/doc/manual/insns/JC.tex
@@ -0,0 +1,14 @@
+\begin{instruction}{JC}{Jump if Carry}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1010} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1010} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control if an arithmetic or shift operation resulted in unsigned overflow.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{C}\end{operation}
+  \begin{remarks}This instruction has the same encoding as \insnref{JUGE}.\end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/JE.tex b/doc/manual/insns/JE.tex
@@ -0,0 +1,14 @@
+\begin{instruction}{JE}{Jump if Equal}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1000} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1000} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control after a \texttt{\insnref{CMP} Ra, Rb} instruction if \texttt{Ra} is equal to \texttt{Rb}.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{Z}\end{operation}
+  \begin{remarks}This instruction has the same encoding as \insnref{JZ}.\end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/JN.tex b/doc/manual/insns/JN.tex
@@ -0,0 +1,14 @@
+\begin{instruction}{JN}{Jump Never}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0111} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0111} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To serve as a placeholder for a jump instruction.}
+  \input{jump-restrictions.tex}
+  \begin{operation}PC ← PC + 1\end{operation}
+  \begin{remarks}The \texttt{JN} instruction has no effect. It may be used as a placeholder for a different jump instruction with a predefiend offset when the exact condition is unknown, such as in certain self-modifying code.\end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/JNC.tex b/doc/manual/insns/JNC.tex
@@ -0,0 +1,14 @@
+\begin{instruction}{JNC}{Jump if Not Carry}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0010} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0010} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control if an arithmetic or shift operation did not result in unsigned overflow.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{\K{not} C}\end{operation}
+  \begin{remarks}This instruction has the same encoding as \insnref{JULT}.\end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/JNE.tex b/doc/manual/insns/JNE.tex
@@ -0,0 +1,14 @@
+\begin{instruction}{JNE}{Jump if Not Equal}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0000} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0000} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control after a \texttt{\insnref{CMP} Ra, Rb} instruction if \texttt{Ra} is not equal to \texttt{Rb}.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{\K{not} Z}\end{operation}
+  \begin{remarks}This instruction has the same encoding as \insnref{JNZ}.\end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/JNO.tex b/doc/manual/insns/JNO.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{JNO}{Jump if Not Overflow}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0011} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0011} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control if an arithmetic or shift operation did not result in signed overflow.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{\K{not} V}\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/JNS.tex b/doc/manual/insns/JNS.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{JNS}{Jump if Not Sign}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0001} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0001} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control if an arithmetic or shift operation produced a non-negative result.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{\K{not} S}\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/JNZ.tex b/doc/manual/insns/JNZ.tex
@@ -0,0 +1,14 @@
+\begin{instruction}{JNZ}{Jump if Not Zero}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0000} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0000} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control if an arithmetic or shift operation produced a non-zero result.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{\K{not} Z}\end{operation}
+  \begin{remarks}This instruction has the same encoding as \insnref{JNE}.\end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/JO.tex b/doc/manual/insns/JO.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{JO}{Jump if Overflow}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1011} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1011} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control if an arithmetic or shift operation resulted in signed overflow.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{V}\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/JR.tex b/doc/manual/insns/JR.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{JR}{Jump to Register}
+  \begin{encoding}
+    \mnemonic & \op{3}{101} & \op{2}{11} & \reg{a} & \bits{8}{00000000} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd}
+  \purpose{To transfer control to an absolute address contained in a register.}
+  \restrictions{None.}
+\begin{operation}
+addr ← mem[W|Ra]
+PC ← addr
+\end{operation}
+  \begin{notice}The exact encoding of this instruction is not final.\end{notice}
+\end{instruction}
diff --git a/doc/manual/insns/JS.tex b/doc/manual/insns/JS.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{JS}{Jump if Sign}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1001} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1001} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control if an arithmetic or shift operation produced a negative result.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{S}\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/JSGE.tex b/doc/manual/insns/JSGE.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{JSGE}{Jump if Signed Greater or Equal}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0101} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0101} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control after a \texttt{\insnref{CMP} Ra, Rb} instruction if \texttt{Ra} is greater than or equal to \texttt{Rb} when interpreted as signed integer.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{\K{not} (S \K{xor} V)}\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/JSGT.tex b/doc/manual/insns/JSGT.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{JSGT}{Jump if Signed Greater Than}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0110} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0110} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control after a \texttt{\insnref{CMP} Ra, Rb} instruction if \texttt{Ra} is greater than to \texttt{Rb} when interpreted as signed integer.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{\K{not} ((S \K{xor} V) \K{or} Z)}\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/JSLE.tex b/doc/manual/insns/JSLE.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{JSLE}{Jump if Signed Less or Equal}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1110} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1110} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control after a \texttt{\insnref{CMP} Ra, Rb} instruction if \texttt{Ra} is less than or equal to \texttt{Rb} when interpreted as signed integer.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{((S \K{xor} V) \K{or} Z)}\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/JSLT.tex b/doc/manual/insns/JSLT.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{JSLT}{Jump if Signed Less Than}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1101} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1101} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control after a \texttt{\insnref{CMP} Ra, Rb} instruction if \texttt{Ra} is less than \texttt{Rb} when interpreted as signed integer.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{(S \K{xor} V)}\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/JUGE.tex b/doc/manual/insns/JUGE.tex
@@ -0,0 +1,14 @@
+\begin{instruction}{JUGE}{Jump if Unsigned Greater or Equal}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1010} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1010} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control after a \texttt{\insnref{CMP} Ra, Rb} instruction if \texttt{Ra} is greater than or equal to \texttt{Rb} when interpreted as unsigned integer.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{C}\end{operation}
+  \begin{remarks}This instruction has the same encoding as \insnref{JC}.\end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/JUGT.tex b/doc/manual/insns/JUGT.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{JUGT}{Jump if Unsigned Greater Than}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0110} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0110} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control after a \texttt{\insnref{CMP} Ra, Rb} instruction if \texttt{Ra} is greater than to \texttt{Rb} when interpreted as unsigned integer.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{\K{not} ((\K{not} C) \K{or} V)}\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/JULE.tex b/doc/manual/insns/JULE.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{JULE}{Jump if Unsigned Less or Equal}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1110} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1110} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control after a \texttt{\insnref{CMP} Ra, Rb} instruction if \texttt{Ra} is less than or equal to \texttt{Rb} when interpreted as unsigned integer.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{(\K{not} C) \K{or} V}\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/JULT.tex b/doc/manual/insns/JULT.tex
@@ -0,0 +1,14 @@
+\begin{instruction}{JULT}{Jump if Unsigned Less Than}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0010} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{0010} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control after a \texttt{\insnref{CMP} Ra, Rb} instruction if \texttt{Ra} is less than \texttt{Rb} when interpreted as unsigned integer.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{\K{not} C}\end{operation}
+  \begin{remarks}This instruction has the same encoding as \insnref{JNC}.\end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/JZ.tex b/doc/manual/insns/JZ.tex
@@ -0,0 +1,14 @@
+\begin{instruction}{JZ}{Jump if Zero}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1000} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{101} & \op{1}{1} & \op{4}{1000} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} label}
+  \purpose{To transfer control if an arithmetic or shift operation produced a zero result.}
+  \input{jump-restrictions.tex}
+  \begin{operation}\off{8}\jump{Z}\end{operation}
+  \begin{remarks}This instruction has the same encoding as \insnref{JE}.\end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/LD.tex b/doc/manual/insns/LD.tex
@@ -0,0 +1,17 @@
+\begin{instruction}{LD}{Load with Address in Register}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{010} & \op{2}{00} & \reg{d} & \reg{a} & \off{5} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{010} & \op{2}{00} & \reg{d} & \reg{a} & \off{5} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rd, Ra, off}
+  \purpose{To load a word from memory at an absolute address contained in a register, with a constant offset.}
+  \input{mem-restrictions.tex}
+\begin{operation}\off{5}
+addr ← mem[W|Ra] + off
+temp ← mem[addr]
+mem[W|Rd] ← temp
+\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/LDI.tex b/doc/manual/insns/LDI.tex
@@ -0,0 +1,17 @@
+\begin{instruction}{LDI}{Load PC-relative with Immediate Offset}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{011} & \op{2}{00} & \reg{d} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{011} & \op{2}{00} & \reg{d} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rd, off}
+  \purpose{To load a word from memory at an address relative to PC with a constant offset.}
+  \input{memi-restrictions.tex}
+\begin{operation}\off{8}
+addr ← PC + off
+temp ← mem[addr]
+mem[W|Rd] ← temp
+\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/LDX.tex b/doc/manual/insns/LDX.tex
@@ -0,0 +1,17 @@
+\begin{instruction}{LDX}{Load External with Address in Register}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{010} & \op{2}{10} & \reg{d} & \reg{a} & \off{5} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{010} & \op{2}{10} & \reg{d} & \reg{a} & \off{5} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rd, Ra, off}
+  \purpose{To complete a load cycle on external bus at an absolute address contained in a register, with a constant offset.}
+  \input{mem-restrictions.tex}
+\begin{operation}\off{5}
+addr ← mem[W|Ra] + off
+temp ← ext[addr]
+mem[W|Rd] ← temp
+\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/LDXI.tex b/doc/manual/insns/LDXI.tex
@@ -0,0 +1,16 @@
+\begin{instruction}{LDXI}{Load External with Immediate Address}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{011} & \op{2}{10} & \reg{d} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{011} & \op{2}{10} & \reg{d} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rd, off}
+  \purpose{To complete a load cycle on external bus at a constant absolute address.}
+  \input{memi-restrictions.tex}
+\begin{operation}\off{8}
+temp ← ext[off]
+mem[W|Rd] ← temp
+\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/LEAV.tex b/doc/manual/insns/LEAV.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{LEAV}{Leave Frame}
+  \assembly{\mnemonic{} Rd, size}
+  \purpose{To tear down a working area at an exit from a function.}
+  \restrictions{None.}
+  \begin{remarks}
+The assembler translates \texttt{\mnemonic} to
+\begin{alltt}
+  ADJW size
+\end{alltt}
+
+See the description of \insnref{ADJW.1}. See also \insnref{ENTR}.
+  \end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/MOV.tex b/doc/manual/insns/MOV.tex
@@ -0,0 +1,12 @@
+\begin{instruction}{MOV}{Move}
+  \assembly{\mnemonic{} Rd, Rs}
+  \purpose{To move a value from register to register.}
+  \restrictions{None.}
+  \begin{remarks}
+The assembler does not translate any instructions for \texttt{\mnemonic} with identical \texttt{Rd} and \texttt{Rs}, and translates \texttt{\mnemonic} with any other register combination to
+\begin{alltt}
+  ANDI Rd, Rs, Rs
+\end{alltt}
+  \end{remarks}
+  \begin{notice}The exact translation of this mnemonic is not final.\end{notice}
+\end{instruction}
diff --git a/doc/manual/insns/MOVA.tex b/doc/manual/insns/MOVA.tex
@@ -0,0 +1,15 @@
+\begin{instruction}{MOVA}{Move Address PC-relative}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{100} & \op{2}{00} & \reg{d} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{100} & \op{2}{00} & \reg{d} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rd, off}
+  \purpose{To load a register with an address relative to PC with a constant offset..}
+  \restrictions{If the long form is used, and \texttt{off8[8:3]} are non-zero, the behavior is \unpredictable.}
+  \begin{operation}\off{8}
+mem[W|Rd] ← PC + 1 + off
+  \end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/MOVI.tex b/doc/manual/insns/MOVI.tex
@@ -0,0 +1,18 @@
+\begin{instruction}{MOVI}{Move Immediate}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{100} & \op{2}{01} & \reg{d} & \imm{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{100} & \op{2}{01} & \reg{d} & \imm{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rd, imm}
+  \purpose{To load a register with a constant.}
+  \restrictions{If the long form is used, and \texttt{off8[8:3]} are non-zero, the behavior is \unpredictable.}
+  \begin{operation}
+\K{if} (has\_ext13)
+\K{then} imm ← ext13|imm8[3:0]
+\K{else} imm ← sign\_extend(imm8)
+mem[W|Rd] ← imm
+  \end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/OR.tex b/doc/manual/insns/OR.tex
@@ -0,0 +1,9 @@
+\begin{instruction}{OR}{Bitwise OR with Register}
+  \begin{encoding}
+    \mnemonic & \op{3}{000} & \op{2}{00} & \reg{d} & \reg{a} & \op{2}{01} & \reg{b} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, Rb}
+  \purpose{To perform bitwise OR between 16-bit integers in registers.}
+  \restrictions{None.}
+  \begin{operation}\aluRR{opA \K{or} opB}\wb\flagZS\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/ORI.tex b/doc/manual/insns/ORI.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{ORI}{Bitwise OR with Immediate}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{001} & \op{2}{00} & \reg{d} & \reg{a} & \op{2}{01} & \imm{3} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{001} & \op{2}{00} & \reg{d} & \reg{a} & \op{2}{01} & \imm{3} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rd, Ra, imm}
+  \purpose{To perform bitwise OR between a constant and a 16-bit integer in a register.}
+  \restrictions{None.}
+  \begin{operation}\aluRI{opA \K{or} opB}\wb\flagZS\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/ROLI.tex b/doc/manual/insns/ROLI.tex
@@ -0,0 +1,6 @@
+\begin{instruction}{ROLI}{Rotate Left Immediate}
+  \assembly{\mnemonic{} Rd, Ra, amount}
+  \purpose{To perform a left rotate of a 16-bit integer in a register by a constant bit amount.}
+  \restrictions{The \texttt{amount} may be between 0 and 15, inclusive.}
+  \begin{remarks}This instruction is an alias for \insnref{ROTI}.\end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/RORI.tex b/doc/manual/insns/RORI.tex
@@ -0,0 +1,15 @@
+\begin{instruction}{RORI}{Rotate Right Immediate}
+  \assembly{\mnemonic{} Rd, Ra, amount}
+  \purpose{To perform a right rotate of a 16-bit integer in a register by a constant bit amount.}
+  \restrictions{The \texttt{amount} may be between 0 and 15, inclusive.}
+  \begin{remarks}
+The assembler translates \texttt{\mnemonic} with \texttt{amount} of 0 to
+\begin{alltt}
+  MOV  Rd, Ra
+\end{alltt}
+and \texttt{\mnemonic} with any other \texttt{amount} to
+\begin{alltt}
+  ROTI Rd, Rd, (15 - amount)
+\end{alltt}
+  \end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/ROT.tex b/doc/manual/insns/ROT.tex
@@ -0,0 +1,9 @@
+\begin{instruction}{ROT}{Rotate}
+  \begin{encoding}
+    \mnemonic & \op{3}{000} & \op{2}{10} & \reg{d} & \reg{a} & \op{2}{01} & \reg{b} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, Rb}
+  \purpose{To perform a left rotate of a 16-bit integer in a register by a variable bit amount.}
+  \input{shift-restrictions.tex}
+  \begin{operation}\aluRR{opA[16-opB:0]|opA[16:16-opB]}\wb\flagZS\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/ROTI.tex b/doc/manual/insns/ROTI.tex
@@ -0,0 +1,10 @@
+\begin{instruction}{ROTI}{Rotate Immediate}
+  \begin{encoding}
+    \mnemonic & \op{3}{001} & \op{2}{10} & \reg{d} & \reg{a} & \op{2}{01} & \imm{3} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, amount}
+  \purpose{To perform a left rotate of a 16-bit integer in a register by a constant bit amount.}
+  \restrictions{The \texttt{amount} may be between 0 and 15, inclusive.}
+  \begin{operation}\aluR{opA[15-imm3:0]|opA[16:15-imm3]}\wb\flagZS\end{operation}
+  \input{shift-remark.tex}
+\end{instruction}
diff --git a/doc/manual/insns/SBB.tex b/doc/manual/insns/SBB.tex
@@ -0,0 +1,17 @@
+\begin{instruction}{SBB}{Subtract Register with Borrow}
+  \begin{encoding}
+    \mnemonic & \op{3}{000} & \op{2}{01} & \reg{d} & \reg{a} & \op{2}{11} & \reg{b} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, Rb}
+  \purpose{To subtract 16-bit integers in registers, with borrow input.}
+  \restrictions{None.}
+  \begin{operation}\aluRR{opA - opB - \K{not} C}\wb\flagZSBV\end{operation}
+  \begin{remarks}
+  A 32-bit subtraction with both operands in registers can be performed as follows:
+  \begin{alltt}
+  ; Perform (R1|R0) ← (R3|R2) - (R5|R4)
+  SUB  R0, R2, R4
+  SBB  R1, R3, R5
+  \end{alltt}
+  \end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/SBBI.tex b/doc/manual/insns/SBBI.tex
@@ -0,0 +1,21 @@
+\begin{instruction}{SBBI}{Subtract Immediate with Borrow}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{001} & \op{2}{01} & \reg{d} & \reg{a} & \op{2}{11} & \imm{3} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{001} & \op{2}{01} & \reg{d} & \reg{a} & \op{2}{11} & \imm{3} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rd, Ra, imm}
+  \purpose{To subtract a constant from a 16-bit integer in a register, with borrow input.}
+  \restrictions{None.}
+  \begin{operation}\aluRI{opA - opB - \K{not} C}\wb\flagZSBV\end{operation}
+  \begin{remarks}
+  A 32-bit subtraction with a register and an immediate operand can be performed as follows:
+  \begin{alltt}
+  ; Perform (R1|R0) ← (R3|R2) - 0x40001
+  SUBI R0, R2, 1
+  SBBI R1, R3, 4
+  \end{alltt}
+  \end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/SLL.tex b/doc/manual/insns/SLL.tex
@@ -0,0 +1,9 @@
+\begin{instruction}{SLL}{Shift Left Logical}
+  \begin{encoding}
+    \mnemonic & \op{3}{000} & \op{2}{10} & \reg{d} & \reg{a} & \op{2}{00} & \reg{b} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, Rb}
+  \purpose{To perform a left logical shift of a 16-bit integer in a register by a variable bit amount.}
+  \input{shift-restrictions.tex}
+  \begin{operation}\aluRR{opA[16-opB:0]|0\string{opB\string}}\wb\flagZS\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/SLLI.tex b/doc/manual/insns/SLLI.tex
@@ -0,0 +1,10 @@
+\begin{instruction}{SLLI}{Shift Left Logical Immediate}
+  \begin{encoding}
+    \mnemonic & \op{3}{001} & \op{2}{10} & \reg{d} & \reg{a} & \op{2}{00} & \imm{3} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, amount}
+  \purpose{To perform a left logical shift of a 16-bit integer in a register by a constant bit amount.}
+  \restrictions{The \texttt{amount} may be between 0 and 15, inclusive.}
+  \begin{operation}\aluR{opA[15-imm3:0]|0\string{imm3+1\string}}\wb\flagZS\end{operation}
+  \input{shift-remark.tex}
+\end{instruction}
diff --git a/doc/manual/insns/SRA.tex b/doc/manual/insns/SRA.tex
@@ -0,0 +1,9 @@
+\begin{instruction}{SRA}{Shift Right Arithmetical}
+  \begin{encoding}
+    \mnemonic & \op{3}{000} & \op{2}{10} & \reg{d} & \reg{a} & \op{2}{11} & \reg{b} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, Rb}
+  \purpose{To perform a right arithmetical shift of a 16-bit integer in a register by a variable bit amount.}
+  \input{shift-restrictions.tex}
+  \begin{operation}\aluRR{opA[15]\string{opB\string}|opA[16:16-opB]}\wb\flagZS\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/SRAI.tex b/doc/manual/insns/SRAI.tex
@@ -0,0 +1,10 @@
+\begin{instruction}{SRAI}{Shift Right Arithmetical Immediate}
+  \begin{encoding}
+    \mnemonic & \op{3}{000} & \op{2}{10} & \reg{d} & \reg{a} & \op{2}{11} & \imm{3} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, amount}
+  \purpose{To perform a right arithmetical shift of a 16-bit integer in a register by a constant bit amount.}
+  \restrictions{The \texttt{amount} may be between 0 and 15, inclusive.}
+  \begin{operation}\aluRR{opA[15]\string{imm3+1\string}|opA[16:15-imm3]}\wb\flagZS\end{operation}
+  \input{shift-remark.tex}
+\end{instruction}
diff --git a/doc/manual/insns/SRL.tex b/doc/manual/insns/SRL.tex
@@ -0,0 +1,9 @@
+\begin{instruction}{SRL}{Shift Right Logical}
+  \begin{encoding}
+    \mnemonic & \op{3}{000} & \op{2}{10} & \reg{d} & \reg{a} & \op{2}{10} & \reg{b} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, Rb}
+  \purpose{To perform a right logical shift of a 16-bit integer in a register by a variable bit amount.}
+  \input{shift-restrictions.tex}
+  \begin{operation}\aluRR{0\string{opB\string}|opA[16:16-opB]}\wb\flagZS\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/SRLI.tex b/doc/manual/insns/SRLI.tex
@@ -0,0 +1,10 @@
+\begin{instruction}{SRLI}{Shift Right Logical Immediate}
+  \begin{encoding}
+    \mnemonic & \op{3}{001} & \op{2}{10} & \reg{d} & \reg{a} & \op{2}{10} & \imm{3} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, amount}
+  \purpose{To perform a right logical shift of a 16-bit integer in a register by a constant bit amount.}
+  \restrictions{The \texttt{amount} may be between 0 and 15, inclusive.}
+  \begin{operation}\aluR{0\string{imm3+1\string}|opA[16:15-imm3]}\wb\flagZS\end{operation}
+  \input{shift-remark.tex}
+\end{instruction}
diff --git a/doc/manual/insns/ST.tex b/doc/manual/insns/ST.tex
@@ -0,0 +1,17 @@
+\begin{instruction}{ST}{Store with Address in Register}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{010} & \op{2}{01} & \reg{s} & \reg{a} & \off{5} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{010} & \op{2}{01} & \reg{s} & \reg{a} & \off{5} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rs, Ra, off}
+  \purpose{To store a word to memory at an absolute address contained in a register, with a constant offset.}
+  \input{mem-restrictions.tex}
+\begin{operation}\off{5}
+addr ← mem[W|Ra] + off
+temp ← mem[W|Rs]
+mem[addr] ← temp
+\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/STI.tex b/doc/manual/insns/STI.tex
@@ -0,0 +1,17 @@
+\begin{instruction}{STI}{Store PC-relative with Immediate Offset}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{011} & \op{2}{01} & \reg{s} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{011} & \op{2}{01} & \reg{s} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rs, off}
+  \purpose{To store a word to memory at an address relative to PC with a constant offset.}
+  \input{memi-restrictions.tex}
+\begin{operation}\off{8}
+addr ← PC + off
+temp ← mem[W|Rs]
+mem[addr] ← temp
+\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/STX.tex b/doc/manual/insns/STX.tex
@@ -0,0 +1,17 @@
+\begin{instruction}{STX}{Store External with Address in Register}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{010} & \op{2}{11} & \reg{s} & \reg{a} & \off{5} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{010} & \op{2}{11} & \reg{s} & \reg{a} & \off{5} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rs, Ra, off}
+  \purpose{To complete a store cycle on external bus at an absolute address contained in a register, with a constant offset.}
+  \input{mem-restrictions.tex}
+\begin{operation}\off{5}
+addr ← mem[W|Ra] + off
+temp ← mem[W|Rs]
+ext[addr] ← temp
+\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/STXI.tex b/doc/manual/insns/STXI.tex
@@ -0,0 +1,16 @@
+\begin{instruction}{STXI}{Store External with Immediate Address}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{011} & \op{2}{11} & \reg{s} & \off{8} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{011} & \op{2}{11} & \reg{s} & \off{8} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rs, off}
+  \purpose{To complete a store cycle on external bus at a constant absolute address.}
+  \input{mem-restrictions.tex}
+\begin{operation}\off{8}
+temp ← mem[W|Rs]
+ext[off] ← temp
+\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/SUB.tex b/doc/manual/insns/SUB.tex
@@ -0,0 +1,9 @@
+\begin{instruction}{SUB}{Subtract Register}
+  \begin{encoding}
+    \mnemonic & \op{3}{000} & \op{2}{01} & \reg{d} & \reg{a} & \op{2}{10} & \reg{b} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, Rb}
+  \purpose{To subtract 16-bit integers in registers.}
+  \restrictions{None.}
+  \begin{operation}\aluRR{opA - opB}\wb\flagZSBV\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/SUBI.tex b/doc/manual/insns/SUBI.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{SUBI}{Subtract Immediate}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{001} & \op{2}{01} & \reg{d} & \reg{a} & \op{2}{10} & \imm{3} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{001} & \op{2}{01} & \reg{d} & \reg{a} & \op{2}{10} & \imm{3} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rd, Ra, imm}
+  \purpose{To subtract a constant from a 16-bit integer in a register.}
+  \restrictions{None.}
+  \begin{operation}\aluRI{opA - opB}\wb\flagZSBV\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/XCHG.tex b/doc/manual/insns/XCHG.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{XCHG}{Exchange Registers}
+  \assembly{\mnemonic{} Ra, Rb}
+  \purpose{To exchange the values of two registers.}
+  \restrictions{None.}
+  \begin{remarks}
+The assembler does not translate any instructions for \texttt{\mnemonic} with identical \texttt{Ra} and \texttt{Rb}, and translates \texttt{\mnemonic} with any other register combination to
+\begin{alltt}
+  XOR  Ra, Ra, Rb
+  XOR  Rb, Rb, Ra
+  XOR  Ra, Ra, Rb
+\end{alltt}
+  \end{remarks}
+\end{instruction}
diff --git a/doc/manual/insns/XOR.tex b/doc/manual/insns/XOR.tex
@@ -0,0 +1,9 @@
+\begin{instruction}{XOR}{Bitwise XOR with Register}
+  \begin{encoding}
+    \mnemonic & \op{3}{000} & \op{2}{00} & \reg{d} & \reg{a} & \op{2}{10} & \reg{b} \\
+  \end{encoding}
+  \assembly{\mnemonic{} Rd, Ra, Rb}
+  \purpose{To perform bitwise XOR between 16-bit integers in registers.}
+  \restrictions{None.}
+  \begin{operation}\aluRR{opA \K{xor} opB}\wb\flagZS\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/XORI.tex b/doc/manual/insns/XORI.tex
@@ -0,0 +1,13 @@
+\begin{instruction}{XORI}{Bitwise XOR with Immediate}
+  \begin{encoding*}{short}
+    \mnemonic & \op{3}{001} & \op{2}{00} & \reg{d} & \reg{a} & \op{2}{10} & \imm{3} \\
+  \end{encoding*}
+  \begin{encoding*}{long}
+    \exti
+    \mnemonic & \op{3}{001} & \op{2}{00} & \reg{d} & \reg{a} & \op{2}{10} & \imm{3} \\
+  \end{encoding*}
+  \assembly{\mnemonic{} Rd, Ra, imm}
+  \purpose{To perform bitwise XOR between a constant and a 16-bit integer in a register.}
+  \restrictions{None.}
+  \begin{operation}\aluRI{opA \K{xor} opB}\wb\flagZS\end{operation}
+\end{instruction}
diff --git a/doc/manual/insns/index.tex b/doc/manual/insns/index.tex
@@ -0,0 +1,196 @@
+\def←{$\leftarrow$}
+
+\newcommand{\insnref}[1]{\hyperref[insn:#1]{\texttt{#1}}}
+
+\newenvironment{instruction}[2]{
+  \subsection[#1 (#2)]{#1 \hfill #2}
+  \label{insn:#1}
+  \vspace{0.5cm}
+
+  \newcommand{\mnemonic}{#1}
+
+  \newcommand{\field}[1]{\par\textbf{##1:}\par}
+  \newcommand{\fieldindent}[2]{\field{##1}\begin{adjustwidth}{10pt}{0pt}##2\end{adjustwidth}}
+
+  \newenvironment{encoding}[1][Encoding]{
+    \newcommand{\bits}[2]{\multicolumn{####1}{c|}{####2}}
+    \newcommand{\op}[2]{\bits{####1}{\texttt{####2}}}
+    \newcommand{\reg}[1]{\bits{3}{R####1}}
+    \newcommand{\imm}[1]{\bits{####1}{imm####1}}
+    \newcommand{\off}[1]{\bits{####1}{off####1}}
+    \newcommand{\exti}{EXTI & \op{3}{110} & \bits{13}{ext13} \\ \cline{2-17}}
+
+    \field{##1}
+    \begin{adjustwidth}{10pt}{0pt}
+    \begin{tabular}{R{2cm}|*{16}{c|}}
+    \cline{2-17}
+    & F & E & D & C & B & A & 9 & 8 & 7 & 6 & 5 & 4 & 3 & 2 & 1 & 0 \\
+    \cline{2-17}
+  }{
+    \cline{2-17}
+    \end{tabular}
+    \end{adjustwidth}
+  }
+  \newenvironment{encoding*}[1]{
+    \begin{encoding}[Encoding (##1 form)]
+  }{
+    \end{encoding}
+  }
+
+  \newcommand{\assembly}[1]{\fieldindent{Assembly}{\texttt{##1}}}
+
+  \newcommand{\purpose}[1]{\fieldindent{Purpose}{##1}}
+
+  % Restrictions often include \unpredictable, which tends to mess with line break algorithm,
+  % so we turn off hyphenation for these paragraphs with \raggedright.
+  \newcommand{\restrictions}[1]{\fieldindent{Restrictions}{\raggedright##1}}
+
+  \newenvironment{operation}{
+    \newcommand{\K}[1]{\textbf{####1}}
+
+    \newcommand{\aluR}[1]{\begin{alltt}
+    opA ← mem[W|Ra]\\
+    res ← ####1
+    \end{alltt}}
+
+    \newcommand{\aluRR}[1]{\begin{alltt}
+    opA ← mem[W|Ra]\\
+    opB ← mem[W|Rb]\\
+    res ← ####1
+    \end{alltt}}
+
+    \newcommand{\aluRI}[1]{
+    \begin{alltt}
+    opA ← mem[W|Ra]\\
+    \K{if} (has\_ext13)\\
+    \K{then} opB ← ext13|imm3\\
+    \K{else} opB ← decode\_immediate(imm3)\\
+    res ← ####1
+    \end{alltt}}
+
+    \newcommand{\wb}{mem[W|Rd] ← res}
+
+    \newcommand{\flagZS}{\begin{alltt}
+    Z ← res = 0\\
+    S ← res[15]\\
+    C ← \undefined\\
+    V ← \undefined
+    \end{alltt}}
+
+    \newcommand{\flagZSCV}{\begin{alltt}
+    Z ← res = 0\\
+    S ← res[15]\\
+    C ← res[16]\\
+    V ← (opA[15] = opB[15]) \K{and} (opA[15] <> res[15])
+    \end{alltt}}
+
+    \newcommand{\flagZSBV}{\begin{alltt}
+    Z ← res = 0\\
+    S ← res[15]\\
+    C ← \K{not} res[16]\\
+    V ← (opA[15] = \K{not} opB[15]) \K{and} (opA[15] <> res[15])
+    \end{alltt}}
+
+    \newcommand{\off}[1]{\begin{alltt}
+    \K{if} (has\_ext13)\\
+    \K{then} off ← ext13|off{####1}[3:0]\\
+    \K{else} off ← sign\_extend(off{####1})
+    \end{alltt}}
+
+    \newcommand{\jump}[1]{\begin{alltt}
+    \K{if} (####1)\\
+    \K{then} PC ← PC + 1 + off\\
+    \K{else} PC ← PC + 1
+    \end{alltt}}
+
+    \field{Operation}
+    \begin{adjustwidth}{10pt}{0pt}
+    \begin{alltt}%
+  }{%
+    \end{alltt}
+    \end{adjustwidth}
+  }
+
+  \newenvironment{remarks}{
+    \field{Remarks}
+    \begin{adjustwidth}{10pt}{0pt}
+  }{
+    \end{adjustwidth}
+  }
+
+  \newenvironment{notice}{
+    \cbcolor{red}
+    \par\textbf{Notice:}\cbstart\par
+  }{
+    \cbend
+  }
+}{
+  \pagebreak
+}
+
+\input{ADC.tex}
+\input{ADCI.tex}
+\input{ADD.tex}
+\input{ADDI.tex}
+\input{ADJW.1.tex}
+\input{ADJW.2.tex}
+\input{AND.tex}
+\input{ANDI.tex}
+\input{CMP.tex}
+\input{CMPI.tex}
+\input{ENTR.tex} % pseudo
+\input{EXTI.tex}
+\input{J.tex}
+\input{JAL.tex}
+\input{JC.tex}
+\input{JE.tex} % pseudo
+\input{JN.tex}
+\input{JNC.tex}
+\input{JNE.tex} % pseudo
+\input{JNO.tex}
+\input{JNS.tex}
+\input{JNZ.tex}
+\input{JO.tex}
+\input{JR.tex}
+\input{JS.tex}
+\input{JSGE.tex}
+\input{JSGT.tex}
+\input{JSLE.tex}
+\input{JSLT.tex}
+\input{JUGE.tex} % pseudo
+\input{JUGT.tex}
+\input{JULE.tex}
+\input{JULT.tex} % pseudo
+\input{JZ.tex}
+\input{LD.tex}
+\input{LDI.tex}
+\input{LDX.tex}
+\input{LDXI.tex}
+\input{LEAV.tex} % pseudo
+\input{MOV.tex} % pseudo
+\input{MOVA.tex}
+\input{MOVI.tex}
+\input{OR.tex}
+\input{ORI.tex}
+\input{ROLI.tex} % pseudo
+\input{RORI.tex} % pseudo
+\input{ROT.tex}
+\input{ROTI.tex}
+\input{SBB.tex}
+\input{SBBI.tex}
+\input{SLL.tex}
+\input{SLLI.tex}
+\input{SRA.tex}
+\input{SRAI.tex}
+\input{SRL.tex}
+\input{SRLI.tex}
+\input{ST.tex}
+\input{STI.tex}
+\input{STX.tex}
+\input{STXI.tex}
+\input{SUB.tex}
+\input{SUBI.tex}
+% \input{SWPW.tex}
+\input{XCHG.tex} % pseudo
+\input{XOR.tex}
+\input{XORI.tex}
diff --git a/doc/manual/insns/jump-restrictions.tex b/doc/manual/insns/jump-restrictions.tex
@@ -0,0 +1 @@
+\restrictions{If the long form is used, and \texttt{off8[8:3]} are non-zero, the behavior is \unpredictable.}
diff --git a/doc/manual/insns/mem-restrictions.tex b/doc/manual/insns/mem-restrictions.tex
@@ -0,0 +1 @@
+\restrictions{If the long form is used, and \texttt{off5[5:3]} are non-zero, the behavior is \unpredictable.}
diff --git a/doc/manual/insns/memi-restrictions.tex b/doc/manual/insns/memi-restrictions.tex
@@ -0,0 +1 @@
+\restrictions{If the long form is used, and \texttt{off8[8:3]} are non-zero, the behavior is \unpredictable.}
diff --git a/doc/manual/insns/shift-remark.tex b/doc/manual/insns/shift-remark.tex
@@ -0,0 +1,11 @@
+\begin{remarks}
+The instruction encoding allows directly representing any \texttt{amount} between 1 and 8, inclusive. The assembler translates \texttt{\mnemonic} with \texttt{amount} of 0 to
+\begin{alltt}
+  MOV  Rd, Ra
+\end{alltt}
+and \texttt{\mnemonic} with \texttt{amount} greater than 8 to
+\begin{alltt}
+  \mnemonic Rd, Ra, 8
+  \mnemonic Rd, Rd, (amount - 8)
+\end{alltt}
+\end{remarks}
diff --git a/doc/manual/insns/shift-restrictions.tex b/doc/manual/insns/shift-restrictions.tex
@@ -0,0 +1 @@
+\restrictions{If \texttt{Rb} contains a value greater than 15, the behavior is \unpredictable.}
diff --git a/doc/manual/manual.pdf b/doc/manual/manual.pdf
diff --git a/doc/manual/manual.tex b/doc/manual/manual.tex
@@ -0,0 +1,57 @@
+\documentclass[12pt,a4paper]{article}
+\usepackage[hmargin=3cm,vmargin=2.5cm]{geometry}
+\usepackage[utf8]{inputenc}
+\usepackage{import}
+\usepackage{parskip}
+\usepackage{color}
+\usepackage[color,leftbars]{changebar}
+\usepackage{ragged2e}
+\usepackage{changepage}
+\usepackage{alltt}
+\renewcommand{\ttdefault}{txtt}
+\usepackage{array}
+\newcolumntype{L}[1]{>{\raggedright\let\newline\\\arraybackslash\hspace{0pt}}m{#1}}
+\newcolumntype{C}[1]{>{\centering\let\newline\\\arraybackslash\hspace{0pt}}m{#1}}
+\newcolumntype{R}[1]{>{\raggedleft\let\newline\\\arraybackslash\hspace{0pt}}m{#1}}
+\usepackage{hyperref}
+\hypersetup{
+  colorlinks=true,
+  linkcolor=blue,
+  pdfstartview=Fit,
+  pdfpagemode=UseOutlines,
+}
+
+\newcommand{\undefined}{\textbf{UNDEFINED}}
+\newcommand{\unpredictable}{\textbf{UNPREDICTABLE}}
+\uchyph=0
+
+\begin{document}
+
+\begin{titlepage}
+  \centering
+  \vspace*{6cm}
+  \par{\Huge Boneless-III}
+  \vspace{1cm}
+  \par{\Huge Architecture Reference Manual}
+\end{titlepage}
+
+\tableofcontents
+\addcontentsline{toc}{section}{Table of Contents}
+\pagebreak
+
+\setcounter{tocdepth}{2}
+
+\section{Guide to Instruction Set}
+TBD
+\pagebreak
+
+\section{List of Instructions}
+
+The following pages provide a detailed description of instructions, arranged in alphabetical order.
+
+Executing any instruction with an encoding not present on the following pages has \unpredictable{} behavior.
+\pagebreak
+
+\import{insns/}{index.tex}
+
+\end{document}
diff --git a/formal/formal.sv b/formal/formal.sv
@@ -246,7 +246,7 @@ module boneless_formal(
                         assert (fi_mem_w_data == (mem[a_regY] << i_shift));
                     OPCODE_SHIFT_L, OPTYPE_ROT:
                         assert (fi_mem_w_data == (mem[a_regY] << i_shift) |
-                                             (mem[a_regY] >> (16 - i_shift)));
+                                                 (mem[a_regY] >> (16 - i_shift)));
                     OPCODE_SHIFT_R, OPTYPE_SRL:
                         assert (fi_mem_w_data == (mem[a_regY] >> i_shift));
                     OPCODE_SHIFT_R, OPTYPE_SRA:
-Original file line number
+Diff line change
@@ -0,0 +1,5 @@
+    *.aux
+    *.log
+    *.toc
+    *.out
+    *.cb*
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		\restrictions{If the long form is used, and \texttt{off8[8:3]} are non-zero, the behavior is \unpredictable.}
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1 @@
		\restrictions{If \texttt{Rb} contains a value greater than 15, the behavior is \unpredictable.}