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
Link To Document :
بازگشت