Lyrebird — assigning meanings to machines
Authors
NICTA
UNSW
Abstract
This paper presents work in progress on the Lyrebird framework, 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 semantic interpretation providing a machine model for use in an interactive theorem prover. Machine specifications are modular, providing abstract interfaces and structural parameterization (MMU-less processors, for example). Also presented is a specific example: An instantiation for the ARM1136jf-s core.
BibTeX Entry
@inproceedings{Cock_10, month = oct, address = {Vancouver, BC, Canada }, publisher = {USENIX}, paperurl = {https://ts.data61.csiro.au/publications/nicta_full_text/3996.pdf}, booktitle = {Systems Software Verification}, slides = {http://ts.data61.csiro.au/publications/nicta_slides/3996.pdf}, author = {Cock, David}, year = {2010}, pages = {1--9}, title = {Lyrebird --- Assigning Meanings to Machines} }