BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Processor Memory System Verification using DOGReL - Daryl Stewart\
 , ARM
DTSTART:20150325T130000Z
DTEND:20150325T140000Z
UID:TALK58646@talks.cam.ac.uk
CONTACT:Peter Sewell
DESCRIPTION:The memory subsystem of a microprocessor is responsible for sc
 heduling 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 access
 es from the ARM Architecture and relevant bus protocols specify an envelop
 e of acceptable behavior that must be maintained by the schedule. Conseque
 ntly\, any given sequence of instructions can be satisfied by a range of d
 ifferent schedules. Verifying the correctness of the memory subsystem is t
 herefore a complex task\, often on the critical path to release. Inspired 
 by earlier work on specifying end-to-end properties we developed a languag
 e of Directed Observer Graphs (DOGReL) capable of expressing implementatio
 n independent properties at a level of abstraction between architecture an
 d micro-architecture that specify the behavior of the memory subsystem. Th
 ese properties are then translated into System Verilog monitors which can 
 be applied for bug-hunting at the RTL level using commercial Model Checkin
 g tools. During a recent micro-controller design project at ARM these prop
 erties proved highly valuable in detecting bugs earlier in the design cycl
 e than simulation. The process of writing an unambiguous specification als
 o exposed early design flaws and provided clearer documentation of the req
 uired behaviors for engineers.\nIn this talk I’ll cover some of the conc
 epts we use for expressing expected ordering in the memory system and shou
 ld have time to explore any other aspects which interest the audience.\n\n
 D. Stewart\, D. Gilday\, D. Nevill\, and T. Roberts\, "Processor Memory Sy
 stem Verification using DOGReL: a language for specifying End-to-End prope
 rties"\, International Workshop on Design and Implementation of Formal Too
 ls and Systems\n\nhttp://fmgroup.polito.it/cabodi/difts2014/papers/difts20
 14_submission_6.pdf\n
LOCATION:FW11
END:VEVENT
END:VCALENDAR