L3: An ISA Specification Language
L3 is implemented in Poly/ML 5.5 and can be downloaded from: l3.tar.bz2 (1st October 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).
versions of these models can be found in the examples directory
These models are now available
for use in Isabelle/HOL
The following are known users of our models/tools: