Processor Memory System Verification using DOGReL

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

• Daryl Stewart, ARM
• Wednesday 25 March 2015, 13:00-14:00
• FW11.

If you have a question about this talk, please contact Peter Sewell.

The memory subsystem of a microprocessor is responsible for scheduling memory accesses as efficiently as possible, hiding latency costs from the Data Processing Unit and, ideally, minimizing power costs. For ARM processors, requirements on ordering and completion of memory accesses from the ARM Architecture and relevant bus protocols specify an envelope of acceptable behavior that must be maintained by the schedule. Consequently, any given sequence of instructions can be satisfied by a range of different schedules. Verifying the correctness of the memory subsystem is therefore a complex task, often on the critical path to release. Inspired by earlier work on specifying end-to-end properties we developed a language of Directed Observer Graphs (DOGReL) capable of expressing implementation independent properties at a level of abstraction between architecture and micro-architecture that specify the behavior of the memory subsystem. These properties are then translated into System Verilog monitors which can be applied for bug-hunting at the RTL level using commercial Model Checking tools. During a recent micro-controller design project at ARM these properties proved highly valuable in detecting bugs earlier in the design cycle than simulation. The process of writing an unambiguous specification also exposed early design flaws and provided clearer documentation of the required behaviors for engineers. In this talk I’ll cover some of the concepts we use for expressing expected ordering in the memory system and should have time to explore any other aspects which interest the audience.

D. Stewart, D. Gilday, D. Nevill, and T. Roberts, “Processor Memory System Verification using DOG ReL: a language for specifying End-to-End properties”, International Workshop on Design and Implementation of Formal Tools and Systems

http://fmgroup.polito.it/cabodi/difts2014/papers/difts2014_submission_6.pdf

This talk is part of the REMS lunch series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Department of Computer Science and Technology talks and seminars
• FW11
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.