Sail is a language for describing the instruction semantics of processors.
It has been used in several papers, available from http://www.cl.cam.ac.uk/~pes20/sail/.