Automatic Modeling and Validation of Pipeline Specifications driven by an Architecture Description Language

Verification is one of the most complex and expensive tasks in the current Systems-on-Chip (SOC) design process. Many existing approaches employ a bottom-up approach to pipeline validation, where the functionality of an existing pipelined processor is, in essence, reverse-engineered from its RT-level implementation. 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 pipeline validation. This paper addresses automatic validation of processor, memory, and co-processor pipelines described in an ADL. We present a graph-based modeling of architectures which captures both structure and behavior of the architecture. Based on this model, we present formal approaches for automatic validation of the architecture described in the ADL. We applied our methodology to verify several realistic architectures from different architectural domains to demonstrate the usefulness of our approach.