Keerthikumara Devarajegowda

• In this thesis, the software development principles of Model-Driven Architecture have been adopted for developing a generation flow for properties. The taken approach for property generation introduces three models, namely the Model-of-Things, the Model-of-Property, and the Model-of-View. Each model belongs to a distinct model layer in the generation flow and each model layer addresses a specific concern of the property generation. The separation of concerns through model layers ensures modular flow development, and enables uncomplicated enhancements and feature extensions. The properties are generated through a series of model-to-model transformations between these model layers. Python is used as the domain-specific language for describing the intermediate transformations. A metamodel-based automation framework is utilized to generate an infrastructure that facilitates the description of transformations. The APIs that form the central part of the infrastructure are generated from the metamodel definitions of the models mentioned before. The generated APIs are further extended with domain-specific APIs to significantly reduce the effort required for developing the transformations. The property generation solution developed in this thesis is termed as “MetaProp”. A key aspect of the property generation flow is the translation of informal specifications to formal specification models. Due to the diverse nature of hardware designs, the methodology includes different modeling paradigms to formalize the specifications. The metamodel Meta-Expression provides features to describe the behavior of combinational designs in the form of expression trees and dataflow expressions. The MetaExpression metamodel is modular in nature and can be integrated into other metamodel definitions that capture the specification level configurations of the design. For modeling the behavior of sequential designs, a formalism using finite state machine-like notations for traces is introduced. The metamodel MetaSTS defines this formalism. The MetaSTS metamodel enables to define the behavior of sequential designs with annotated timing information for transitions between important states. Annotation is also used to map abstract states in the Model-of-Things to the Model-of-Property and, finally, to the design implementation. Such an annotation or binding mechanism enables Model-of-Properties to be applicable on a variety of design implementations. Another important contribution of this thesis is a complete processor verification methodology, which is based on the aforementioned generation approach. The introduced methods for specification modeling are employed to formalize the ISA and the behavior of instructions within the processor pipelines. However, it requires substantial manual efforts and in-depth knowledge of the microarchitectural details of the processor implementation to describe the transformations that define the Model-of-Properties. The prime reason for this requirement is the overlapped execution of instructions within the pipelined architectures of processors and the numerous internal and external pipeline stall scenarios. For a complete processor verification, a set of generated properties must consider all combinations of instruction overlapping coupled with all scenarios of pipeline stalls. In retrospect, the Model-of-Properties —from which the properties are generated — are required to consider all combinations of the aforementioned scenarios. To address these aspects, the C-S²QED method — an extension of the S²QED method — has been developed to completely verify a processor. The C-S²QED method is also applicable to exceptions within the processor pipelines and superscalar pipeline architectures. The C-S²QED method detects all functional bugs in a processor implementation and requires significantly less manual efforts compared to state-of-the-art processor verification methods. The completeness hypothesis of the C-S²QED method based on the completeness criterion defined by C-IPC and a completeness proof are also part of this thesis. The property generation flow has been leveraged to generate a set of C-S²QED properties to further enhance the effectiveness of the methodology. The applicability and effectiveness of the introduced modeling paradigms and developed methods have been demonstrated with the formal verification of several industry strength designs. Numerous logic bugs including the bugs that are typically regarded as difficult to find have been detected during the formal verification with generated properties. Most IPs of an SoC called “RiVal” including the RISC-V core and excluding the legacy IPs have been formally verified only with the proposed methods in this thesis. The Rival SoC is used in the powertrain and safety automotive applications. The manufactured chip works “first time right” and no logic bug has been detected during the post-manufacturing tests. Various architectural alternatives of the RISC-V based processor designs are verified with the generated C-S²QED properties. The property generation is built in a configurable manner such that any changes in microarchitecture of the processor — that may be caused by the changes in specifications — are implicitly covered by the generation flow. Thus, additional manual efforts are not required and the functional flaws due to the changes in specifications are neutralized. Furthermore, the proposed methods have also been applied to communication protocol IPs, bus bridges, interrupt controllers and safety-relevant designs.