Compositional verification using a formal component and interface specification

Yue Xing, Huaixi Lu, Aarti Gupta, Sharad Malik

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

Property-based specification such as SystemVerilog Assertions (SVA) uses mathematical logic to specify the temporal behavior of RTL designs which can then be formally verified using model checking algorithms. These properties are specified for a single component (which may contain other components in the design hierarchy). Composing design components that have already been verified requires additional verification since incorrect communication at their interface may invalidate the properties that have been checked for the individual components. This paper focuses on a specification for their interface which can be checked individually for each component, and which guarantees that refinement-based properties checked for each component continue to hold after their composition. We do this in the setting of the Instruction-level Abstraction (ILA) specification and verification methodology. The ILA methodology provides a uniform specification for processors, accelerators and general modules at the instruction-level, and the automatic generation of a complete set of correctness properties for checking that the RTL model is a refinement of the ILA specification. We add an interface specification to model the inter-ILA communication. Further, we use our interface specification to generate a s et of interface checking properties that check that the communication between the RTL components is correct. This provides the following guarantee: if each RTL component is a refinement of its ILA specification and the interface checks pass, then the RTL composition is a refinement of the ILA composition. We have applied the proposed methodology to six case studies including parts of large-scale designs such as parts of the FlexASR and NVDLA machine learning accelerators, demonstrating the practical applicability of our method.

Original languageEnglish (US)
Title of host publicationProceedings of the 41st IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2022
PublisherInstitute of Electrical and Electronics Engineers Inc.
ISBN (Electronic)9781450392174
DOIs
StatePublished - Oct 30 2022
Event41st IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2022 - San Diego, United States
Duration: Oct 30 2022Nov 4 2022

Publication series

NameIEEE/ACM International Conference on Computer-Aided Design, Digest of Technical Papers, ICCAD
ISSN (Print)1092-3152

Conference

Conference41st IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2022
Country/TerritoryUnited States
CitySan Diego
Period10/30/2211/4/22

All Science Journal Classification (ASJC) codes

  • Software
  • Computer Science Applications
  • Computer Graphics and Computer-Aided Design

Fingerprint

Dive into the research topics of 'Compositional verification using a formal component and interface specification'. Together they form a unique fingerprint.

Cite this