Industrial strength refinement checking

This paper discusses a methodology used on an industrial hardware development project to validate various cache-coherence protocol components. The idea is to use a high level model (HLM) written in Murphi for model checking purposes, and then to use the HLM as a checker during dynamic (i.e. simulation based-) validation of the RTL. Such a checker requires a formal notion of what it means for the RTL to implement the HLM. Due to RTL pipelining, concurrency, and different RTL/HLM semantics, an appropriate notion is nonobvious. We employ a notion we call behavioral refinement, and describe a methodology for creating refinement checkers. A novel aspect of our methodology is that all "ingredients" are specified using System Verilog (SV): even the Murphi model itself is compiled into SV. Thus any off-the-shelf SV simulation engine can be used. We report the successful use of our refinement checkers to catch bugs in a real project at Intel and give an example illustrating our method...

• Type: Conference
• Year: 2009
• Where: FMCAD
• Authors: Jesse D. Bingham, John Erickson, Gaurav Singh, Flemming Andersen
• Keywords: FMCAD 2009, Formal Methods, Methodology, Model Checking Purposes, Refinement Checkers