Automatic synthesis of cache-coherence protocol processors using Bluespec

There are few published examples of the proof of correctness of a cache-coherence protocol expressed in an HDL. A designer generally shows the correctness of a protocol ny implementation details have been abstracted stract protocols are often expressed as a table of rules or state transition diagrams with an (implicit) model of atomic actions. There is enough of a semanbetween these high-level abstract descriptions and HDLs that the task of showing the correctness of an imtion of a verified abstract protocol is as daunting ng the correctness of the abstract protocol in the first place. The main contribution of this paper is to show

• Type: Conference
• Year: 2005
• Where: MEMOCODE
• Authors: Nirav Dave, Man Cheuk Ng, Arvind
• Keywords: Abstract Protocol, Correctness, MEMOCODE 2005, Protocol Ny Implementation