BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:The ARM Cortex-M1 Architecture in Coq - Samin Ishtiaq (Currently: 
 ARM)
DTSTART:20070619T120000Z
DTEND:20070619T130000Z
UID:TALK7412@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:We describe on-going work to define the latest ARM Cortex-M1 A
 rchitecture in the higher-order dependently-typed functional language of C
 oq\, and prove an ISA completeness result with regard to the verilog RTL i
 mplementation.\n\nThe current way of doing modelling and verification is a
 s follows: a high-level model is written in C++ and a low-level one in Ver
 ilog RTL. It is not possible to reason about the C++ model. There is also 
 no way to show logical equivalence between the C++ and Verilog models and 
 there is no way to compile the high-level model into an efficient implemen
 tation. In particular\, there is no way to show how compliant the RTL impl
 ementation is of the architecture. Admitedly\, both models pass the same t
 est suites\, but there are very likely deficiencies in the models and the 
 test suites that mean that some bugs are not found during development.\n\n
 Here\, we take a more formal approach by first describing the ARM architec
 ture in Coq\; we call this definition Spec. This is done in the expected w
 ay of defining the syntax and dynamic semantics of the Instruction Set Arc
 hitecture. The Memory and Exception Models of the architecture are more co
 mplex to formalize. It is important to consider how to structure the defin
 ition in terms of Coq's module system\, to enable architecture features to
  be combined. Spec is of independant value by itself\; for instance\, it c
 an be used to prove compiler rewrites are correct. But we concentrate here
  on the particular verification problem in trying to link the definition t
 o the separate RTL implementation\, which we do in two ways:\n\n* A formal
  ISA Completeness claim\n\nOn the other side of the fence\, in the RTL wor
 ld\, we write top-level OVL properties describing the ISA semantics in ter
 ms of pre- and post-conditions for each instruction. These properties effe
 ctively describe a transition relation which we call RTL. The properties a
 re written in a high-level\, architectural style\, using macros to represe
 nt architectural state in terms of the micro-architectural state. The RTL 
 and properties are then thrown over the wall to a standard model checker t
 o verify.\n\nRTL is then pulled back into the Coq world of Spec\; this is 
 possible because RTL only ever refers to architectural state. A completene
 ss result is proved by a simulation argument: that if both transition rela
 tions start in a similar state St and (St\,Spec) transitions to (St'\,Spec
 ')\, then (St\,RTL) transitions (in zero or more steps) to (St'\,RTL').\n\
 n* A correct-by-construction ISS\n\nAnother way to link Architecture and R
 TL is to use Coq's extraction facility to generate a purely-architectural 
 ISS to run software on. We will discuss the issues with trying to obtain a
  reasonably fast ISS this way.\n\nOur project begins with two assumptions:
  that the processor architecture needs to be defined\; and that micro-arch
 itects will still hand-code RTL for performance-per-watt efficiency. In bo
 th cases\, implementors need to be assured that they are building complian
 t micro-architectures. And while there have been several projects using fu
 nctional languages to model hardware\, none have addressed the fact that r
 eal-world microprocessors continue to be separately hand-coded.
LOCATION:Computer Laboratory\, William Gates Building\, Room GS15
END:VEVENT
END:VCALENDAR