L3: A Specification Language for Instruction Set Architectures
L3 is implemented in Poly/ML and the latest version is l3.tar.bz2 [2016-06-24]. There is also a manual and an ITP 2012 paper: Directions in ISA specification.
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 in the GitHub repository l3mips.
- — 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).
- — Prashanth Mundkur has written an L3 specification of the RISC-V architecture. This is available in the GitHub repository l3riscv.
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: