Verification of microarchitectural refinements in rule-based systems

Nirav Dave, Michael Katelman, Myron King, Arvind, Jose Meseguer

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

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.

Original languageEnglish (US)
Title of host publication9th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011
Pages61-71
Number of pages11
DOIs
StatePublished - Sep 1 2011
Event9th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011 - Cambridge, United Kingdom
Duration: Jul 11 2011Jul 13 2011

Publication series

Name9th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011

Other

Other9th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2011
CountryUnited Kingdom
CityCambridge
Period7/11/117/13/11

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Modeling and Simulation

Fingerprint Dive into the research topics of 'Verification of microarchitectural refinements in rule-based systems'. Together they form a unique fingerprint.

Cite this