The ARM Cortex-M1 Architecture in Coq

Add to your list(s) Download to your calendar using vCal

• Samin Ishtiaq (Currently: ARM)
• Tuesday 19 June 2007, 13:00-14:00
• Computer Laboratory, William Gates Building, Room GS15.

If you have a question about this talk, please contact Thomas Tuerk.

We describe on-going work to define the latest ARM Cortex-M1 Architecture in the higher-order dependently-typed functional language of Coq, and prove an ISA completeness result with regard to the verilog RTL implementation.

The current way of doing modelling and verification is as follows: a high-level model is written in C+ and a low-level one in Verilog 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 implementation. In particular, there is no way to show how compliant the RTL implementation is of the architecture. Admitedly, both models pass the same test suites, but there are very likely deficiencies in the models and the test suites that mean that some bugs are not found during development.

Here, we take a more formal approach by first describing the ARM architecture in Coq; we call this definition Spec. This is done in the expected way of defining the syntax and dynamic semantics of the Instruction Set Architecture. The Memory and Exception Models of the architecture are more complex to formalize. It is important to consider how to structure the definition in terms of Coq’s module system, to enable architecture features to be combined. Spec is of independant value by itself; for instance, it can be used to prove compiler rewrites are correct. But we concentrate here on the particular verification problem in trying to link the definition to the separate RTL implementation, which we do in two ways:

• A formal ISA Completeness claim

On the other side of the fence, in the RTL world, we write top-level OVL properties describing the ISA semantics in terms of pre- and post-conditions for each instruction. These properties effectively describe a transition relation which we call RTL . The properties are written in a high-level, architectural style, using macros to represent architectural state in terms of the micro-architectural state. The RTL and properties are then thrown over the wall to a standard model checker to verify.

RTL is then pulled back into the Coq world of Spec; this is possible because RTL only ever refers to architectural state. A completeness result is proved by a simulation argument: that if both transition relations 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’).

• A correct-by-construction ISS

Another way to link Architecture and RTL 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.

Our project begins with two assumptions: that the processor architecture needs to be defined; and that micro-architects will still hand-code RTL for performance-per-watt efficiency. In both cases, implementors need to be assured that they are building compliant micro-architectures. And while there have been several projects using functional languages to model hardware, none have addressed the fact that real-world microprocessors continue to be separately hand-coded.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room GS15
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.