Article ID | Journal | Published Year | Pages | File Type |
---|---|---|---|---|
422474 | Electronic Notes in Theoretical Computer Science | 2008 | 20 Pages |
Abstract
The refinement of an implementation-independent specification of an instruction set to a simple pipelined architecture is presented to illustrate subtleties in the formal development and analysis of pipelined hardware from such specifications. The Event-B language and its tool support (the Eclipse-based Rodin platform) is used for this purpose. The example demonstrates that naïve use of Event-B's superposition refinement fails to expose all of the potential hazards in pipelining. This paper introduces a form of 'event merging' to complete the analysis.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics