BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Verification of Microarchitectural Refinements in  Rule-based Syst
 ems - Dr Nirav Dave\, MIT but heading to SRI
DTSTART:20110718T100000Z
DTEND:20110718T110000Z
UID:TALK32065@talks.cam.ac.uk
CONTACT:Prof Simon Moore
DESCRIPTION:Microarchitectural refinements are often required to meet perf
 ormance\, area\, or timing constraints when designing complex digital syst
 ems. While refinements are often straightforward to implement\, it is diff
 icult to formally specify the conditions of correctness for those which ch
 ange cycle-level timing. As a result\, in the later stages of design only 
 those changes are\nconsidered that do not affect timing and whose verifica
 tion can be automated using tools for checking FSM equivalence. This\nexcl
 udes an essential class of microarchitectural changes\, such as the insert
 ion of a register in a long combinational path to meet\ntiming.\n\nA desig
 n methodology based on guarded atomic actions\, or rules\, offers an oppor
 tunity to raise the notion of correctness\nto a more abstract level. In ru
 le-based systems\, many useful refinements can be expressed simply by brea
 king a single rule\ninto smaller rules which execute the original operatio
 n in multiple steps. Since the smaller rule executions can be interleaved 
 with\nother rules\, the verification task is to determine that no new beha
 viors have been introduced. We formalize this notion of\ncorrectness and p
 resent a tool based on SMT solvers that can automatically prove that a ref
 inement is correct\, or provide\nconcrete information as to why it is not 
 correct. With this tool\, a larger class of refinements at all stages of t
 he design process can\nbe verified easily. We demonstrate the use of our t
 ool in proving the correctness of the refinement of a processor pipeline f
 rom\nfour stages to five.\n
LOCATION:SS03\, Computer Laboratory
END:VEVENT
END:VCALENDAR