Paper Number:15
Paper Title: Creating a Formal Verification Platform for IBM
CoreConnect-based SoC
Authors: Wen-Shiu Liao and Pao-Ann Hsiung

-------(Review 1)------------------------------------------
Appropriateness: 4
Originality: 2
Technical strength: 3
Presentation: 3

Overall': 3




Score values              0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). 
---------(Review 2)---------------------------------------------------------------------------------------------------------
Appropriateness:	3 
Originality: 		2
Technical strength: 	1
Presentation: 		2
-------------------------------------------------------------------------------------------------------------------
Overall: 2

Comments to the authors: 

This paper presents how to model IBM CoreConnect architecture by using
the formal verification platform that the authors developed. Since the
platform itself was presented in a different conference, the
contribution of this paper is the modeling part of IBM CoreConnect
architecture, and it is mentioned in Section 4.1.

It does not seem to me that this contribution is significant, because
the figure showing the PLB master model is rather straightforward. The
abstractions used are typical ones. If some case study is done using
the proposed model, it may be interesting. Especially, I'm very
interested in how the state explosion problem can be avoided for some
kind of actual application in the IBM CoreConnect
architecture. However, without any experimental results, I cannot
strongly recommend this paper to be accepted.



Score values              0 (reject), 1(weak reject), 2 (neutral), 3 (weak accept), and 4 (accept). 
----------(Review 3)--------------------------------------------------------------------------------------------------------
Appropriateness: 4
Originality: 2
Technical strength: 2
Presentation: 3
-------------------------------------------------------------------------------------------------------------------
Overall: 3

Comments to the authors: 

The authors use Timed Automata as the formal model to verify an IBM
CoreConnect-based System on Chip design. Although hardware
verification using discrete model is a common practice, it is
interesting to see that Timed Automata can be used as well. The
authors also perform manual abstraction to simplify the CoreConnect
specification. Finally, verification is performed on the CoreConnect
specification as well as an intergated design.

The clock model used in the paper is very natural. The authors use the
implicit global clock in Timed Automata to model multiple clocks with
different frequencies. In contrast, the verifier would explicitly
create a gloabl clock in discrete-timed models. The modeling of
CoreConnect, however, is less interesting to me. Perhaps the authors
could explain a little more about the architecture than a paragraph
with a timing diagram. 

Finally, I fail to see the significance of Figure 1 and 2 in this
work. Although both diagrams do have their respective merits, the
authors seldom mention them in the technical part of the paper. I
would suggest the authors to make the connection between the work and
their methodology clear.