Lyrebird: assigning meanings to machines
David Cock · 2010
This paper presents work in progress on the Lyrebird frame-work, consisting of a language for specifying the programmer-visible behaviour of a processor and its associated devices, a tool for automatically producing a fast simulator, and a formal seman-tic interpretation providing a ma-chine model for use in an inter-active theorem prover. Machine specifications are modular, pro-viding abstract interfaces and structural parameterization (MMU-less processors, for example). Also presented is a specific example: An instantiation for the ARM1136jf-s core. 1