• Login
    View Item 
    •   DORA Home
    • Faculty of Computing, Engineering and Media
    • School of Computer Science and Informatics
    • View Item
    •   DORA Home
    • Faculty of Computing, Engineering and Media
    • School of Computer Science and Informatics
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Proving the correctness of the interlock mechanism in processor design.

    Thumbnail
    View/Open
    Main article text (142.7Kb)
    Main article in postscript (193.0Kb)
    Date
    1997
    Author
    Li, Xiaoshan;
    Cau, A. (Antonio);
    Moszkowski, B. C.;
    Coleman, Nick;
    Zedan, Hussein
    Metadata
    Show attachments and full item record
    Abstract
    In this paper, Interval Temporal Logic (ITL) us used to specify and verify the event processor EP/3, which is a multi-threaded pipeline processor capable of executing parallel programs. We first give the high level specification of the EP/3 with emphasis on the interlock mechanism. The interlock mechanism is used in processor design especially for dealing with pipeline conflict problems. We prove that the specification satisfies certain safety and liveness properties. An advantage of ITL is that it has an executable part, i.e., we can simulate a specification before proving properties about it. This will help us to get the right specification.
    Description
    Citation : Li, X., Cau, A., Moszkowski, B., Coleman, N. and Zedan, H. (1997) Proving the correctness of the interlock mechanism in processor design. In: Advances in hardware design and verification: IFIP TC10 WG10.5 International Conference on Correct Hardware and Verification Methods, 16-18 October 1997, Montreal Canada, edited by Hon F. Li and David K. Probst, London: Chapman & Hall, on behalf of the International Federation for Information Processing (IFIP), 1997, pp?
    URI
    http://hdl.handle.net/2086/43
    DOI
    http://dx.doi.org/10.1007/978-0-387-35190-2_2
    ISBN : 0412813300
    Research Group : Software Technology Research Laboratory (STRL)
    Collections
    • School of Computer Science and Informatics [2966]

    Submission Guide | Reporting Guide | Reporting Tool | DMU Open Access Libguide | Take Down Policy | Connect with DORA
    DMU LIbrary
     

     

    Browse

    All of DORACommunities & CollectionsAuthorsTitlesSubjects/KeywordsResearch InstituteBy Publication DateBy Submission DateThis CollectionAuthorsTitlesSubjects/KeywordsResearch InstituteBy Publication DateBy Submission Date

    My Account

    Login

    Submission Guide | Reporting Guide | Reporting Tool | DMU Open Access Libguide | Take Down Policy | Connect with DORA
    DMU LIbrary