L3: A Specification Language for Instruction Set Architectures

L3 is implemented in Poly/ML 5.7 and the latest version is l3.tar.bz2 [2018-02-09]. 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.

Models

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.

HOL4 versions of these models can be found in the examples directory. These models are now available for use in Isabelle/HOL.

Users

The following are known users of our models/tools:

• — University of Cambridge Computer Laboratory and Chalmers University of Technology (Magnus Myreen and Hira Taqdees Syeda (formally at Data61))
• — KTH School of Computer Science and Communication
• — The Trustworthy Systems group at Data61. (Formerly called the Software Systems Research Group at NICTA.)
• — University of Wisconsin-Madison (Thomas Reps) and GrammaTech
• — University of Edinburgh School of Informatics (Brian Campbell)
• — Rockwell Collins
• — D-RisQ
• — SRI International (Prashanth Mundkur)