Compositional Verification Using a Formal Component and Interface Specification

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 r equires a dditional v erification since incorrect communication at their interface may invalidate the properties that have been checked for the individual components. This paper focuses on a specification f or t heir i nterface which can be checked individually for each component, and which guarantees that refinement-based p roperties c hecked f or 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 p rovides a uniform specification for processors, accelerators a nd 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 o f t he ILA s pecification. 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 o f t he I LA 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.