Speaker: Ziyad Hanna, Computing Laboratory, University of Oxford

Title : "ALM - Algorithm Level Modeling and Verification of Computer
Microarchitecture"

Abstract:
Design size and complexity continue to grow and outstrip what the
validation techniques can do for producing high quality and correct
hardware and software systems. As a results, the validation problem is
becoming more complex to solve and is indeed the main limiter for
producing a high quality products. Design abstraction and high level
modeling is a fundamental design strategy to cope with system
complexity.  

In this research we propose a new framework for algorithm-level modeling
(ALM) with a high level of specification and validation.  The semantics
of our models is based on Abstract State Machines (ASM - Yuri Gurevich
et al. ). Algorithm Level Models with this semantics are written at a
high level of representation in a hardware-oriented adaptation of AsmL,
an executable object-oriented language with rich data types.  The
framework we describe provides a semantic infrastructure for both formal
property verification and refinement verification.  It also provides a
link between Algorithm Level Models at the lowest level of abstraction
and Design Models, RTL - the industry's golden models for circuit
implementation.

In this talk, I will present a work in progress, starting by an overview
of the main ideas and description of the capabilities via a case study
to illustrate how ALM can be used for modeling and testing of in-order
instruction scheduler. We believe our approach will make it easier to
explore microarchitectural algorithms and to validate them using dynamic
or formal techniques. Recent progress will be outlined as well including
symbolic execution of programs, abstract data types for hardware, and
other verification techniques.