# rubyphi

**Repository Path**: twohaha/rubyphi

## Basic Information

- **Project Name**: rubyphi
- **Description**: No description available
- **Primary Language**: Unknown
- **License**: MIT
- **Default Branch**: master
- **Homepage**: None
- **GVP Project**: No

## Statistics

- **Stars**: 0
- **Forks**: 0
- **Created**: 2024-05-08
- **Last Updated**: 2024-07-22

## Categories & Tags

**Categories**: Uncategorized

**Tags**: None

## README

# Rubyphi: Automatic Verification of Ruby Protocol with Murphi

Rubyphi is an automated verification tool that automatically translates cache coherence protocols defined in [Gem5](https://www.gem5.org/)'s [Ruby](https://www.gem5.org/documentation/learning_gem5/part3/MSIintro/) system into a file recognized by the model checking tool Murphi. Then Murphi can detect errors in Ruby protocols and provide the input that triggers the error.

## Supported Protocols

- [MESI_Two_Level](https://www.gem5.org/documentation/general_docs/ruby/MESI_Two_Level/)
- [MI_example](https://www.gem5.org/documentation/general_docs/ruby/MI_example/)

## Bug Report

We will update the bugs discovered through Rubyphi in the following table.

<table>
  <tr>
    <th>Bug ID</th>
    <th>Protocol</th>
    <th>Description</th>
    <th>Gem5 Issue/PR</th>
  </tr>
  <tr>
    <td>1</td>
    <td>MI</td>
    <td>Unhandled events DMA_READ & DMA_WRITE in M_DRDI</td>
    <td rowspan="2">
    <a href="https://github.com/gem5/gem5/issues/1210">issue 1210</a>
    <br>
    <a href="https://github.com/gem5/gem5/pull/1236">PR 1236</a>
    </td>
  </tr>
  <tr>
    <td>2</td>
    <td>MI</td>
    <td>Unhandled event PUTX_NotOwner in {M_DWR, M_DRD, M_DRDI, M_DWRI}</td>
  </tr>
</table>

## Requirements

python >= 3.10.14

transitions >= 0.9.0

## Quick Start

### Generate murphi files

To generate murphi files for the protocol, see _tests/test.py_.

### Model Checking with Murphi

- [Murphi](https://gitee.com/twohaha/murphi): Model Checking with single thread
- [Eddy_Murphi](https://gitee.com/twohaha/Eddy_Murphi): Model Checking with multiple threads (MPI)

## Contributors

- Xuezheng (xuezhengxu@126.com)