| Summary: | The Instruction Set Architecture (ISA) describes the key functionalities of a processor design and is the most comprehensible format for enabling humans to understand the structure of the entire processor design. This thesis first introduces the construction of a generic ISA formal model with mathematical notations rather than programming languages, and demonstrates the extensions towards specific ISA designs. The stepwise refinement modeling technique gives rise to the hierarchically structured model, which eases the overall comprehensibility of the ISA and reduces the effort required for modeling similar designs. The ISA models serve as self-consistent, complete, and unambiguous specifications for coding, while helping engineers explore different design options beforehand. In the design phase, a selection of features is available to architects in order for the design to be trimmed towards a particular optimization target, e.g. low power consumption or fast computation, which can be assessed before implementation. However, taking verification into consideration, there is to my knowledge no way to estimate the difficulty of verifying a design before coding it. There needs to be a platform and a metric, from which both functional and non-functional properties can be quantitatively represented and then compared before implementation. Hence, this thesis secondly pro- poses a metric, based on the formally reasoned extension of the generic ISA models, as an estimator of some non-functional property, i.e. the verification complexity for achieving verification goals. The main claim of this thesis is that the verification complexity in simulation-based verification can be accurately retrieved from a hierarchically constructed ISA formal model in which the functionalities are fully specified with the correctness preserved. The modeling structure allows relative comparisons at a reasonably high level of abstraction brought by the hierarchically constructed formalization. The analysis on the experimental ISA emulator assesses the quality of the metric and concludes the applicability of the proposed metric.
|
|---|
