The advantages and disadvantages of top-down hardware design methodologies based on the formal verification of transitions to subsequent design steps are illustrated in detail. The methodology is illustrated on a nontrivial example: a Rollback accelerator chip to improve the performance of distributed (discrete) simulations. The fundamental novel idea of the approach discussed in this paper is the combination of designer experience with respect to optimal performance of digital circuits with formal techniques by not trying to build a compiler to automate the conversion from a higher level to a lower level, but doing the design manually and then verifying this implementation at a lower level against the higher-level specification semiautomatically. It is also clear that this is how the design was done: one author,  Fujimoto,  has a lot of design and application experience, and the other is knowledgeable in the field of formal techniques. A good informal and formal description of the Rollback Chip is given, although some knowledge of its application field (distributed discrete event simulation) will help the reader understand its function. Although an introductory description of Miranda is given, the use of the dedicated language HOP sometimes makes it difficult for readers unfamiliar with this specific language to understand the details. The use of such a language also illustrates that no standard (de facto or otherwise) exists in this field and that a lot more research is needed in order to identify key features to be supported by a general-purpose hardware description language. The core of the paper is also a good illustration of the strategy of top-down stepwise refinement in hardware design. The authors give a timing estimate of the parts of their work so that the increases in productivity from their method (once it is learned), both in design time and in the quality of the end result, are quantified.

The paper is definitely oriented toward researchers and fulfills its purpose for this audience. Its length is good, although readers unfamiliar with Miranda might appreciate a more elaborate introduction to this language and HOP. The best feature of this paper is its completeness in giving a detailed overview of the authors’ design process and methodology. A disadvantage could be that advanced knowledge of distributed discrete simulation and functional (hardware) description languages is almost required, but this requirement should be seen in the context of the intended audience of specialists and researchers in this field. The references and the physical presentation are good.