Formatting table. Adding missing admonitions.

Removed grid lines from table to match LaTeX.
Added bullets to listing to match LaTeX.
Added missing admonitions.

1 files changed, 18 insertions, 22 deletions

diff --git a/src/mm-formal.adoc b/src/mm-formal.adoc
index cad4ac9..50028f5 100644
--- a/src/mm-formal.adoc
+++ b/src/mm-formal.adoc
@@ -638,53 +638,49 @@ state. Most states identify a pending memory or register operation,
 requested by the pseudocode, which the memory model has to do. The
 states are (this is a tagged union; tags in small-caps):
 
-[cols="<,<",]
+[cols="<,<",grid="none"]
 |===
-|Load_mem(_kind_, _address_, _size_, _load_continuation_) |memory load
+|Load_mem(_kind_, _address_, _size_, _load_continuation_) |- memory load
 operation
 
-|Early_sc_fail(_res_continuation_) |allow `sc` to fail early
+|Early_sc_fail(_res_continuation_) |- allow `sc` to fail early
 
-|Store_ea(_kind_, _address_, _size_, _next_state_) |memory store
+|Store_ea(_kind_, _address_, _size_, _next_state_) |- memory store
 effective address
 
-|Store_memv(_mem_value_, _store_continuation_) |memory store value
+|Store_memv(_mem_value_, _store_continuation_) |- memory store value
 
-|Fence(_kind_, _next_state_) |fence
+|Fence(_kind_, _next_state_) |- fence
 
-|Read_reg(_reg_name_, _read_continuation_) |register read
+|Read_reg(_reg_name_, _read_continuation_) |- register read
 
-|Write_reg(_reg_name_, _reg_value_, _next_state_) |register write
+|Write_reg(_reg_name_, _reg_value_, _next_state_) |- register write
 
-|Internal(_next_state_) |pseudocode internal step
+|Internal(_next_state_) |- pseudocode internal step
 
-|Done |end of pseudocode
+|Done |- end of pseudocode
 |===
 
 Here:
 
-_mem_value_ and _reg_value_ are lists of bytes;
-
-_address_ is an integer of XLEN bits;
+* _mem_value_ and _reg_value_ are lists of bytes;
+* _address_ is an integer of XLEN bits;
 
 for load/store, _kind_ identifies whether it is `lr/sc`,
 acquire-RCpc/release-RCpc, acquire-RCsc/release-RCsc,
 acquire-release-RCsc;
-
-for fence, _kind_ identifies whether it is a normal or TSO, and (for
+* for fence, _kind_ identifies whether it is a normal or TSO, and (for
 normal fences) the predecessor and successor ordering bits;
-
-_reg_name_ identifies a register and a slice thereof (start and end bit
-indices); and
-
-the continuations describe how the instruction instance will continue
+* _reg_name_ identifies a register and a slice thereof (start and end bit
+indices); and the continuations describe how the instruction instance will continue
 for each value that might be provided by the surrounding memory model
 (the _load_continuation_ and _read_continuation_ take the value loaded
 from memory and read from the previous register write, the
 _store_continuation_ takes _false_ for an `sc` that failed and _true_ in
 all other cases, and _res_continuation_ takes _false_ if the `sc` fails
 and _true_ otherwise).
-
+[NOTE]
+====
 For example, given the load instruction `lw x1,0(x2)`, an execution will
 typically go as follows. The initial execution state will be computed
 from the pseudocode for the given opcode. This can be expected to be
@@ -696,7 +692,7 @@ _load_continuation_). Feeding the 4-byte value loaded from memory
 location `0x4000`, say `0x42`, to _load_continuation_ returns
 Write_reg(`x1`, `0x42`, Done). Many Internal(_next_state_) states may
 appear before and between the states above.
-
+====
 Notice that writing to memory is split into two steps, Store_ea and
 Store_memv: the first one makes the memory footprint of the store
 provisionally known, and the second one adds the value to be stored. We