Towards Automatic Validation of Dynamic Behavior in Pipelined Processor Specifications

摘要

As embedded systems continue to face increasingly higher performance requirements, deeply pipelined processor architectures are being employed to meet desired system performance. A significant bottleneck in the validation of such systems is the lack of a golden reference model. Thus, many existing techniques employ a bottom-up approach to architecture validation, where the functionality of an existing pipelined architecture is, in essence, reverse-engineered from its implementation. Our validation technique is complementary to these bottom-up approaches. Our approach leverages the system architect's knowledge about the behavior of the pipelined architecture, through Architecture Description Language (ADL) constructs, and thus allows a powerful top-down approach to architecture validation. The most important requirement in top-down validation process is to ensure that the specification (reference model) is golden. Earlier, we have developed validation techniques to ensure that the static behavior of the pipeline is well-formed by analyzing the structural aspects of the specification using a graph based model. In this paper, we verify the dynamic behavior by analyzing the instruction flow in the pipeline using a Finite State Machine (FSM) based model to validate several important architectural properties such as determinism and in-order execution in the presence of hazards and multiple exceptions. We applied this methodology to the specification of a representative pipelined processor to demonstrate the usefulness of our approach.