Cross-Abstraction Functional Verification and Performance Analysis of Chip Multiprocessor Designs

This paper introduces the cross-abstraction real-time analysis (Carta) framework for the model-based functional verification and performance estimation of chip multiprocessors (CMPs) utilizing bus matrix (crossbar switch) interconnection networks. We argue that the inherent complexity in CMP designs requires the synergistic use of various models of computation to efficiently manage the tradeoffs between accuracy and complexity. Our approach builds on domain-specific modeling languages (DSMLs) driving an open-source tool-chain that provides a cross-abstraction bridge between the finite-state machine (FSM), discrete-event (DE), and timed automata (TA) models of computation, and utilizes multiple model checkers to analyze formal properties at the cycle-accurate and transaction-level abstractions. The cross-abstraction analysis exploits accuracy for functional verification, and achieves significant speedups for performance estimation with marginal accuracy loss. We demonstrate results on an industrial strength networking CMP design utilizing a bus matrix interconnection network. To the best of our knowledge, the Carta framework is the first model-based tool-chain that utilizes multiple abstractions and model checkers for the comprehensive and formal functional verification, performance estimation, and real-time verification of bus matrix-based CMP designs.