L3: An ISA Specification Language
L3 is implemented in Poly/ML 5.5 and can downloaded from here: l3.tar.bz2 (22st July 2015).
Alexandre Joannou has provided support for Vim syntax highlighting. This is maintained at the repository vim-l3.
Some documentation is available here: l3.pdf.
The release contains a sample specification "tiny.spec" that is based on Thaker's Tiny 3 computer. For background information see Simon Moore's ECAD course notes.
ARM, MIPS and x86 models are available here: isa-models.tar.bz2.
- — The ARM model covers ARMv4 to ARMv7. It does not cover the Advanced SIMD extensions (Neon) or co-processor instructions. There is partial coverage for floating-point instructions (VFPv3-D32). There is also a separate ARMv8 model that covers AArch64 mode only. It also omits the Advanced SIMD and floating-point instructions.
- — The MIPS model is near complete for MIPS III (64-bit mode only). It does not cover floating-point and memory management instructions (e.g. TLBR and CACHE). Limited support is provided for some co-processor instructions. A more complete model is available on GitHub.
- — The x86 model covers a core selection of x86-64 instructions (64-bit mode only). It does not cover any extensions (x87 FPU, MMX, SSE and so forth).
The following are known users of our models/tools: