L3: An ISA Specification Language

L3 is implemented in Poly/ML 5.5 and can downloaded from here: l3.tar.bz2 (13th August 2014).

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.

Bibliography

Anthony Fox. Directions in ISA specification. In Interactive Theorem Proving (ITP), 2012.

Users

The following are known users of our models/tools: