Speaker/Affiliation: Steven Ge

rman/IBM T.J. Watson Research Center

Date/Time: Friday November 16
2007 1:30 p.m.

Where: ACES 6.304

Host: E. Allen Emerson<

br>
Talk Title: High Level Design and Refinement Checking in Hardware M

urphi

Talk Abstract:

Joint work with Geert Janssen (IBM) Xia

ofang Chen and Ganesh
Gopalakrishnan (University of Utah)

Specify

ing hardware using atomic guarded commands with interleaving
semantics i

s popular owing to the conceptual clarity of modeling and
verifying hig

h level behavior. To map such specifications into
hardware one can dec

ompose each specification transition into a
sequence of implementation t

ransitions taking one clock cycle each.
While the specification is inter

leaved the implementation allows many
operations to overlap in time.

We envision a development process in which an interleaving
specific

ation is refined into a concurrent implementation. In order
to support

this process we have defined the language Hardware
Murphi. Hardware M

urphi extends the Murphi language of Dill
%7B%5Cem et al%7D into a lang

uage of concurrent guarded commands with
shared variables. We have dev

eloped a translator from Hardware
Murphi into synthesizeable VHDL.
<

br>We have developed two methods for checking refinement between
interle

aved specifications and concurrent implementations. In the
monolithic

approach refinement is checked by building a cross-product
model which
is then model checked. In order to check refinement on
large implemen

tations we have developed a compositional approach
that divides the ch

ecking into a number of smaller models.

We have applied the refineme

nt checking methods to a non-trivial
benchmark example of a cache cohere

nce protocol showing that the
high-level specification is correctly ref

ined into an RTL implementation.

Speaker Bio:
Steven German studi

ed Applied Mathematics at Harvard University
receiving the Ph.D. degree
in 1981. His thesis presented the first
automated system for showing t

he absence of common runtime errors
in computer programs. He has worke

d in many areas of formal methods
including logics of programs systems
with many processes synthesis
of inductive assertions and verificatio

n hardware including arithmetic
hardware and processor pipelines. In I

BM he started a project that
currently verifies the cache coherence pr

otocols for IBM''s servers in
both the Power architecture pSeries and t