简介： 本发明提供了一种验证Cache一致性协议的装置，所述的装置包括：形式验证平台，利用验证平台内的验证工具，使用工具的内部变量失效命令对模型初始表中的状态变量进行失效；模型初始表，用来枚举模型中的状态变量并进行初始状态赋值；模型其他表，包含协议说明书或者说明表的所有协议表，用来定义模型协议表之间跳转接口，并实现模型协议表之间的跳转验证；模型规则定义表，用来定义模型协议表的跳转规则，以及检查Cache协议模型一致性。通过对模型中的变量状态进行组合，增加验证工具的验证路径，缩短验证时间。基于装置，本发明还提供了一种验证Cache一致性协议的方法。