[otbn] Improve documentation for the Operations sections

Also get rid of the pseudo-code notes at the end: this related to a
version of the instruction set simulator from last summer; a lot has
changed since then!

Signed-off-by: Rupert Swarbrick <rswarbrick@lowrisc.org>
diff --git a/hw/ip/otbn/doc/isa.md b/hw/ip/otbn/doc/isa.md
index 0a987b5..0de8807 100644
--- a/hw/ip/otbn/doc/isa.md
+++ b/hw/ip/otbn/doc/isa.md
@@ -21,18 +21,60 @@
 These operands are further documented in a table.
 Immediate operands like `offset` show their valid range of values.
 
-In the pseudo-code in the Operation sections, all operands have integer values.
-These values come from the encoded bits in the instruction and the operand table describes exactly how.
-The `signed()` and `unsigned()` functions denote signed and unsigned extension from raw bits to an integer.
-Signed values are encoded 2's complement.
-Some operands are encoded PC-relative and have their absolute values when they appear in the Operation section.
-To show this, the operand table's description includes `PC` to denote the current value of the program counter as an integer.
-
 Below the table of operands is an encoding table.
 This shows how the 32 bits of the instruction word are filled in.
 Ranges of bits that map to an operand are named (in capitals) and those names are used in the operand table.
 For example, the `SW` instruction's `offset` operand is split across two ranges of bits (31:25 and 11:7) called `OFF_1` and `OFF_0`, respectively.
 
+# Pseudo-code for operation descriptions
+
+Each instruction has an Operation section.
+This is written in a Python-like pseudo-code, generated from the instruction set simulator (which can be found at `hw/ip/otbn/dv/otbnsim`).
+The code is generated from Python, but there are some extra changes made to aid readability.
+
+All instruction operands are considered to be in scope and have integer values.
+These values come from the encoded bits in the instruction and the operand table for the instruction describes exactly how they are decoded.
+Some operands are encoded PC-relative.
+Such an operand has its absolute value (an address) when it appears in the Operation section.
+
+Some state updates are represented as an assignment, but take effect at the end of the instruction.
+This includes register updates or jumps and branches (updating the PC).
+To denote this, we use the &#x21d0; symbol, reminiscent of Verilog's non-blocking assignment.
+
+The program counter (PC) is represented as a variable called `PC`.
+
+Machine registers are accessed with an array syntax.
+These arrays are:
+
+- `GPRs`: General purpose registers
+- `WDRs`: Wide data registers
+- `CSRs`: Control and status registers
+- `WSRs`: Wide special purpose registers
+
+Accesses to these arrays are as unsigned integers.
+The instruction descriptions are written to ensure that any value written to a register is representable.
+For example, a write to `GPRs[2]` will always have a non-negative value less than `1 << 32`.
+
+Memory accesses are represented as function calls.
+This is because the memory can be accessed on either the narrow or the wide side, which isn't easy to represent with an array syntax.
+Memory loads are represented as `DMEM.load_u32(addr)`, `DMEM.load_u256(addr)`.
+Memory stores are represented as `DMEM.store_u32(addr, value)` and `DMEM.store_u256(addr, value)`.
+In all cases, memory values are interpreted as unsigned integers and, as for register accesses, the instruction descriptions are written to ensure that any value stored to memory is representable.
+
+There are a few other helper functions, defined here to avoid having to inline their bodies into each instruction.
+```python3
+def from_2s_complement(n: int) -> int:
+    '''Interpret the bits of unsigned integer n as a 32-bit signed integer'''
+    assert 0 <= n < (1 << 32)
+    return n if n < (1 << 31) else n - (1 << 32)
+
+
+def to_2s_complement(n: int) -> int:
+    '''Interpret the bits of signed integer n as a 32-bit unsigned integer'''
+    assert -(1 << 31) <= n < (1 << 31)
+    return (1 << 32) + n if n < 0 else n
+```
+
 <!-- Documentation for the instructions in the ISA. Generated from ../data/insns.yml. -->
 # Base Instruction Subset
 
@@ -41,138 +83,3 @@
 # Big Number Instruction Subset
 
 {{< otbn_isa bignum >}}
-
-# Pseudo-Code Functions for BN Instructions
-
-The instruction description uses Python-based pseudocode.
-Commonly used functions are defined once below.
-
-<div class="bd-callout bd-callout-warning">
-  <h5>Note</h5>
-
-  This "pseudo-code" is intended to be Python 3, and contains known inconsistencies at the moment.
-  It will be further refined as we make progress in the implementation of a simulator using this syntax.
-</div>
-
-```python3
-class Flag(Enum):
-  C: Bits[1]
-  M: Bits[1]
-  L: Bits[1]
-  Z: Bits[1]
-
-class FlagGroup:
-  C: Bits[1]
-  M: Bits[1]
-  L: Bits[1]
-  Z: Bits[1]
-
-  def set(self, flag: Flag, value: Bits[1]):
-    assert flag in Flag
-
-    if flag == Flag.C:
-      self.C = value
-    elif flag == Flag.M:
-      self.M = value
-    elif flag == Flag.L:
-      self.L = value
-    elif flag == Flag.Z:
-      self.Z = value
-
-  def get(self, flag: Flag):
-    assert flag in Flag
-
-    if flag == Flag.C:
-      return self.C
-    elif flag == Flag.M:
-      return self.M
-    elif flag == Flag.L:
-      return self.L
-    elif flag == Flag.Z:
-      return self.Z
-
-
-class ShiftType(Enum):
-  LSL = 0 # logical shift left
-  LSR = 1 # logical shift right
-
-class HalfWord(Enum):
-  LOWER = 0 # lower or less significant half-word
-  UPPER = 1 # upper or more significant half-word
-
-def DecodeShiftType(st: Bits(1)) -> ShiftType:
-  if st == 0:
-    return ShiftType.LSL
-  elif st == 1:
-    return ShiftType.LSR
-  else:
-    raise UndefinedException()
-
-def DecodeFlagGroup(flag_group: Bits(1)) -> UInt:
-  if flag_group > 1:
-    raise UndefinedException()
-  return UInt(flag_group)
-
-def DecodeFlag(flag: Bits(1)) -> Flag:
-  if flag == 0:
-    return ShiftType.C
-  elif flag == 1:
-    return ShiftType.M
-  elif flag == 2:
-    return ShiftType.L
-  elif flag == 3:
-    return ShiftType.Z
-  else:
-    raise UndefinedException()
-
-
-def ShiftReg(reg, shift_type, shift_bytes) -> Bits(N):
-  if ShiftType == ShiftType.LSL:
-    return GPR[reg] << shift_bytes << 3
-  elif ShiftType == ShiftType.LSR:
-    return GPR[reg] >> shift_bytes >> 3
-
-def AddWithCarry(a: Bits(WLEN), b: Bits(WLEN), carry_in: Bits(1)) -> (Bits(WLEN), FlagGroup):
-  result: Bits[WLEN+1] = a + b + carry_in
-
-  flags_out = FlagGroup()
-  flags_out.C = result[WLEN]
-  flags_out.L = result[0]
-  flags_out.M = result[WLEN-1]
-  flags_out.Z = (result[WLEN-1:0] == 0)
-
-  return (result[WLEN-1:0], flags_out)
-
-def SubtractWithBorrow(a: Bits(WLEN), b: Bits(WLEN), borrow_in: Bits(1)) -> (Bits(WLEN), FlagGroup):
-  result: Bits[WLEN+1] = a - b - borrow_in
-
-  flags_out = FlagGroup()
-  flags_out.C = result[WLEN]
-  flags_out.L = result[0]
-  flags_out.M = result[WLEN-1]
-  flags_out.Z = (result[WLEN-1:0] == 0)
-
-  return (result[WLEN-1:0], flags_out)
-
-def DecodeHalfWordSelect(hwsel: Bits(1)) -> HalfWord:
-  if hwsel == 0:
-    return HalfWord.LOWER
-  elif hwsel == 1:
-    return HalfWord.UPPER
-  else:
-    raise UndefinedException()
-
-def GetHalfWord(reg: integer, hwsel: HalfWord) -> Bits(WLEN/2):
-  if hwsel == HalfWord.LOWER:
-    return GPR[reg][WLEN/2-1:0]
-  elif hwsel == HalfWord.UPPER:
-    return GPR[reg][WLEN-1:WLEN/2]
-
-def LoadWlenWordFromMemory(byteaddr: integer) -> Bits(WLEN):
-  wordaddr = byteaddr >> 5
-  return DMEM[wordaddr]
-
-def StoreWlenWordToMemory(byteaddr: integer, storedata: Bits(WLEN)):
-  wordaddr = byteaddr >> 5
-  DMEM[wordaddr] = storedata
-```