• DocumentCode
    1835756
  • Title

    A design flow based on modular refinement

  • Author

    Dave, Nirav ; Ng, Man Cheuk ; Pellauer, Michael ; Arvind

  • Author_Institution
    Comput. Sci. & Artificial Intell. Lab., Massachusetts Inst. of Technol., Cambridge, MA, USA
  • fYear
    2010
  • fDate
    26-28 July 2010
  • Firstpage
    11
  • Lastpage
    20
  • Abstract
    We propose a practical methodology based on modular refinement to design complex systems. The methodology relies on modules with latency-insensitive interfaces so that the refinements can change the timing contract of a module without affecting the overall functional correctness of the system. Such refinements can exacerbate the unit testing problem for modules whose specifications admit a set of output behaviors for the same input (non-determinism), or modules whose input behavior may be affected by past outputs (feedback). We avoid the difficult problem of generating appropriate unit tests for such modules by using system-level tests as unit tests to verify the correctness of refined modules. We illustrate our methodology by showing how one might develop a microprocessor with an in-order pipeline. We then develop a superscalar pipeline using the in-order pipeline as the starting point. Our methodology leverages the effort of design exploration to reduce the effort of specifying interface contracts and unit testing.
  • Keywords
    formal verification; large-scale systems; multiprocessing systems; pipeline processing; program testing; programming languages; complex systems; design flow; in-order pipeline; latency-insensitive interfaces; microprocessor; modular refinement; overall functional correctness; past outputs; superscalar pipeline; system-level tests; timing contract; unit testing; Contracts; Hardware; Pipelines; Registers; Semantics; Testing; Timing;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Formal Methods and Models for Codesign (MEMOCODE), 2010 8th IEEE/ACM International Conference on
  • Conference_Location
    Grenoble
  • Print_ISBN
    978-1-4244-7885-9
  • Electronic_ISBN
    978-1-4244-7886-6
  • Type

    conf

  • DOI
    10.1109/MEMCOD.2010.5558626
  • Filename
    5558626