Verification of Microarchitectural Refinements in Rule-based Systems

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

• Dr Nirav Dave, MIT but heading to SRI
• Monday 18 July 2011, 11:00-12:00
• SS03, Computer Laboratory.

If you have a question about this talk, please contact Prof Simon Moore.

Note unusual time and location

Microarchitectural refinements are often required to meet performance, area, or timing constraints when designing complex digital systems. While refinements are often straightforward to implement, it is difficult to formally specify the conditions of correctness for those which change cycle-level timing. As a result, in the later stages of design only those changes are considered that do not affect timing and whose verification can be automated using tools for checking FSM equivalence. This excludes an essential class of microarchitectural changes, such as the insertion of a register in a long combinational path to meet timing.

A design methodology based on guarded atomic actions, or rules, offers an opportunity to raise the notion of correctness to a more abstract level. In rule-based systems, many useful refinements can be expressed simply by breaking a single rule into smaller rules which execute the original operation in multiple steps. Since the smaller rule executions can be interleaved with other rules, the verification task is to determine that no new behaviors have been introduced. We formalize this notion of correctness and present a tool based on SMT solvers that can automatically prove that a refinement is correct, or provide concrete information as to why it is not correct. With this tool, a larger class of refinements at all stages of the design process can be verified easily. We demonstrate the use of our tool in proving the correctness of the refinement of a processor pipeline from four stages to five.

This talk is part of the Computer Laboratory Computer Architecture Group Meeting series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Computer Architecture Group Meeting
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• SS03, Computer Laboratory
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31

Note that ex-directory lists are not shown.