Abstract
As embedded systems continue to face increasingly higher performance requirements, deeply pipelined processor ar-chitectures are being employed to meet desired system per-formance. System architects critically need modeling tech-niques that allow exploration, evaluation, customization and validation of different processor pipeline configurations, tuned for a specific application domain. We propose a novel Finite State Machine (FSM) based modeling of pipelined processors and define a set of properties that can be used to verify the correctness of in-order execution in the presence of fragmented pipelines and multicycle functional units. Our approach leverages the system architect?s knowledge about the behavior of the pipelined processor, through Architecture Description Language (ADL) constructs, and thus allows a powerful top-down approach to pipeline verification. We ap-plied this methodology to the DLX processor to demonstrate the usefulness of our approach.