SoC Protocol Implementation Verification Using Instruction-Level Abstraction Specifications

Huaixi Lu, Yue Xing, Aarti Gupta, Sharad Malik

Research output: Contribution to journalArticlepeer-review

Abstract

In modern systems-on-chips, several hardware protocols are used for communication and interaction among different modules. These protocols are complex and need to be implemented correctly for correct operation of the system-on-chip. Therefore, protocol verification has received significant attention. However, this verification is often limited to checking high-level properties on a protocol specification or an implementation. Verifying these properties directly on an implementation faces scalability challenges due to its size and design complexity. Further, even after some high-level properties are verified, there is no guarantee that an implementation fully complies with a given specification, even if the same properties have also been checked on the specification. We address these challenges and gaps by adding a layer of component specifications, one for each component in the protocol implementation, and specifying and verifying the interactions at the interfaces between each pair of communicating components. We use the recently proposed formal model termed Instruction-Level Abstraction (ILA) as a component specification, which includes an interface specification for the interactions in composing different components. The use of ILA models as component specifications allows us to decompose the complete verification task into two sub-tasks: checking that the composition of ILAs is sequentially equivalent to a verified formal protocol specification, and checking that the protocol implementation is a refinement of the ILA composition. This check requires that each component implementation is a refinement of its ILA specification and includes interface checks guaranteeing that components interact with each other as specified. We have applied the proposed ILA-based methodology for protocol verification to several third-party design case studies. These include an AXI on-chip communication protocol, an off-chip communication protocol, and a cache coherence protocol. For each system, we successfully detected bugs in the implementation, and show that the full formal verification can be completed in reasonable time and effort.

Original languageEnglish (US)
Article number89
JournalACM Transactions on Design Automation of Electronic Systems
Volume28
Issue number6
DOIs
StatePublished - Oct 16 2023

All Science Journal Classification (ASJC) codes

  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design
  • Electrical and Electronic Engineering

Keywords

  • System-on-chip
  • formal verification
  • hardware protocol specification
  • instruction-level abstraction
  • refinement checking
  • sequential equivalence checking

Fingerprint

Dive into the research topics of 'SoC Protocol Implementation Verification Using Instruction-Level Abstraction Specifications'. Together they form a unique fingerprint.

Cite this