The Sail instruction-set semantics specification language
Vendor architecture specification documents typically describe the sequential behaviour of their ISA with a combination of prose, tables, and pseudocode for each instruction.
They vary in how precise that pseudocode is: in some it is just suggestive, while in others it is close to a complete description of the envelope of architecturally allowed behaviour for sequential code.
For x86 [1] , the Intel pseudocode is just suggestive, with embedded prose, while the AMD descriptions [2] are prose alone. For IBM Power [3] , there is detailed pseudocode which has recently become machine-processed [4] . For Arm [5] , there is detailed pseudocode, which has recently become machine-processed [6] . For MIPS [7, 8] there is also reasonably detailed pseudocode.
To be accessible to engineers familiar with existing vendor pseudocodes, with a similar style to the pseudocodes used by ARM and IBM Power (modulo minor syntactic differences);
