Verification of microarchitectural refinements in rule-based systems
http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5970511&tag=1
| Main Authors: | , , , |
|---|---|
| Other Authors: | |
| Format: | Article |
| Language: | en_US |
| Published: |
Institute of Electrical and Electronics Engineers
2012
|
| Online Access: | http://hdl.handle.net/1721.1/73470 https://orcid.org/0000-0002-9737-2366 https://orcid.org/0000-0003-2075-4654 |
| _version_ | 1826188074223140864 |
|---|---|
| author | Dave, Nirav H. Katelman, Michael King, Myron Decker Mithal, Arvind |
| author2 | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory |
| author_facet | Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Dave, Nirav H. Katelman, Michael King, Myron Decker Mithal, Arvind |
| author_sort | Dave, Nirav H. |
| collection | MIT |
| description | http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5970511&tag=1 |
| first_indexed | 2024-09-23T07:54:11Z |
| format | Article |
| id | mit-1721.1/73470 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T07:54:11Z |
| publishDate | 2012 |
| publisher | Institute of Electrical and Electronics Engineers |
| record_format | dspace |
| spelling | mit-1721.1/734702022-09-30T00:53:53Z Verification of microarchitectural refinements in rule-based systems Dave, Nirav H. Katelman, Michael King, Myron Decker Mithal, Arvind Massachusetts Institute of Technology. Computer Science and Artificial Intelligence Laboratory Mithal, Arvind Dave, Nirav H. Mithal, Arvind King, Myron Decker http://ieeexplore.ieee.org/xpls/abs_all.jsp?arnumber=5970511&tag=1 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. National Science Foundation (U.S.) (NSF (#CCF-0541164)) 2012-09-28T15:08:34Z 2012-09-28T15:08:34Z 2011-07 Article http://purl.org/eprint/type/ConferencePaper 978-1-4577-0118-4 1457701189 INSPEC Accession Number: 12145172 http://hdl.handle.net/1721.1/73470 Dave, Nirav et al. “Verification of Microarchitectural Refinements in Rule-based Systems.” 2011 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE) IEEE, 11-13 July 2011. 61–71. Web. https://orcid.org/0000-0002-9737-2366 https://orcid.org/0000-0003-2075-4654 en_US http://dx.doi.org/10.1109/MEMCOD.2011.5970511 2011 9th IEEE/ACM International Conference on Formal Methods and Models for Codesign (MEMOCODE) Creative Commons Attribution-Noncommercial-Share Alike 3.0 http://creativecommons.org/licenses/by-nc-sa/3.0/ application/pdf Institute of Electrical and Electronics Engineers MIT web domain |
| spellingShingle | Dave, Nirav H. Katelman, Michael King, Myron Decker Mithal, Arvind Verification of microarchitectural refinements in rule-based systems |
| title | Verification of microarchitectural refinements in rule-based systems |
| title_full | Verification of microarchitectural refinements in rule-based systems |
| title_fullStr | Verification of microarchitectural refinements in rule-based systems |
| title_full_unstemmed | Verification of microarchitectural refinements in rule-based systems |
| title_short | Verification of microarchitectural refinements in rule-based systems |
| title_sort | verification of microarchitectural refinements in rule based systems |
| url | http://hdl.handle.net/1721.1/73470 https://orcid.org/0000-0002-9737-2366 https://orcid.org/0000-0003-2075-4654 |
| work_keys_str_mv | AT daveniravh verificationofmicroarchitecturalrefinementsinrulebasedsystems AT katelmanmichael verificationofmicroarchitecturalrefinementsinrulebasedsystems AT kingmyrondecker verificationofmicroarchitecturalrefinementsinrulebasedsystems AT mithalarvind verificationofmicroarchitecturalrefinementsinrulebasedsystems |