Hardware Murphi: An approach to raising the level of abstraction in hardware design and verification

Traditionally, early-stage hardware design has been based on informal engineering workbooks. In traditional hardware design projects, a precise functional model of the design is not created until the low-level register transfer level (RTL) design is developed.

There would be many advantages if design teams could write and verify precise functional models early in the design process. An early-stage functional model should be abstract, capturing the overall function of the design, but omitting many low-level implementation details.

• An early-stage functional model can be formally verified and simulated, to assure that the high-level design is sound.
• The functional model serves as a precise specification for implementing the actual hardware.
• When the hardware implementation is developed, it should be possible to formally verify that the hardware is a correct implementation of the functional model.

Many years of experience support the use of atomic guarded commands as the basis of high-level specifications. Among the specification methods based on guarded commands are Unity, Murphi, TLA+, and Bluespec.

In IBM, we have developed a hardware language called Hardware Murphi. Hardware Murphi extends the Murphi language of Dill into a hardware specification and implementation language.

Hardware language requirements
In order to take advantage of verification methods, the high-level specifications and the implementations need to be written in a language with the following properties:

• It should be possible to formally verify specifications written in the language. In practice, this requirement is most easily satisfied if the specification language provides a direct translation into finite-state machines, enabling the use of model checking.
• It should be possible to synthesize RTL descriptions from designs written in the language. This requirement can be satisfied if the specification language has a direct translation into a hardware description language such as VHDL or Verilog.
• It should be possible to formally verify that implementation-level designs satisfy their high-level specifications.

The Muv translator
Hardware Murphi has been designed to meet all of the above requirements. We are developing a translator called Muv, that translates Hardware Murphi designs into synthesizeable VHDL. Muv provides a way to verify a high-level design or synthesize a design into VHDL. Our language provides facilities for writing both high-level models and implementations.

Verifying implementations
To check the correctness of implementation models in Hardware Murphi, we are developing compositional methods for checking refinement between high-level and implementation models. We have used the compositional method to check the refinement of a complete cache coherence protocol model into a VHDL implementation.




Publications
1. S.M. German and G. Janssen, A tutorial example of a cache Memory Protocol and RTL implementation, IBM Research Report, RC23958, 2006.

2. X. Chen, S. German and G. Gopalakrishnan, Transaction based modeling and verification of hardware protocols, in Formal Methods in Computer-Aided Design, 2007.

Last updated August 15, 2007