Skip to main content
CSIRO Logo Data 61 logo

Lyrebird — assigning meanings to machines

Authors

David Cock

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}
  }

Download