• Login
    View Item 
    •   SMARTech Home
    • Center for Experimental Research in Computer Systems (CERCS)
    • CERCS Technical Reports
    • View Item
    •   SMARTech Home
    • Center for Experimental Research in Computer Systems (CERCS)
    • CERCS Technical Reports
    • View Item
    JavaScript is disabled for your browser. Some features of this site may not work without it.

    Automatic Verification of Safety and Liveness for XScale-Like Processor Models Using WEB-Refinements

    Thumbnail
    View/Open
    git-cercs-03-17.pdf (66.97Kb)
    Date
    2003
    Author
    Manolios, Panagiotis
    Srinivasan, Sudarshan Kumar
    Metadata
    Show full item record
    Abstract
    We show how to automatically verify that a complex XScale-like pipelined machine model is a WEB-refinement of an instruction set architecture model, which implies that the machines satisfy the same safety and liveness properties. Automation is achieved by reducing the WEB-refinement proof obligation to a formula in the logic of Counter arithmetic with Lambda expressions and Uninterpreted functions (CLU). We use UCLID to transform the resulting CLU formula into a CNF formula, which is then checked with a SAT solver. We define several XScale-like models with out of order completion, including models with precise exceptions, branch prediction, and interrupts. We use two types of refinement maps. In one, flushing is used to map pipelined machine states to instruction set architecture states; in the other, we use the commitment approach, which is the dual of flushing, since partially completed instructions are invalidated. We present experimental results for all the machines mode! led, including verification times. For our application, we found that the SAT solver Siege provides superior performance over Chaff and that the amount of time spent proving liveness when using the commitment approach is less than 1% of the overall verification time, whereas when flushing is employed, the liveness proof accounts for about 10% of the verification time.
    URI
    http://hdl.handle.net/1853/5953
    Collections
    • CERCS Technical Reports [193]

    Browse

    All of SMARTechCommunities & CollectionsDatesAuthorsTitlesSubjectsTypesThis CollectionDatesAuthorsTitlesSubjectsTypes

    My SMARTech

    Login

    Statistics

    View Usage StatisticsView Google Analytics Statistics
    facebook instagram twitter youtube
    • My Account
    • Contact us
    • Directory
    • Campus Map
    • Support/Give
    • Library Accessibility
      • About SMARTech
      • SMARTech Terms of Use
    Georgia Tech Library266 4th Street NW, Atlanta, GA 30332
    404.894.4500
    • Emergency Information
    • Legal and Privacy Information
    • Human Trafficking Notice
    • Accessibility
    • Accountability
    • Accreditation
    • Employment
    © 2020 Georgia Institute of Technology