L3: A Specification Language for Instruction Set Architectures
L3 is implemented in Poly/ML 5.5 and the latest version can be downloaded from l3.tar.bz2 [2015-11-27]. There is also a manual.
Alexandre Joannou has provided support for Vim syntax highlighting. This is maintained at the repository vim-l3.
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 in 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: