Newsgroups: fr.announce.seminaires
Distribution: fr
From: Nelly.Maloisel@inria.COUPER-MOI.fr
Organization: INRIA-Rocquencourt
Subject: SEM - INRIA : Para - 14/12/98 - Paris - FR

           http://pauillac.inria.fr/bin/calendar/Seminaires


                             S E M I N A I R E
       ____               ____                             ___                
      /    _   _         /     __     __  /_  _   /       /   |  _   __   _   
     /    / \ / \  ___  /     /  | / /_  /   __| /  ___  /___/  __| /  | __|  
    |___  |_/ |_/      |____ /    / __/ |_  |_/ |_      /      |_/ /    |_/   
               /                                                              
              /                                                               
                          I N R I A - Rocquencourt, 
                       Salle de conference du Bat 08

                          lundi 14 decembre, 10h30

                              ----------------
                              Professor Arvind
                              ----------------

                                M.I.T. - LCS

     =================================================================
                                 Synthesis
     Titre-long : Synthesis and Verification of Modern Microprocessors
     =================================================================

 We have developed a new method for describing parallel and
 asynchronous systems and successfully applied it to describing
 micro-architectures and cache coherence protocols. The method is based
 on term rewriting systems (TRS), in which system states are specified
 by terms, and state transitions are defined by rewriting rules.  Such
 descriptions are amenable to formal verification as well as hardware
 synthesis.  The TRS descriptions provide an executable
 specification or a simulator, which is suitable for studying
 architecture related performance issues.

 We will present a TRS description of a modern speculative
 microprocessor and show its correctness vis-a-vis a non-pipelined,
 one-instruction-per-cycle implementation. We will discuss how a TRS
 can be transformed into another which is deeply pipelined, and then
 further transformed into one which does superscalar execution.
 Finally, we will show the actual hardware synthesis from the pipelined
 TRS. A synthesis tool under development will eventually
 generate structural Verilog from TRS's.
 
 The work on verification is done jointly with Xiaowei Shen, while the
 synthesis work is being done jointly with James Hoe and Professor
 Martin Rinard.